awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable.{u_1, 0} (α := 𝕜) fun (c : ℕ+ × ℕ+) ↦ HPow.hPow (α := 𝕜) (↑(↑c.2 : ℕ) : 𝕜) k * r ^ ((↑c.1 : ℕ) * (↑c.2 : ℕ))

Tactic:
simpa [sigmaAntidiagonalEquivProd.summable_iff.symm] using summable_divisorsAntidiagonal_aux k hr

Premises used: _private.0.summable_divisorsAntidiagonal_aux, Equiv.summable_iff, sigmaAntidiagonalEquivProd, Iff.symm
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
this :
  Eq.{u_1 + 1} (α := 𝕜) (∑' (c : ℕ+ × ℕ+), HPow.hPow (α := 𝕜) (↑(↑c.2 : ℕ) : 𝕜) k * r ^ ((↑c.1 : ℕ) * (↑c.2 : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))
rwa rwa₁ rwa₂ rwa₃ :
  Eq.{u_1 + 1} (α := 𝕜) (∑' (p : ℕ+ × ℕ+), HPow.hPow (α := 𝕜) (↑(↑p.2 : ℕ) : 𝕜) k * r ^ ((↑p.1 : ℕ) * (↑p.2 : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑' (d : ℕ+) (c : ℕ+), HPow.hPow (α := 𝕜) (↑(↑c : ℕ) : 𝕜) k * r ^ ((↑d : ℕ) * (↑c : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))

Tactic:
rwa [← (summable_prod_mul_pow k hr).tsum_prod]

Premises used: summable_prod_mul_pow, Summable.tsum_prod
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
suffices :
  Eq.{u_1 + 1} (α := 𝕜) (∑' (c : ℕ+ × ℕ+), HPow.hPow (α := 𝕜) (↑(↑c.2 : ℕ) : 𝕜) k * r ^ ((↑c.1 : ℕ) * (↑c.2 : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑' (d : ℕ+) (c : ℕ+), HPow.hPow (α := 𝕜) (↑(↑c : ℕ) : 𝕜) k * r ^ ((↑d : ℕ) * (↑c : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))

Tactic:
suffices ∑' c : ℕ+ × ℕ+, c.2 ^ k * r ^ (c.1 * c.2 : ℕ) =
    ∑' e : ℕ+, σ k e * r ^ (e : ℕ) by rwa [← (summable_prod_mul_pow k hr).tsum_prod]
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
simp :
  Eq.{u_1 + 1} (α := 𝕜)
    (∑' (b : ℕ+) (c : ↥(↑b : ℕ).divisorsAntidiagonal),
      HPow.hPow (α := 𝕜) (↑(↑c : ℕ × ℕ).2 : 𝕜) k * r ^ ((↑c : ℕ × ℕ).1 * (↑c : ℕ × ℕ).2))
    (∑' (e : ℕ+), (∑ x ∈ (↑e : ℕ).divisors, HPow.hPow (α := 𝕜) (↑((↑e : ℕ) / x) : 𝕜) k) * r ^ (↑e : ℕ))
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑' (c : ℕ+ × ℕ+), HPow.hPow (α := 𝕜) (↑(↑c.2 : ℕ) : 𝕜) k * r ^ ((↑c.1 : ℕ) * (↑c.2 : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))

Tactic:
simp only [← sigmaAntidiagonalEquivProd.tsum_eq, sigmaAntidiagonalEquivProd,
    divisorsAntidiagonalFactors, PNat.mk_coe, Equiv.coe_fn_mk, sigma_eq_sum_div, cast_sum,
    cast_pow, Summable.tsum_sigma (summable_divisorsAntidiagonal_aux k hr)]

Premises used: divisorsAntidiagonalFactors, Summable.tsum_sigma, Equiv.tsum_eq, _private.0.summable_divisorsAntidiagonal_aux, Nat.cast_sum, Equiv.coe_fn_mk, sigmaAntidiagonalEquivProd, Nat.cast_pow, ArithmeticFunction.sigma_eq_sum_div, PNat.mk_coe
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑' (b : ℕ+) (c : ↥(↑b : ℕ).divisorsAntidiagonal),
      HPow.hPow (α := 𝕜) (↑(↑c : ℕ × ℕ).2 : 𝕜) k * r ^ ((↑c : ℕ × ℕ).1 * (↑c : ℕ × ℕ).2))
    (∑' (e : ℕ+), (∑ x ∈ (↑e : ℕ).divisors, HPow.hPow (α := 𝕜) (↑((↑e : ℕ) / x) : 𝕜) k) * r ^ (↑e : ℕ))

Tactic:
tsum_congr fun n ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
refine :
  ∀ (n : ℕ+),
    ∑' (c : ↥(↑n : ℕ).divisorsAntidiagonal),
        HPow.hPow (α := 𝕜) (↑(↑c : ℕ × ℕ).2 : 𝕜) k * r ^ ((↑c : ℕ × ℕ).1 * (↑c : ℕ × ℕ).2) =
      (∑ x ∈ (↑n : ℕ).divisors, HPow.hPow (α := 𝕜) (↑((↑n : ℕ) / x) : 𝕜) k) * r ^ (↑n : ℕ)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (∑' (b : ℕ+) (c : ↥(↑b : ℕ).divisorsAntidiagonal),
      HPow.hPow (α := 𝕜) (↑(↑c : ℕ × ℕ).2 : 𝕜) k * r ^ ((↑c : ℕ × ℕ).1 * (↑c : ℕ × ℕ).2))
    (∑' (e : ℕ+), (∑ x ∈ (↑e : ℕ).divisors, HPow.hPow (α := 𝕜) (↑((↑e : ℕ) / x) : 𝕜) k) * r ^ (↑e : ℕ))

Tactic:
refine tsum_congr fun n ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
n : ℕ+
i : ℕ
hi : i ∈ (↑n : ℕ).divisors
rw rw₁ :
  HPow.hPow (α := 𝕜) (↑((↑n : ℕ) / i) : 𝕜) k * r ^ (↑n : ℕ) = HPow.hPow (α := 𝕜) (↑((↑n : ℕ) / i) : 𝕜) k * r ^ (↑n : ℕ)
⊢ HPow.hPow (α := 𝕜) (↑((↑n : ℕ) / i) : 𝕜) k * r ^ (i * ((↑n : ℕ) / i)) =
    HPow.hPow (α := 𝕜) (↑((↑n : ℕ) / i) : 𝕜) k * r ^ (↑n : ℕ)

Tactic:
rw [Nat.mul_div_cancel' (dvd_of_mem_divisors hi)]

Premises used: Nat.dvd_of_mem_divisors, Nat.mul_div_cancel'
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
n : ℕ+
⊢ ∑' (c : ↥(↑n : ℕ).divisorsAntidiagonal),
      HPow.hPow (α := 𝕜) (↑(↑c : ℕ × ℕ).2 : 𝕜) k * r ^ ((↑c : ℕ × ℕ).1 * (↑c : ℕ × ℕ).2) =
    (∑ x ∈ (↑n : ℕ).divisors, HPow.hPow (α := 𝕜) (↑((↑n : ℕ) / x) : 𝕜) k) * r ^ (↑n : ℕ)

Tactic:
simpa [tsum_fintype, Finset.sum_mul,
    (n : ℕ).divisorsAntidiagonal.sum_attach fun x : ℕ × ℕ ↦ x.2 ^ k * r ^ (x.1 * x.2),
    sum_divisorsAntidiagonal fun x y ↦ y ^ k * r ^ (x * y)]
      using Finset.sum_congr rfl fun i hi ↦ by rw [Nat.mul_div_cancel' (dvd_of_mem_divisors hi)]

Premises used: PNat.val, HMul.hMul, Nat.divisorsAntidiagonal, Finset.sum_attach, Nat.cast, Prod.fst, HPow.hPow, tsum_fintype, Prod.snd, Finset.sum_congr, rfl, Finset.sum_mul, Nat.sum_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k m : ℕ
inst_3 : NeZero m
⊢ 0 ≤ ‖r‖

Tactic:
simp
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k m : ℕ
inst_3 : NeZero m
⊢ ‖r ^ m‖ < 1

Tactic:
simpa using pow_lt_one₀ (by simp) hr (NeZero.ne _)

Premises used: pow_lt_one₀, NeZero.ne
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
⊢ ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹

Tactic:
have (m : ℕ) [NeZero m] := tsum_geometric_of_norm_lt_one (ξ := r ^ m)
    (by simpa using pow_lt_one₀ (by simp) hr (NeZero.ne _))
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
simp :
  Eq.{u_1 + 1} (α := 𝕜) (∑' (n : ℕ+) (n_1 : ℕ+), HPow.hPow (α := 𝕜) (↑(↑n : ℕ) : 𝕜) k * (r ^ (↑n : ℕ)) ^ (↑n_1 : ℕ))
    (∑' (n : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑n : ℕ)) : 𝕜) * r ^ (↑n : ℕ))
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑' (n : ℕ+), HPow.hPow (α := 𝕜) (↑(↑n : ℕ) : 𝕜) k * r ^ (↑n : ℕ) / (1 - r ^ (↑n : ℕ)))
    (∑' (n : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑n : ℕ)) : 𝕜) * r ^ (↑n : ℕ))

Tactic:
simp only [div_eq_mul_inv, ← this, ← tsum_mul_left, mul_assoc, ← _root_.pow_succ',
    ← fun (n : ℕ) ↦ tsum_pnat_eq_tsum_succ (f := fun m ↦ n ^ k * (r ^ n) ^ m)]

Premises used: mul_assoc, tsum_pnat_eq_tsum_succ, tsum_mul_left, div_eq_mul_inv, pow_succ'
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑' (d : ℕ+) (c : ℕ+), HPow.hPow (α := 𝕜) (↑(↑c : ℕ) : 𝕜) k * r ^ ((↑d : ℕ) * (↑c : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))

Tactic:
have h00 := tsum_prod_pow_eq_tsum_sigma k hr
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
h00 :
  Eq.{u_1 + 1} (α := 𝕜) (∑' (d : ℕ+) (c : ℕ+), HPow.hPow (α := 𝕜) (↑(↑c : ℕ) : 𝕜) k * r ^ ((↑d : ℕ) * (↑c : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))
⊢ Summable.{u_1, 0} (α := 𝕜) (β := ℕ+ × ℕ+)
    (Function.uncurry fun (c d : ℕ+) ↦ HPow.hPow (α := 𝕜) (↑(↑c : ℕ) : 𝕜) k * r ^ ((↑d : ℕ) * (↑c : ℕ)))

Tactic:
apply (summable_prod_mul_pow k hr).prod_symm

Premises used: summable_prod_mul_pow, Summable.prod_symm
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
h00 :
  Eq.{u_1 + 1} (α := 𝕜) (∑' (d : ℕ+) (c : ℕ+), HPow.hPow (α := 𝕜) (↑(↑c : ℕ) : 𝕜) k * r ^ ((↑d : ℕ) * (↑c : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑' (b : ℕ+) (c : ℕ+), HPow.hPow (α := 𝕜) (↑(↑b : ℕ) : 𝕜) k * r ^ ((↑c : ℕ) * (↑b : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))

Tactic:
rw [Summable.tsum_comm (by apply (summable_prod_mul_pow k hr).prod_symm)] at h00

Premises used: Summable.tsum_comm
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
h00 :
  Eq.{u_1 + 1} (α := 𝕜) (∑' (b : ℕ+) (c : ℕ+), HPow.hPow (α := 𝕜) (↑(↑b : ℕ) : 𝕜) k * r ^ ((↑c : ℕ) * (↑b : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))
rw :
  Eq.{u_1 + 1} (α := 𝕜) (∑' (n : ℕ+) (n_1 : ℕ+), HPow.hPow (α := 𝕜) (↑(↑n : ℕ) : 𝕜) k * (r ^ (↑n : ℕ)) ^ (↑n_1 : ℕ))
    (∑' (b : ℕ+) (c : ℕ+), HPow.hPow (α := 𝕜) (↑(↑b : ℕ) : 𝕜) k * r ^ ((↑c : ℕ) * (↑b : ℕ)))
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑' (n : ℕ+) (n_1 : ℕ+), HPow.hPow (α := 𝕜) (↑(↑n : ℕ) : 𝕜) k * (r ^ (↑n : ℕ)) ^ (↑n_1 : ℕ))
    (∑' (n : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑n : ℕ)) : 𝕜) * r ^ (↑n : ℕ))

Tactic:
rw [← h00]
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
h00 :
  Eq.{u_1 + 1} (α := 𝕜) (∑' (b : ℕ+) (c : ℕ+), HPow.hPow (α := 𝕜) (↑(↑b : ℕ) : 𝕜) k * r ^ ((↑c : ℕ) * (↑b : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))
b c : ℕ+
⊢ HPow.hPow (α := 𝕜) (↑(↑b : ℕ) : 𝕜) k * (r ^ (↑b : ℕ)) ^ (↑c : ℕ) =
    HPow.hPow (α := 𝕜) (↑(↑b : ℕ) : 𝕜) k * r ^ ((↑c : ℕ) * (↑b : ℕ))

Tactic:
simp [mul_comm c.val b.val, pow_mul]

Premises used: PNat.val, pow_mul, mul_comm
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
h00 :
  Eq.{u_1 + 1} (α := 𝕜) (∑' (b : ℕ+) (c : ℕ+), HPow.hPow (α := 𝕜) (↑(↑b : ℕ) : 𝕜) k * r ^ ((↑c : ℕ) * (↑b : ℕ)))
    (∑' (e : ℕ+), (↑((σ k : (a : ℕ) → ℕ) (↑e : ℕ)) : 𝕜) * r ^ (↑e : ℕ))
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑' (n : ℕ+) (n_1 : ℕ+), HPow.hPow (α := 𝕜) (↑(↑n : ℕ) : 𝕜) k * (r ^ (↑n : ℕ)) ^ (↑n_1 : ℕ))
    (∑' (b : ℕ+) (c : ℕ+), HPow.hPow (α := 𝕜) (↑(↑b : ℕ) : 𝕜) k * r ^ ((↑c : ℕ) * (↑b : ℕ)))

Tactic:
exact tsum_congr₂ <| fun b c ↦ by simp [mul_comm c.val b.val, pow_mul]

Premises used: tsum_congr₂
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
m : ℕ+
rwa : ‖r‖ ^ (↑m : ℕ) < 1
rwa₁ rwa₂ rwa₃ rwa₄ : ‖r‖ < 1
⊢ ‖r ^ (↑m : ℕ)‖ < 1

Tactic:
rwa [norm_pow, pow_lt_one_iff_of_nonneg (norm_nonneg _) (NeZero.ne _)]

Premises used: norm_pow, pow_lt_one_iff_of_nonneg, norm_nonneg, NeZero.ne
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ ∀ (m : ℕ+), ‖r ^ (↑m : ℕ)‖ < 1

Tactic:
have h1 (m : ℕ+) : ‖r ^ (m : ℕ)‖ < 1 := by
    rwa [norm_pow, pow_lt_one_iff_of_nonneg (norm_nonneg _) (NeZero.ne _)]
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ (↑m : ℕ)‖ < 1
m : ℕ+
⊢ ∑' (n : ℕ), (r ^ (↑m : ℕ)) ^ n = (1 - r ^ (↑m : ℕ))⁻¹

Tactic:
have := tsum_geometric_of_norm_lt_one (h1 m)
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ (↑m : ℕ)‖ < 1
m : ℕ+
this : ∑' (n : ℕ), (r ^ (↑m : ℕ)) ^ n = (1 - r ^ (↑m : ℕ))⁻¹
⊢ HPow.hPow (β := ℕ) (r ^ (↑m : ℕ)) 0 + ∑' (n : ℕ+), (r ^ (↑m : ℕ)) ^ (↑n : ℕ) = (1 - r ^ (↑m : ℕ))⁻¹

Tactic:
rw [← tsum_zero_pnat_eq_tsum_nat (summable_geometric_of_norm_lt_one (h1 m))] at this

Premises used: tsum_zero_pnat_eq_tsum_nat, summable_geometric_of_norm_lt_one
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ (↑m : ℕ)‖ < 1
m : ℕ+
this : HPow.hPow (β := ℕ) (r ^ (↑m : ℕ)) 0 + ∑' (n : ℕ+), (r ^ (↑m : ℕ)) ^ (↑n : ℕ) = (1 - r ^ (↑m : ℕ))⁻¹
simp_rw :
  ∑' (n : ℕ+), r ^ ((↑n : ℕ) * (↑m : ℕ)) =
    HPow.hPow (β := ℕ) (r ^ (↑m : ℕ)) 0 + ∑' (n : ℕ+), (r ^ (↑m : ℕ)) ^ (↑n : ℕ) - 1
simp_rw₁ : ∑' (n : ℕ+), r ^ ((↑n : ℕ) * (↑m : ℕ)) = HAdd.hAdd (α := 𝕜) 1 (∑' (n : ℕ+), (r ^ (↑m : ℕ)) ^ (↑n : ℕ)) - 1
simp_rw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑' (n : ℕ+), r ^ ((↑n : ℕ) * (↑m : ℕ))) (∑' (n : ℕ+), (r ^ (↑m : ℕ)) ^ (↑n : ℕ))
simp_rw₃ : Eq.{u_1 + 1} (α := 𝕜) (∑' (n : ℕ+), r ^ ((↑m : ℕ) * (↑n : ℕ))) (∑' (n : ℕ+), (r ^ (↑m : ℕ)) ^ (↑n : ℕ))
⊢ ∑' (n : ℕ+), r ^ ((↑n : ℕ) * (↑m : ℕ)) = (1 - r ^ (↑m : ℕ))⁻¹ - 1

Tactic:
simp_rw [← this, pow_zero, add_sub_cancel_left, mul_comm, pow_mul]

Premises used: add_sub_cancel_left, pow_mul, pow_zero, mul_comm
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ (↑m : ℕ)‖ < 1
⊢ ∀ (m : ℕ+), ∑' (n : ℕ+), r ^ ((↑n : ℕ) * (↑m : ℕ)) = (1 - r ^ (↑m : ℕ))⁻¹ - 1

Tactic:
have h2 (m : ℕ+) : ∑' n : ℕ+, r ^ (n * m : ℕ) = (1 - r ^ (m : ℕ))⁻¹ - 1 := by
    have := tsum_geometric_of_norm_lt_one (h1 m)
    rw [← tsum_zero_pnat_eq_tsum_nat (summable_geometric_of_norm_lt_one (h1 m))] at this
    simp_rw [← this, pow_zero, add_sub_cancel_left, mul_comm, pow_mul]
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ (↑m : ℕ)‖ < 1
h2 : ∀ (m : ℕ+), ∑' (n : ℕ+), r ^ ((↑n : ℕ) * (↑m : ℕ)) = (1 - r ^ (↑m : ℕ))⁻¹ - 1
⊢ 𝓝 0 = 𝓝 ((HSub.hSub (α := 𝕜) 1 0)⁻¹ - 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ (↑m : ℕ)‖ < 1
h2 : ∀ (m : ℕ+), ∑' (n : ℕ+), r ^ ((↑n : ℕ) * (↑m : ℕ)) = (1 - r ^ (↑m : ℕ))⁻¹ - 1
⊢ HSub.hSub (α := 𝕜) 1 0 ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ (↑m : ℕ)‖ < 1
h2 : ∀ (m : ℕ+), ∑' (n : ℕ+), r ^ ((↑n : ℕ) * (↑m : ℕ)) = (1 - r ^ (↑m : ℕ))⁻¹ - 1
rw : Tendsto.{0, u_1} (β := 𝕜) (fun (x : ℕ+) ↦ r ^ (↑x : ℕ)) atTop (𝓝 0)
⊢ Tendsto.{0, u_1} (β := 𝕜) (fun (m : ℕ+) ↦ ∑' (n : ℕ+), r ^ ((↑n : ℕ) * (↑m : ℕ))) atTop (𝓝 0)

Tactic:
rw [funext h2, (by simp : 𝓝 (0 : 𝕜) = 𝓝 ((1 - 0)⁻¹ - 1)), tendsto_sub_const_iff,
    tendsto_inv_iff₀ (by simp), tendsto_const_sub_iff]

Premises used: Filter.tendsto_sub_const_iff, funext, tendsto_inv_iff₀, Filter.tendsto_const_sub_iff
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ (↑m : ℕ)‖ < 1
h2 : ∀ (m : ℕ+), ∑' (n : ℕ+), r ^ ((↑n : ℕ) * (↑m : ℕ)) = (1 - r ^ (↑m : ℕ))⁻¹ - 1
⊢ Tendsto.{0, u_1} (β := 𝕜) (fun (x : ℕ+) ↦ r ^ (↑x : ℕ)) atTop (𝓝 0)

Tactic:
(tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).comp <| tendsto_PNat_val_atTop_atTop

Premises used: tendsto_PNat_val_atTop_atTop, Filter.Tendsto.comp, tendsto_pow_atTop_nhds_zero_of_norm_lt_one
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ (↑m : ℕ)‖ < 1
h2 : ∀ (m : ℕ+), ∑' (n : ℕ+), r ^ ((↑n : ℕ) * (↑m : ℕ)) = (1 - r ^ (↑m : ℕ))⁻¹ - 1
⊢ Tendsto.{0, u_1} (β := 𝕜) (fun (x : ℕ+) ↦ r ^ (↑x : ℕ)) atTop (𝓝 0)

Tactic:
exact (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).comp <| tendsto_PNat_val_atTop_atTop

Premises used: tendsto_PNat_val_atTop_atTop, Filter.Tendsto.comp, tendsto_pow_atTop_nhds_zero_of_norm_lt_one
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedGroup A
n : ℕ
δ : ℝ
a : A
⊢ a ∈ approxOrderOf A n δ ↔ ∃ (b : A), orderOf b = n ∧ a ∈ ball b δ

Tactic:
simp only [approxOrderOf, thickening_eq_biUnion_ball, mem_iUnion₂, mem_setOf_eq, exists_prop]

Premises used: Metric.thickening_eq_biUnion_ball, Set.mem_setOf_eq, approxOrderOf, exists_prop, Set.mem_iUnion₂
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedGroup A
δ : ℕ → ℝ
a : A
⊢ a ∈ wellApproximable A δ ↔
    Membership.mem (γ := Set A) (blimsup (fun (n : ℕ) ↦ approxOrderOf A n (δ n)) atTop fun (n : ℕ) ↦ 0 < n) a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, wellApproximable
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
obtain : ∀ (b : A) (hb : orderOf b = n) (hab : a ∈ ball b δ), (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)
⊢ (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)

Tactic:
obtain ⟨b, hb, hab⟩ := mem_approxOrderOf_iff.mp ha

Premises used: mem_approxOrderOf_iff, Iff.mp
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hb : orderOf b = n
hab : a ∈ ball b δ
rw :
  ∀ (hmn : (orderOf b).Coprime m) (hb : orderOf b = n) (hab : a ∈ ball b δ),
    Membership.mem (γ := Set A) {u : A | orderOf u = orderOf b} (b ^ m)
⊢ Membership.mem (γ := Set A) {u : A | orderOf u = n} (b ^ m)

Tactic:
rw [← hb] at hmn ⊢
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hmn : (orderOf b).Coprime m
hb : orderOf b = n
hab : a ∈ ball b δ
⊢ Membership.mem (γ := Set A) {u : A | orderOf u = orderOf b} (b ^ m)

Tactic:
hmn.orderOf_pow

Premises used: Set.Mem, setOf, Nat.Coprime.orderOf_pow
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hmn : (orderOf b).Coprime m
hb : orderOf b = n
hab : a ∈ ball b δ
⊢ Membership.mem (γ := Set A) {u : A | orderOf u = orderOf b} (b ^ m)

Tactic:
exact hmn.orderOf_pow

Premises used: Nat.Coprime.orderOf_pow
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hb : orderOf b = n
hab : a ∈ ball b δ
⊢ Membership.mem (γ := Set A) {u : A | orderOf u = n} (b ^ m)

Tactic:
replace hb : b ^ m ∈ {u : A | orderOf u = n} := by
    rw [← hb] at hmn ⊢; exact hmn.orderOf_pow
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hab : a ∈ ball b δ
hb : Membership.mem (γ := Set A) {u : A | orderOf u = n} (b ^ m)
a₁ : (fun (y : A) ↦ y ^ m) a ∈ ball (b ^ m) (HSMul.hSMul (α := ℝ) (↑m : ℝ) δ)
⊢ (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)

Tactic:
apply ball_subset_thickening hb ((m : ℝ) • δ)

Premises used: Metric.ball_subset_thickening, Nat.cast, HSMul.hSMul
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hab : a ∈ ball b δ
hb : Membership.mem (γ := Set A) {u : A | orderOf u = n} (b ^ m)
⊢ a ^ m ∈ ball (b ^ m) (m • δ)

Tactic:
pow_mem_ball hm hab

Premises used: pow_mem_ball
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hab : a ∈ ball b δ
hb : Membership.mem (γ := Set A) {u : A | orderOf u = n} (b ^ m)
h : ball (b ^ m) (HSMul.hSMul (α := ℝ) (↑m : ℝ) δ) = ball (b ^ m) (m • δ)
⊢ (fun (y : A) ↦ y ^ m) a ∈ ball (b ^ m) (HSMul.hSMul (α := ℝ) (↑m : ℝ) δ)

Tactic:
convert! pow_mem_ball hm hab using 1

Premises used: pow_mem_ball
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
b : A
hab : a ∈ ball b δ
hb : Membership.mem (γ := Set A) {u : A | orderOf u = n} (b ^ m)
⊢ ball (b ^ m) (HSMul.hSMul (α := ℝ) (↑m : ℝ) δ) = ball (b ^ m) (m • δ)

Tactic:
simp only [nsmul_eq_mul, smul_eq_mul]

Premises used: nsmul_eq_mul, smul_eq_mul
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
obtain :
  ∀ (b : A) (hb : orderOf b = n * m) (hab : a ∈ ball b δ), (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)
⊢ (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)

Tactic:
obtain ⟨b, hb : orderOf b = n * m, hab : a ∈ ball b δ⟩ := mem_approxOrderOf_iff.mp ha

Premises used: mem_approxOrderOf_iff, Iff.mp
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hb : orderOf b = n * m
hab : a ∈ ball b δ
rw : orderOf (b ^ m) = n
rw₁ : orderOf b / (orderOf b).gcd m = n
rw₂ : n * m / (n * m).gcd m = n
rw₃ : n * m / m = n
rw₄ rw₅ : n = n
⊢ Membership.mem (γ := Set A) {y : A | orderOf y = n} (b ^ m)

Tactic:
rw [mem_setOf_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]

Premises used: Nat.mul_div_cancel, orderOf_pow', Nat.gcd_mul_left_left, Set.mem_setOf_eq, LT.lt.ne'
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hb : orderOf b = n * m
hab : a ∈ ball b δ
⊢ Membership.mem (γ := Set A) {y : A | orderOf y = n} (b ^ m)

Tactic:
replace hb : b ^ m ∈ {y : A | orderOf y = n} := by
    rw [mem_setOf_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hab : a ∈ ball b δ
hb : Membership.mem (γ := Set A) {y : A | orderOf y = n} (b ^ m)
a₁ : (fun (y : A) ↦ y ^ m) a ∈ ball (b ^ m) ((↑m : ℝ) * δ)
⊢ (fun (y : A) ↦ y ^ m) a ∈ approxOrderOf A n ((↑m : ℝ) * δ)

Tactic:
apply ball_subset_thickening hb (m * δ)

Premises used: HMul.hMul, Metric.ball_subset_thickening, Nat.cast
-- Module: Mathlib.NumberTheory.WellApproximable
Goal:
A : Type u_1
inst : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hab : a ∈ ball b δ
hb : Membership.mem (γ := Set A) {y : A | orderOf y = n} (b ^ m)
⊢ a ^ m ∈ ball (b ^ m) (m • δ)

Tactic:
pow_mem_ball hm hab

Premises used: pow_mem_ball