awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
P : ℕ[X] := Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1))
n : ℕ
mP : P.Monic
dP : P.natDegree = k
A : (n + k).descFactorial k = Polynomial.eval n P
conv_lhs :
  Polynomial.eval n
      (HPow.hPow (α := ℕ[X]) X k +
        ∑ i ∈ Finset.range k,
          HMul.hMul (α := ℕ[X]) ((C : (a : ℕ) → ℕ[X]) (P.coeff i) : ℕ[X]) (HPow.hPow (α := ℕ[X]) X i)) =
    n ^ k + ∑ i ∈ Finset.range k, (fun (i : ℕ) ↦ P.coeff i) i * n ^ i
⊢ (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun (i : ℕ) ↦ P.coeff i) i * n ^ i

Tactic:
conv_lhs => rw [A, mP.as_sum, dP]

Premises used: Polynomial.Monic.as_sum
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
P : ℕ[X] := Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1))
n : ℕ
mP : P.Monic
dP : P.natDegree = k
A : (n + k).descFactorial k = Polynomial.eval n P
⊢ Polynomial.eval n
      (HPow.hPow (α := ℕ[X]) X k +
        ∑ i ∈ Finset.range k,
          HMul.hMul (α := ℕ[X]) ((C : (a : ℕ) → ℕ[X]) (P.coeff i) : ℕ[X]) (HPow.hPow (α := ℕ[X]) X i)) =
    n ^ k + ∑ i ∈ Finset.range k, (fun (i : ℕ) ↦ P.coeff i) i * n ^ i

Tactic:
simp [eval_finsetSum]

Premises used: Polynomial.eval_finsetSum
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
obtain :
  ∀ (a : ℕ → ℕ) (ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i),
    Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n

Tactic:
obtain ⟨a, ha⟩ : ∃ (a : ℕ → ℕ), ∀ n, (n + k).descFactorial k
      = n ^ k + ∑ i ∈ range k, a i * n ^ i := by
    let P : Polynomial ℕ := (ascPochhammer ℕ k).comp (Polynomial.X + C 1)
    refine ⟨fun i ↦ P.coeff i, fun n ↦ ?_⟩
    have mP : Monic P := Monic.comp_X_add_C (monic_ascPochhammer ℕ k) _
    have dP : P.natDegree = k := by
      simp only [P, natDegree_comp, ascPochhammer_natDegree, mul_one, natDegree_X_add_C]
    have A : (n + k).descFactorial k = P.eval n := by
      have : n + 1 + k - 1 = n + k := by lia
      simp [P, ascPochhammer_nat_eq_descFactorial, this]
    conv_lhs => rw [A, mP.as_sum, dP]
    simp [eval_finsetSum]
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
apply :
  Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑b : R) i * r ^ b
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n

Tactic:
apply (summable_descFactorial_mul_geometric_of_norm_lt_one k hr).sub

Premises used: Summable.sub, summable_descFactorial_mul_geometric_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
apply :
  ∀ (i : ℕ) (hi : i ∈ Finset.range k),
    Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ (↑(a i) : R) * HPow.hPow (α := R) (↑b : R) i * r ^ b
⊢ Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑b : R) i * r ^ b

Tactic:
apply summable_sum (fun i hi ↦ ?_)

Premises used: summable_sum
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
i : ℕ
hi : i ∈ Finset.range k
simp_rw : Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ (↑(a i) : R) * (HPow.hPow (α := R) (↑b : R) i * r ^ b)
⊢ Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ (↑(a i) : R) * HPow.hPow (α := R) (↑b : R) i * r ^ b

Tactic:
simp_rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
i : ℕ
hi : i ∈ Finset.range k
⊢ i < k

