How to prove this lemma in Lean 4?

Stream: new members

[decade_g]

I'm trying to prove the following lemma in Lean 4:

import Mathlib
lemma two_pow_div (m n : ℕ) : 2^m / 2^n = 2^(m - n) := by

How can I prove this in Lean 4? Also, what is the best way to efficiently find similar theorems in Mathlib?

Thanks!

[Ruben Van de Velde]

@loogle ?x ^ ?n / ?x ^ ?m

[loogle]

:search: Nat.pow_div, zpow_natCast_sub_natCast, and 24 more

[Marcus Rossel]

I think this theorem doesn't hold when m < n, does it? Because then 2^m / 2^n = 0 wheres 2^(m - n) = 1.

[Marcus Rossel]

If I add the condition (h : n ≤ m), then using the apply? tactic suggests:

import Mathlib

lemma two_pow_div (m n : Nat) (h : n ≤ m) : 2^m / 2^n = 2^(m - n) := by
  refine Nat.pow_div h ?_
  -- Remaining goal: 0 < 2

[decade_g]

You're right! The theorem doesn't hold when both m and n are of type Nat.

But what if we change the statement to the following? How can we prove it in this case? The apply? tactic doesn't seem to provide a useful strategy here:

lemma two_pow_div (m n : ℤ) : (2 : ℝ)^m / 2^n = 2^(m - n) := by   sorry

[Kevin Buzzard]

import Mathlib

lemma two_pow_div (m n : ℤ) : (2 : ℝ)^m / 2^n = 2^(m - n) := by
  have h : (2 : ℝ) ≠ 0 := by norm_num -- mathematically necessary for the proof to work
  exact? -- finds it in the library

[Ruben Van de Velde]

It's the second suggestion from apply? on the live server for me

[Kevin Buzzard]

(Even without h it's second)

[Ruben Van de Velde]

And it's the third result in the loogle output above

[decade_g]

Are there any theorems in Lean 4's mathlib for summing geometric series? I've attempted to use 'apply?' and searched in Loogle but haven't found a suitable theorem. For instance, I'm trying to prove the following lemma:

import Mathlib

lemma two_pow_sum : ∀ (x y : ℕ), x ≤ y → ∑ a in Finset.Icc x y, (2 : ℝ)^a = 2^(y + 1) - 2^x := by
  intros x y hxy
  have h_2_ge_0 : (2 : ℝ) > 0 := by norm_num
  have h_2_not_1 : (2 : ℝ) ≠ 1 := by norm_num
  sorry

How to find such theorems in mathlib or how to prove this lemma?

[Ruben Van de Velde]

None with Finset.Icc, apparently, but there's a number of declarations with "geom" in the name that will hopefully help