awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
n : ℕ+
k l : ℕ
h_1 : (k, l) ∈ (↑n : ℕ).divisorsAntidiagonal
h : (k, l).1 * (k, l).2 = (↑n : ℕ) ∧ (↑n : ℕ) ≠ 0
⊢ Eq (α := ℕ)
    (↑(Sigma.snd (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
              ((fun (x : ℕ+ × ℕ+) ↦
                  (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯)
                      (Subtype.mk (p := fun (x_1 : ℕ × ℕ) ↦
                        x_1 ∈
                          (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯) :
                              ℕ).divisorsAntidiagonal)
                        ((↑x.1 : ℕ), (↑x.2 : ℕ)) ⋯) :
                    (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal))
                ((fun (x : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
                    divisorsAntidiagonalFactors (x.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal))
                      (x.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)))
                  (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
                    (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1)))) :
            ↥(↑(Sigma.fst (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
                      ((fun (x : ℕ+ × ℕ+) ↦
                          (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                              (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯)
                              (Subtype.mk (p := fun (x_1 : ℕ × ℕ) ↦
                                x_1 ∈
                                  (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯) :
                                      ℕ).divisorsAntidiagonal)
                                ((↑x.1 : ℕ), (↑x.2 : ℕ)) ⋯) :
                            (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal))
                        ((fun (x : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
                            divisorsAntidiagonalFactors (x.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal))
                              (x.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)))
                          (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
                            (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))))) :
                  ℕ).divisorsAntidiagonal) :
        ℕ × ℕ).1
    (↑(Sigma.snd (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
            (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
              (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))) :
        ℕ × ℕ).1

Tactic:
simp [divisorsAntidiagonalFactors, ← PNat.coe_injective.eq_iff, h.1]

Premises used: divisorsAntidiagonalFactors, PNat.coe_injective, Function.Injective.eq_iff, And.left
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
n : ℕ+
k l : ℕ
h_1 : (k, l) ∈ (↑n : ℕ).divisorsAntidiagonal
h : (k, l).1 * (k, l).2 = (↑n : ℕ) ∧ (↑n : ℕ) ≠ 0
⊢ Eq (α := ℕ)
    (↑(Sigma.snd (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
              ((fun (x : ℕ+ × ℕ+) ↦
                  (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯)
                      (Subtype.mk (p := fun (x_1 : ℕ × ℕ) ↦
                        x_1 ∈
                          (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯) :
                              ℕ).divisorsAntidiagonal)
                        ((↑x.1 : ℕ), (↑x.2 : ℕ)) ⋯) :
                    (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal))
                ((fun (x : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
                    divisorsAntidiagonalFactors (x.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal))
                      (x.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)))
                  (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
                    (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1)))) :
            ↥(↑(Sigma.fst (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
                      ((fun (x : ℕ+ × ℕ+) ↦
                          (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                              (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯)
                              (Subtype.mk (p := fun (x_1 : ℕ × ℕ) ↦
                                x_1 ∈
                                  (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) ((↑x.1 : ℕ) * (↑x.2 : ℕ)) ⋯) :
                                      ℕ).divisorsAntidiagonal)
                                ((↑x.1 : ℕ), (↑x.2 : ℕ)) ⋯) :
                            (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal))
                        ((fun (x : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
                            divisorsAntidiagonalFactors (x.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal))
                              (x.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)))
                          (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
                            (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))))) :
                  ℕ).divisorsAntidiagonal) :
        ℕ × ℕ).2
    (↑(Sigma.snd (β := fun (a : ℕ+) ↦ ↥(↑a : ℕ).divisorsAntidiagonal)
            (Sigma.mk (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal) n
              (Subtype.mk (p := fun (x : ℕ × ℕ) ↦ x ∈ (↑n : ℕ).divisorsAntidiagonal) (k, l) h_1))) :
        ℕ × ℕ).2

Tactic:
simp [divisorsAntidiagonalFactors, ← PNat.coe_injective.eq_iff, h.1]