Tactic:
simp only [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
i : ℕ
hi : i < k
⊢ Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ (↑(a i) : R) * (HPow.hPow (α := R) (↑b : R) i * r ^ b)

Tactic:
(hk _ hi).mul_left _

Premises used: Summable.mul_left
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
i : ℕ
hi : i < k
⊢ Summable.{u_4, 0} (α := R) fun (b : ℕ) ↦ (↑(a i) : R) * (HPow.hPow (α := R) (↑b : R) i * r ^ b)

Tactic:
exact (hk _ hi).mul_left _

Premises used: Summable.mul_left
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n

Tactic:
have : Summable (fun n ↦ (n + k).descFactorial k * r ^ n
      - ∑ i ∈ range k, a i * n ^ (i : ℕ) * r ^ n) := by
    apply (summable_descFactorial_mul_geometric_of_norm_lt_one k hr).sub
    apply summable_sum (fun i hi ↦ ?_)
    simp_rw [mul_assoc]
    simp only [Finset.mem_range] at hi
    exact (hk _ hi).mul_left _
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this :
  Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n

Tactic:
this
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this :
  Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
h :
  Eq.{u_4 + 1} (α := ℕ → R) (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
⊢ Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n

Tactic:
convert! this using 1
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this :
  Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
h :
  ∀ (n : ℕ),
    HPow.hPow (α := R) (↑n : R) k * r ^ n =
      (↑((n + k).descFactorial k) : R) * r ^ n -
        ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
⊢ Eq.{u_4 + 1} (α := ℕ → R) (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r ^ n) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n

Tactic:
ext n
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
k_1 : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
this :
  Summable.{u_4, 0} (α := R) fun (n : ℕ) ↦
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n
n : ℕ
⊢ HPow.hPow (α := R) (↑n : R) k * r ^ n =
    (↑((n + k).descFactorial k) : R) * r ^ n -
      ∑ i ∈ Finset.range k, (↑(a i) : R) * HPow.hPow (α := R) (↑n : R) i * r ^ n

Tactic:
simp [ha n, add_mul, sum_mul]

Premises used: add_mul, Finset.sum_mul
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ (↑((n + 1).choose 1) : R) * x ^ n) ((1 - x)⁻¹ʳ ^ HAdd.hAdd (α := ℕ) 1 1)

Tactic:
hasSum_choose_mul_geometric_of_norm_lt_one' 1 h

Premises used: hasSum_choose_mul_geometric_of_norm_lt_one', OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
h₁ : ∀ (n : ℕ), HAdd.hAdd (α := R) (↑n : R) 1 = (↑((n + 1).choose 1) : R)
⊢ HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)

Tactic:
convert! hasSum_choose_mul_geometric_of_norm_lt_one' 1 h with n

Premises used: hasSum_choose_mul_geometric_of_norm_lt_one', OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
n : ℕ
⊢ HAdd.hAdd (α := R) (↑n : R) 1 = (↑((n + 1).choose 1) : R)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)

Tactic:
have A : HasSum (fun (n : ℕ) ↦ (n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2) := by
    convert! hasSum_choose_mul_geometric_of_norm_lt_one' 1 h with n
    simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
⊢ HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ

Tactic:
have B : HasSum (fun (n : ℕ) ↦ x ^ n) ((1 - x)⁻¹ʳ) := hasSum_geom_series_inverse x h
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ HasSum (fun (b : ℕ) ↦ HAdd.hAdd (α := R) (↑b : R) 1 * x ^ b - x ^ b) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x)⁻¹ʳ)

Tactic:
A.sub B

Premises used: HasSum.sub
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
h₁ :
  Eq.{u_4 + 1} (α := ℕ → R) (fun (n : ℕ) ↦ (↑n : R) * x ^ n) fun (b : ℕ) ↦ HAdd.hAdd (α := R) (↑b : R) 1 * x ^ b - x ^ b
h₂ : x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 = HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x)⁻¹ʳ
⊢ HasSum (fun (n : ℕ) ↦ (↑n : R) * x ^ n) (x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)

Tactic:
convert! A.sub B using 1

Premises used: HasSum.sub
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
h₁ : ∀ (n : ℕ), (↑n : R) * x ^ n = HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n - x ^ n
⊢ Eq.{u_4 + 1} (α := ℕ → R) (fun (n : ℕ) ↦ (↑n : R) * x ^ n) fun (b : ℕ) ↦ HAdd.hAdd (α := R) (↑b : R) 1 * x ^ b - x ^ b

Tactic:
ext n
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
n : ℕ
⊢ (↑n : R) * x ^ n = HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n - x ^ n

Tactic:
simp [add_mul]

Premises used: add_mul
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
h₁ : HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x)⁻¹ʳ = x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2
⊢ x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 = HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x)⁻¹ʳ

Tactic:
symm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x)⁻¹ʳ = HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x) * (1 - x)⁻¹ʳ * (1 - x)⁻¹ʳ

Tactic:
simp [Ring.mul_inverse_cancel (1 - x) (isUnit_one_sub_of_norm_lt_one h)]

Premises used: HSub.hSub, Ring.mul_inverse_cancel, OfNat.ofNat, isUnit_one_sub_of_norm_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
noncomm_ring noncomm_ring₁ noncomm_ring₂ noncomm_ring₃ :
  (1 + -x)⁻¹ʳ * (1 + -x)⁻¹ʳ + -((1 + -x)⁻¹ʳ * (1 + -x)⁻¹ʳ + -(x * ((1 + -x)⁻¹ʳ * (1 + -x)⁻¹ʳ))) =
    x * ((1 + -x)⁻¹ʳ * (1 + -x)⁻¹ʳ)
⊢ HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x) * (1 - x)⁻¹ʳ * (1 - x)⁻¹ʳ = x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2

Tactic:
noncomm_ring
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_4
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun (n : ℕ) ↦ HAdd.hAdd (α := R) (↑n : R) 1 * x ^ n) (HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2)
B : HasSum (fun (n : ℕ) ↦ x ^ n) (1 - x)⁻¹ʳ
calc :
  HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x)⁻¹ʳ = HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x) * (1 - x)⁻¹ʳ * (1 - x)⁻¹ʳ
calc₁ : HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x) * (1 - x)⁻¹ʳ * (1 - x)⁻¹ʳ = x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2
⊢ HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x)⁻¹ʳ = x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2

Tactic:
calc (1 - x)⁻¹ʳ ^ 2 - (1 - x)⁻¹ʳ
    _ = (1 - x)⁻¹ʳ ^ 2 - ((1 - x) * (1 - x)⁻¹ʳ) * (1 - x)⁻¹ʳ := by
      simp [Ring.mul_inverse_cancel (1 - x) (isUnit_one_sub_of_norm_lt_one h)]
    _ = x * (1 - x)⁻¹ʳ ^ 2 := by noncomm_ring

Premises used: HMul.hMul, HSub.hSub, Ring.inverse, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ ∑' (n : ℕ), (↑n : 𝕜) * r ^ n = r * HPow.hPow (β := ℕ) (1 - r)⁻¹ʳ 2

Tactic:
(hasSum_coe_mul_geometric_of_norm_lt_one' hr).tsum_eq

Premises used: hasSum_coe_mul_geometric_of_norm_lt_one', HasSum.tsum_eq
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ (↑n : 𝕜) * r ^ n) (r * HPow.hPow (β := ℕ) (1 - r)⁻¹ʳ 2)

Tactic:
hasSum_coe_mul_geometric_of_norm_lt_one' hr

Premises used: hasSum_coe_mul_geometric_of_norm_lt_one'
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
r : 𝕜
hr : ‖r‖ < 1
h : r / HPow.hPow (β := ℕ) (1 - r) 2 = r * HPow.hPow (β := ℕ) (1 - r)⁻¹ʳ 2
⊢ HasSum (fun (n : ℕ) ↦ (↑n : 𝕜) * r ^ n) (r / HPow.hPow (β := ℕ) (1 - r) 2)

Tactic:
convert! hasSum_coe_mul_geometric_of_norm_lt_one' hr using 1

Premises used: hasSum_coe_mul_geometric_of_norm_lt_one'
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ r / HPow.hPow (β := ℕ) (1 - r) 2 = r * HPow.hPow (β := ℕ) (1 - r)⁻¹ʳ 2

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ ∑' (n : ℕ), (↑n : 𝕜) * r ^ n = r / HPow.hPow (β := ℕ) (1 - r) 2

Tactic:
(hasSum_coe_mul_geometric_of_norm_lt_one hr).tsum_eq

Premises used: hasSum_coe_mul_geometric_of_norm_lt_one, HasSum.tsum_eq
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
C r : ℝ
hr : r < 1
u : ℕ → α
h : ∀ (n : ℕ), ‖u n - u (n + 1)‖ ≤ C * r ^ n
⊢ ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ C * r ^ n

Tactic:
simpa [dist_eq_norm] using h

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
rw : ‖f n‖ ≤ C * r ^ n
⊢ dist.{u_1} (α := α) (∑ i ∈ Finset.range n, f i) (∑ i ∈ Finset.range (n + 1), f i) ≤ C * r ^ n