Premises used: divisorsAntidiagonalFactors, PNat.coe_injective, Function.Injective.eq_iff, And.left
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
x : ℕ+ × ℕ+
⊢ (↑(Sigma.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
          ((sigmaAntidiagonalEquivProd.symm : (a : ℕ+ × ℕ+) → (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) x)) :
      ℕ) =
    (↑x.1 : ℕ) * (↑x.2 : ℕ)

Tactic:
rfl

Premises used: PNat.val, rfl
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
x : ℕ+ × ℕ+
⊢ (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
            ((sigmaAntidiagonalEquivProd.symm : (a : ℕ+ × ℕ+) → (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) x) :
          ↥(↑(Sigma.fst (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                    ((sigmaAntidiagonalEquivProd.symm : (a : ℕ+ × ℕ+) → (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) x)) :
                ℕ).divisorsAntidiagonal) :
      ℕ × ℕ) =
    ((↑x.1 : ℕ), (↑x.2 : ℕ))

Tactic:
rfl

Premises used: PNat.val, rfl
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
simp : Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ HPow.hPow (α := 𝕜) (↑n : 𝕜) k * r ^ n * (1 / (1 - r ^ n))
⊢ Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ HPow.hPow (α := 𝕜) (↑n : 𝕜) k * r ^ n / (1 - r ^ n)

Tactic:
simp only [div_eq_mul_one_div (_ * _ ^ _)]

Premises used: HMul.hMul, HPow.hPow, div_eq_mul_one_div
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖HPow.hPow (α := 𝕜) (↑n : 𝕜) k * r ^ n‖

Tactic:
simpa using summable_norm_pow_mul_geometric_of_norm_lt_one k hr

Premises used: summable_norm_pow_mul_geometric_of_norm_lt_one
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
apply : Tendsto (fun (n : ℕ) ↦ 1 / (1 - r ^ n)) cofinite (𝓝 (1 / HSub.hSub (α := 𝕜) 1 0))
⊢ Summable.{u_1, 0} (α := 𝕜) fun (n : ℕ) ↦ HPow.hPow (α := 𝕜) (↑n : 𝕜) k * r ^ n * (1 / (1 - r ^ n))

Tactic:
apply Summable.mul_tendsto_const (c := 1 / (1 - 0))
    (by simpa using summable_norm_pow_mul_geometric_of_norm_lt_one k hr)

Premises used: Summable.mul_tendsto_const
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ HSub.hSub (α := 𝕜) 1 0 ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Tendsto (fun (n : ℕ) ↦ 1 / (1 - r ^ n)) cofinite (𝓝 (1 / HSub.hSub (α := 𝕜) 1 0))

Tactic:
simpa only [Nat.cofinite_eq_atTop] using
   tendsto_const_nhds.div ((tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).const_sub 1) (by simp)

Premises used: tendsto_const_nhds, Filter.Tendsto.div, Filter.Tendsto.const_sub, Nat.cofinite_eq_atTop, OfNat.ofNat, tendsto_pow_atTop_nhds_zero_of_norm_lt_one
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
hf :
  Summable (α := ℝ) fun (a : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
    ‖HPow.hPow (α := 𝕜) (↑(↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2 : 𝕜) k *
        r ^
          ((↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).1 *
            (↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2)‖
⊢ Summable.{u_1, 0} (α := 𝕜) fun (c : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
    HPow.hPow (α := 𝕜) (↑(↑(c.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2 : 𝕜) k *
      r ^
        ((↑(c.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).1 *
          (↑(c.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2)

Tactic:
apply Summable.of_norm

Premises used: Summable.of_norm
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
a : (x : ℕ+) × ↥(↑x : ℕ).divisorsAntidiagonal
⊢ 0 ≤
    ‖HPow.hPow (α := 𝕜) (↑(↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2 : 𝕜) k *
        r ^
          ((↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).1 *
            (↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2)‖

Tactic:
positivity
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
hf :
  (∀ (x : ℕ+),
      Summable (α := ℝ) fun (y : ↥(↑x : ℕ).divisorsAntidiagonal) ↦
        ‖HPow.hPow (α := 𝕜)
              (↑(↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                          (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                      ℕ × ℕ).2 :
                𝕜)
              k *
            r ^
              HMul.hMul (α := ℕ)
                (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).1
                (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).2‖) ∧
    Summable (α := ℝ) fun (x : ℕ+) ↦
      ∑' (y : ↥(↑x : ℕ).divisorsAntidiagonal),
        ‖HPow.hPow (α := 𝕜)
              (↑(↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                          (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                      ℕ × ℕ).2 :
                𝕜)
              k *
            r ^
              HMul.hMul (α := ℕ)
                (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).1
                (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).2‖
⊢ Summable (α := ℝ) fun (a : (n : ℕ+) × ↥(↑n : ℕ).divisorsAntidiagonal) ↦
    ‖HPow.hPow (α := 𝕜) (↑(↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2 : 𝕜) k *
        r ^
          ((↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).1 *
            (↑(a.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)) : ℕ × ℕ).2)‖

Tactic:
rw [summable_sigma_of_nonneg (fun a ↦ by positivity)]

Premises used: summable_sigma_of_nonneg
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ ∀ (x : ℕ+),
    Summable (α := ℝ) fun (y : ↥(↑x : ℕ).divisorsAntidiagonal) ↦
      ‖HPow.hPow (α := 𝕜)
            (↑(↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).2 :
              𝕜)
            k *
          r ^
            HMul.hMul (α := ℕ)
              (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).1
              (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).2‖

Tactic:
fun n ↦ (hasSum_fintype _).summable

Premises used: PNat.val, Norm.norm, HMul.hMul, Nat.divisorsAntidiagonal, Membership.mem, Subtype, hasSum_fintype, Nat.cast, Prod.fst, HasSum.summable, HPow.hPow, Sigma.mk, Sigma.snd, Subtype.val, Prod.snd, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ ∀ (x : ℕ+),
    Summable (α := ℝ) fun (y : ↥(↑x : ℕ).divisorsAntidiagonal) ↦
      ‖HPow.hPow (α := 𝕜)
            (↑(↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).2 :
              𝕜)
            k *
          r ^
            HMul.hMul (α := ℕ)
              (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).1
              (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).2‖

Tactic:
exact fun n ↦ (hasSum_fintype _).summable

Premises used: hasSum_fintype, HasSum.summable, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
hf :
  Summable (α := ℝ) fun (x : ℕ+) ↦
    ∑ y ∈ (↑x : ℕ).divisorsAntidiagonal.attach,
      norm.{u_1} (E := 𝕜) (↑(↑y : ℕ × ℕ).2 : 𝕜) ^ k * ‖r‖ ^ ((↑y : ℕ × ℕ).1 * (↑y : ℕ × ℕ).2)
⊢ Summable (α := ℝ) fun (x : ℕ+) ↦
    ∑' (y : ↥(↑x : ℕ).divisorsAntidiagonal),
      ‖HPow.hPow (α := 𝕜)
            (↑(↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                        (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                    ℕ × ℕ).2 :
              𝕜)
            k *
          r ^
            HMul.hMul (α := ℕ)
              (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).1
              (↑(Sigma.snd (β := fun (n : ℕ+) ↦ ↥(↑n : ℕ).divisorsAntidiagonal)
                      (Sigma.mk (β := fun (x : ℕ+) ↦ ↥(↑x : ℕ).divisorsAntidiagonal) x y)) :
                  ℕ × ℕ).2‖

Tactic:
simp only [norm_mul, norm_pow, tsum_fintype, Finset.univ_eq_attach]

Premises used: norm_pow, norm_mul, Finset.univ_eq_attach, tsum_fintype
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
x : ↥(↑b : ℕ).divisorsAntidiagonal
h : x ∈ (↑b : ℕ).divisorsAntidiagonal.attach
⊢ 0 ≤ norm.{u_1} (E := 𝕜) (↑(↑x : ℕ × ℕ).2 : 𝕜) ^ k

Tactic:
simp
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
x : ↥(↑b : ℕ).divisorsAntidiagonal
h : x ∈ (↑b : ℕ).divisorsAntidiagonal.attach
⊢ 0 ≤ ‖r‖ ^ ((↑x : ℕ × ℕ).1 * (↑x : ℕ × ℕ).2)

Tactic:
simp
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable (α := ℝ) fun (c : ℕ+) ↦ ‖HPow.hPow (α := 𝕜) (↑(↑c : ℕ) : 𝕜) (k + 1) * r ^ (↑c : ℕ)‖

Tactic:
apply (summable_norm_pow_mul_geometric_of_norm_lt_one (k + 1) hr).subtype

Premises used: Summable.subtype, HAdd.hAdd, summable_norm_pow_mul_geometric_of_norm_lt_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
apply :
  ∀ (b : ℕ+),
    LE.le (α := ℝ)
      (∑ i ∈ (↑b : ℕ).divisorsAntidiagonal.attach,
        norm.{u_1} (E := 𝕜) (↑(↑i : ℕ × ℕ).2 : 𝕜) ^ k * ‖r‖ ^ ((↑i : ℕ × ℕ).1 * (↑i : ℕ × ℕ).2))
      ((fun (c : ℕ+) ↦ ‖HPow.hPow (α := 𝕜) (↑(↑c : ℕ) : 𝕜) (k + 1) * r ^ (↑c : ℕ)‖) b)
⊢ Summable (α := ℝ) fun (x : ℕ+) ↦
    ∑ y ∈ (↑x : ℕ).divisorsAntidiagonal.attach,
      norm.{u_1} (E := 𝕜) (↑(↑y : ℕ × ℕ).2 : 𝕜) ^ k * ‖r‖ ^ ((↑y : ℕ × ℕ).1 * (↑y : ℕ × ℕ).2)

Tactic:
apply Summable.of_nonneg_of_le (f := fun c : ℕ+ ↦ ‖(c : 𝕜) ^ (k + 1) * r ^ (c : ℕ)‖)
      (fun b ↦ Finset.sum_nonneg (fun _ _ ↦ mul_nonneg (by simp) (by simp))) (fun b ↦ ?_)
      (by apply (summable_norm_pow_mul_geometric_of_norm_lt_one (k + 1) hr).subtype)

Premises used: mul_nonneg, Finset.sum_nonneg, Summable.of_nonneg_of_le
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
transitivity :
  LE.le (α := ℝ)
    (∑ i ∈ (↑b : ℕ).divisorsAntidiagonal.attach,
      norm.{u_1} (E := 𝕜) (↑(↑i : ℕ × ℕ).2 : 𝕜) ^ k * ‖r‖ ^ ((↑i : ℕ × ℕ).1 * (↑i : ℕ × ℕ).2))
    (∑ x ∈ (↑b : ℕ).divisors, norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜) ^ k * ‖r ^ (↑b : ℕ)‖)
transitivity₁ :
  LE.le (α := ℝ) (∑ x ∈ (↑b : ℕ).divisors, norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜) ^ k * ‖r ^ (↑b : ℕ)‖)
    ((fun (c : ℕ+) ↦ ‖HPow.hPow (α := 𝕜) (↑(↑c : ℕ) : 𝕜) (k + 1) * r ^ (↑c : ℕ)‖) b)
⊢ LE.le (α := ℝ)
    (∑ i ∈ (↑b : ℕ).divisorsAntidiagonal.attach,
      norm.{u_1} (E := 𝕜) (↑(↑i : ℕ × ℕ).2 : 𝕜) ^ k * ‖r‖ ^ ((↑i : ℕ × ℕ).1 * (↑i : ℕ × ℕ).2))
    ((fun (c : ℕ+) ↦ ‖HPow.hPow (α := 𝕜) (↑(↑c : ℕ) : 𝕜) (k + 1) * r ^ (↑c : ℕ)‖) b)

Tactic:
transitivity ∑ _ ∈ (b : ℕ).divisors, ‖(b : 𝕜)‖ ^ k * ‖r ^ (b : ℕ)‖

Premises used: PNat.val, Nat.cast, Nat.divisors
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
rw :
  LE.le (α := ℝ) (∑ i ∈ (↑b : ℕ).divisors, norm.{u_1} (E := 𝕜) (↑((↑b : ℕ) / i) : 𝕜) ^ k * ‖r‖ ^ (i * ((↑b : ℕ) / i)))
    (∑ x ∈ (↑b : ℕ).divisors, norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜) ^ k * ‖r ^ (↑b : ℕ)‖)
⊢ LE.le (α := ℝ)
    (∑ i ∈ (↑b : ℕ).divisorsAntidiagonal.attach,
      norm.{u_1} (E := 𝕜) (↑(↑i : ℕ × ℕ).2 : 𝕜) ^ k * ‖r‖ ^ ((↑i : ℕ × ℕ).1 * (↑i : ℕ × ℕ).2))
    (∑ x ∈ (↑b : ℕ).divisors, norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜) ^ k * ‖r ^ (↑b : ℕ)‖)

Tactic:
rw [(b : ℕ).divisorsAntidiagonal.sum_attach (fun x ↦ ‖(x.2 : 𝕜)‖ ^ _ * _ ^ (x.1 * x.2)),
          sum_divisorsAntidiagonal ((fun x y ↦ ‖(y : 𝕜)‖ ^ k * _ ^ (x * y)))]

Premises used: PNat.val, Norm.norm, HMul.hMul, Nat.divisorsAntidiagonal, Finset.sum_attach, Nat.cast, Prod.fst, HPow.hPow, Prod.snd, Nat.sum_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
h :
  ∀ (i : ℕ) (hi : i ∈ (↑b : ℕ).divisors),
    norm.{u_1} (E := 𝕜) (↑((↑b : ℕ) / i) : 𝕜) ≤ norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜)
h₁ : ∀ (i : ℕ) (hi : i ∈ (↑b : ℕ).divisors), ‖r‖ ^ (i * ((↑b : ℕ) / i)) ≤ ‖r ^ (↑b : ℕ)‖
⊢ LE.le (α := ℝ) (∑ i ∈ (↑b : ℕ).divisors, norm.{u_1} (E := 𝕜) (↑((↑b : ℕ) / i) : 𝕜) ^ k * ‖r‖ ^ (i * ((↑b : ℕ) / i)))
    (∑ x ∈ (↑b : ℕ).divisors, norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜) ^ k * ‖r ^ (↑b : ℕ)‖)

Tactic:
gcongr with i hi
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
i : ℕ
hi : i ∈ (↑b : ℕ).divisors
⊢ norm.{u_1} (E := 𝕜) (↑((↑b : ℕ) / i) : 𝕜) ≤ norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜)

Tactic:
simpa using le_of_dvd b.2 (div_dvd_of_dvd (dvd_of_mem_divisors hi))

Premises used: Nat.dvd_of_mem_divisors, Nat.div_dvd_of_dvd, Nat.le_of_dvd, Subtype.property
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
i : ℕ
hi : i ∈ (↑b : ℕ).divisors
h : ‖r‖ ^ (i * ((↑b : ℕ) / i)) ≤ ‖r‖ ^ (↑b : ℕ)
h₁ : ‖r‖ ^ ((↑b : ℕ) / i * i) ≤ ‖r‖ ^ (↑b : ℕ)
h₂ h₃ : ‖r‖ ^ (↑b : ℕ) ≤ ‖r‖ ^ (↑b : ℕ)
⊢ ‖r‖ ^ (i * ((↑b : ℕ) / i)) ≤ ‖r ^ (↑b : ℕ)‖

Tactic:
rw [norm_pow, mul_comm, Nat.div_mul_cancel (dvd_of_mem_divisors hi)]

Premises used: Nat.div_mul_cancel, norm_pow, Nat.dvd_of_mem_divisors, mul_comm
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
simp :
  (↑(↑b : ℕ).divisors.card : ℝ) * norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜) ^ k * ‖r‖ ^ (↑b : ℕ) ≤
    norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜) * norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜) ^ k * ‖r‖ ^ (↑b : ℕ)
⊢ LE.le (α := ℝ) (∑ x ∈ (↑b : ℕ).divisors, norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜) ^ k * ‖r ^ (↑b : ℕ)‖)
    ((fun (c : ℕ+) ↦ ‖HPow.hPow (α := 𝕜) (↑(↑c : ℕ) : 𝕜) (k + 1) * r ^ (↑c : ℕ)‖) b)

Tactic:
simp only [norm_pow, Finset.sum_const, nsmul_eq_mul, ← mul_assoc, add_comm k 1, pow_add,
        pow_one, norm_mul]

Premises used: norm_pow, mul_assoc, pow_add, norm_mul, add_comm, pow_one, nsmul_eq_mul, OfNat.ofNat, Finset.sum_const
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
hbc : (↑(↑b : ℕ).divisors.card : ℝ) ≤ norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜)
⊢ (↑(↑b : ℕ).divisors.card : ℝ) * norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜) ^ k * ‖r‖ ^ (↑b : ℕ) ≤
    norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜) * norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜) ^ k * ‖r‖ ^ (↑b : ℕ)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
⊢ (↑(↑b : ℕ).divisors.card : ℝ) ≤ norm.{u_1} (E := 𝕜) (↑(↑b : ℕ) : 𝕜)

Tactic:
simpa using Nat.card_divisors_le_self b

Premises used: PNat.val, Nat.card_divisors_le_self