Tactic:
rw [sum_range_succ, dist_eq_norm, ← norm_neg, neg_sub, add_sub_cancel_left]

Premises used: neg_sub, dist_eq_norm, add_sub_cancel_left, norm_neg, Finset.sum_range_succ
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ ‖f n‖ ≤ C * r ^ n

Tactic:
hf n
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ ‖f n‖ ≤ C * r ^ n

Tactic:
exact hf n
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
⊢ CauchySeq.{u_1, 0} (α := α) fun (s : Finset ℕ) ↦ ∑ x ∈ s, f x

Tactic:
cauchySeq_finset_of_norm_bounded
    (aux_hasSum_of_le_geometric hr (dist_partial_sum_le_of_le_geometric hf)).summable hf

Premises used: aux_hasSum_of_le_geometric, HasSum.summable, dist_partial_sum_le_of_le_geometric, cauchySeq_finset_of_norm_bounded
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
rw : dist (∑ x ∈ Finset.range n, f x) a ≤ C * r ^ n / (1 - r)
⊢ ‖∑ x ∈ Finset.range n, f x - a‖ ≤ C * r ^ n / (1 - r)

Tactic:
rw [← dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
ha₁ : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 a)
⊢ dist (∑ x ∈ Finset.range n, f x) a ≤ C * r ^ n / (1 - r)

Tactic:
apply dist_le_of_le_geometric_of_tendsto r C hr (dist_partial_sum_le_of_le_geometric hf)

Premises used: dist_partial_sum_le_of_le_geometric, dist_le_of_le_geometric_of_tendsto
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 a)

Tactic:
ha.tendsto_sum_nat

Premises used: HasSum.tendsto_sum_nat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 a)

Tactic:
exact ha.tendsto_sum_nat

Premises used: HasSum.tendsto_sum_nat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
u : ℕ → α
n : ℕ
⊢ dist.{u_1} (α := α) (∑ k ∈ Finset.range (n + 1), u k) (∑ k ∈ Finset.range n, u k) = ‖u n‖

Tactic:
simp [dist_eq_norm, sum_range_succ]

Premises used: dist_eq_norm, Finset.sum_range_succ
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
u : ℕ → α
n : ℕ
⊢ dist.{u_1} (α := α) (∑ k ∈ Finset.range n, u k) (∑ k ∈ Finset.range (n + 1), u k) = ‖u n‖

Tactic:
simp [dist_eq_norm', sum_range_succ]

Premises used: dist_eq_norm', Finset.sum_range_succ
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
r : ℝ
hr : r < 1
h : ∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n
⊢ ∀ (n : ℕ), dist.{u_1} (α := α) (∑ k ∈ Finset.range n, u k) (∑ k ∈ Finset.range (n + 1), u k) ≤ C * r ^ n

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
r : ℝ
hr : r < 1
h : ∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n
⊢ CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ k ∈ Finset.range (n + 1), u k

Tactic:
(cauchy_series_of_le_geometric hr h).comp_tendsto <| tendsto_add_atTop_nat 1

Premises used: Multiset.sum, Multiset.foldr, Filter.tendsto_add_atTop_nat, CauchySeq.comp_tendsto, OfNat.ofNat, cauchy_series_of_le_geometric, Finset.sum
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun (n : ℕ) ↦ if n < N then 0 else u n
⊢ 0 ≤ C

Tactic:
have hC : 0 ≤ C :=
    (mul_nonneg_iff_of_pos_right <| pow_pos hr₀ N).mp ((norm_nonneg _).trans <| h N <| le_refl N)
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun (n : ℕ) ↦ if n < N then 0 else u n
hC : 0 ≤ C
n : ℕ
hn : n ≥ N
⊢ u n = v n

Tactic:
simp [v, if_neg (not_lt.mpr hn)]

Premises used: Iff.mpr, not_lt, if_neg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun (n : ℕ) ↦ if n < N then 0 else u n
hC : 0 ≤ C
⊢ ∀ n ≥ N, u n = v n

Tactic:
have : ∀ n ≥ N, u n = v n := by
    intro n hn
    simp [v, if_neg (not_lt.mpr hn)]