awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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) * (1 - x)⁻¹ʳ * (1 - x)⁻¹ʳ = x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2
have noncomm_ring : (1 + -x)⁻¹ʳ * (1 + -x)⁻¹ʳ + -((1 + -x)⁻¹ʳ * (1 + -x)⁻¹ʳ + -(x * ((1 + -x)⁻¹ʳ * (1 + -x)⁻¹ʳ))) =
  x * ((1 + -x)⁻¹ʳ * (1 + -x)⁻¹ʳ)
Tactic: noncomm_ring
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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)⁻¹ʳ = x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2
have calc : HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x)⁻¹ʳ = HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x) * (1 - x)⁻¹ʳ * (1 - x)⁻¹ʳ
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
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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)⁻¹ʳ
⊢ HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x)⁻¹ʳ = x * HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2
have calc₁ : HPow.hPow (β := ℕ) (1 - x)⁻¹ʳ 2 - (1 - x) * (1 - x)⁻¹ʳ * (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
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
r : 𝕜
hr : ‖r‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ (↑n : 𝕜) * r ^ n) (r / HPow.hPow (β := ℕ) (1 - r) 2)
have h : r / HPow.hPow (β := ℕ) (1 - r) 2 = r * HPow.hPow (β := ℕ) (1 - r)⁻¹ʳ 2
Tactic: convert! hasSum_coe_mul_geometric_of_norm_lt_one' hr using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ dist.{u_1} (α := α) (∑ i ∈ Finset.range n, f i) (∑ i ∈ Finset.range (n + 1), f i) ≤ C * r ^ n
have rw : ‖f n‖ ≤ C * r ^ n
Tactic: rw [sum_range_succ, dist_eq_norm, ← norm_neg, neg_sub, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 : ℕ
⊢ ‖∑ x ∈ Finset.range n, f x - a‖ ≤ C * r ^ n / (1 - r)
have rw : dist (∑ x ∈ Finset.range n, f x) a ≤ C * r ^ n / (1 - r)
Tactic: rw [← dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 : ℕ
⊢ dist (∑ x ∈ Finset.range n, f x) a ≤ C * r ^ n / (1 - r)
have ha₁ : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 a)
Tactic: apply dist_le_of_le_geometric_of_tendsto r C hr (dist_partial_sum_le_of_le_geometric hf)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
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
⊢ CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ k ∈ Finset.range (n + 1), u k
have hC : 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
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
⊢ CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ k ∈ Finset.range (n + 1), u k
have this : ∀ 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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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
this : ∀ n ≥ N, u n = v n
apply : ℝ
⊢ CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ k ∈ Finset.range (n + 1), u k
have apply₁ : ∀ (n : ℕ), ‖v n‖ ≤ C * r ^ n
Tactic: apply cauchySeq_sum_of_eventually_eq this
    (NormedAddCommGroup.cauchy_series_of_le_geometric' hr₁ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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
this : ∀ n ≥ N, u n = v n
n : ℕ
⊢ ‖if n < N then 0 else u n‖ ≤ C * r ^ n
have pos : ∀ (H : n < N), norm.{u_1} (E := α) 0 ≤ C * r ^ n
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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
this : ∀ n ≥ N, u n = v n
n : ℕ
pos : ∀ (H : n < N), norm.{u_1} (E := α) 0 ≤ C * r ^ n
⊢ ‖if n < N then 0 else u n‖ ≤ C * r ^ n
have neg : ∀ (H : ¬n < N), ‖u n‖ ≤ C * r ^ n
Tactic: split_ifs with H
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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
this : ∀ n ≥ N, u n = v n
n : ℕ
H : n < N
⊢ norm.{u_1} (E := α) 0 ≤ C * r ^ n
have pos : 0 ≤ C * r ^ n
Tactic: rw [norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
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
this : ∀ n ≥ N, u n = v n
n : ℕ
H : ¬n < N
⊢ ‖u n‖ ≤ C * r ^ n
have H₁ : N ≤ n
Tactic: push Not at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
f : ℕ → α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, f k
⊢ ∃ (C : ℝ), ∀ (n : ℕ), ‖f n‖ ≤ C
have obtain : ∀ (b : ℕ → ℝ),
  (∀ (n : ℕ), 0 ≤ b n) →
    ∀
      (key :
        ∀ (n m N : ℕ),
          N ≤ n → N ≤ m → dist.{u_1} (α := α) (∑ k ∈ Finset.range n, f k) (∑ k ∈ Finset.range m, f k) ≤ b N),
      Tendsto b atTop (𝓝 0) → ∃ (C : ℝ), ∀ (n : ℕ), ‖f n‖ ≤ C
Tactic: obtain ⟨b, ⟨_, key, _⟩⟩ := cauchySeq_iff_le_tendsto_0.mp h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
f : ℕ → α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, f k
b : ℕ → ℝ
left : ∀ (n : ℕ), 0 ≤ b n
key : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist.{u_1} (α := α) (∑ k ∈ Finset.range n, f k) (∑ k ∈ Finset.range m, f k) ≤ b N
right : Tendsto b atTop (𝓝 0)
⊢ ∃ (C : ℝ), ∀ (n : ℕ), ‖f n‖ ≤ C
have refine : ∀ (n : ℕ), ‖f n‖ ≤ b 0
Tactic: refine ⟨b 0, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
⊢ Summable f
have pos : ∀ (hr₀ : 0 ≤ r), Summable f
Tactic: by_cases! hr₀ : 0 ≤ r
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
pos : ∀ (hr₀ : 0 ≤ r), Summable f
⊢ Summable f
have neg : ∀ (hr₀ : r < 0), Summable f
Tactic: by_cases! hr₀ : 0 ≤ r
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : 0 ≤ r
⊢ Summable f
have h₁ : ∃ (a : ℕ), ∀ b ≥ a, ‖f (b + 1)‖ ≤ r * ‖f b‖
Tactic: rw [eventually_atTop] at h
Cleared hypotheses: h, hr₀
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∃ (a : ℕ), ∀ b ≥ a, ‖f (b + 1)‖ ≤ r * ‖f b‖
hr₀ : 0 ≤ r
⊢ Summable f
have pos : ∀ (N : ℕ) (hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖), Summable f
Tactic: rcases h with ⟨N, hN⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable f
have pos : Summable.{u_4, 0} (α := α) fun (n : ℕ) ↦ f (n + N)
Tactic: rw [← @summable_nat_add_iff α _ _ _ _ N]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable.{u_4, 0} (α := α) fun (n : ℕ) ↦ f (n + N)
have pos : ∀ (n : ℕ), ‖f (n + N)‖ ≤ (fun (n : ℕ) ↦ ‖f N‖ * r ^ n) n
Tactic: refine .of_norm_bounded (g := fun n ↦ ‖f N‖ * r ^ n)
      (Summable.mul_left _ <| summable_geometric_of_lt_one hr₀ hr₁) fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
| ‖f N‖ * r ^ n
have rw : r ^ n * ‖f (0 + N)‖
Tactic: rw [mul_comm, ← zero_add N]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ ‖f N‖ * r ^ n
have pos : ‖f (n + N)‖ ≤ r ^ n * ‖f (0 + N)‖
Tactic: conv_rhs => rw [mul_comm, ← zero_add N]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ r ^ n * ‖f (0 + N)‖
have pos : ∀ i < n, (fun (n : ℕ) ↦ ‖f (n + N)‖) (i + 1) ≤ r * (fun (n : ℕ) ↦ ‖f (n + N)‖) i
Tactic: refine le_geom (u := fun n ↦ ‖f (n + N)‖) hr₀ n fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
n i : ℕ
h : i < n
⊢ (fun (n : ℕ) ↦ ‖f (n + N)‖) (i + 1) ≤ r * (fun (n : ℕ) ↦ ‖f (n + N)‖) i
have h : i + 1 + N = i + N + 1
Tactic: convert! hN (i + N) (N.le_add_left i) using 3
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ Summable f
have neg : ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ 0
Tactic: refine .of_norm_bounded_eventually_nat summable_zero ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ 0
have h₁ : ∀ (a : ℕ) (hn : ‖f (a + 1)‖ ≤ r * ‖f a‖), ‖f a‖ ≤ 0
Tactic: filter_upwards [h] with _ hn
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a : ℕ
hn : ‖f (a + 1)‖ ≤ r * ‖f a‖
⊢ ‖f a‖ ≤ 0
have h₁ : ∀ (h : 0 < ‖f a‖), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : NormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
⊢ Summable f
have rcases : ∀ (r : ℝ) (hr₀ : l < r) (hr₁ : r < 1), Summable f
Tactic: rcases exists_between hl₁ with ⟨r, hr₀, hr₁⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : NormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
⊢ Summable f
have refine : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
Tactic: refine summable_of_ratio_norm_eventually_le hr₁ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : NormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
l : ℝ
hl₁ : l < 1
hf : ∀ᶠ (n : ℕ) in atTop, f n ≠ 0
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
r : ℝ
hr₀ : l < r
hr₁ : r < 1
⊢ ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
have h₁ : ∀ (a : ℕ), ‖f (a + 1)‖ / ‖f a‖ ≤ r → ∀ (h₁ : f a ≠ 0), ‖f (a + 1)‖ ≤ r * ‖f a‖
Tactic: filter_upwards [h.eventually_le_const hr₀, hf] with _ _ h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖
⊢ ¬Summable f
have h₁ : ∃ (a : ℕ), ∀ b ≥ a, r * ‖f b‖ ≤ ‖f (b + 1)‖
Tactic: rw [eventually_atTop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
h : ∃ (a : ℕ), ∀ b ≥ a, r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
have rcases : ∀ (N₀ : ℕ) (hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖), ¬Summable f
Tactic: rcases h with ⟨N₀, hN₀⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
have rw : ∀ (hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0) (N₀ : ℕ) (hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖), ¬Summable f
Tactic: rw [frequently_atTop] at hf
Cleared hypotheses: hf, N₀, hN₀
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
have rcases : ∀ (N : ℕ) (hNN₀ : N₀ ≤ N) (hN : ‖f N‖ ≠ 0), ¬Summable f
Tactic: rcases hf N₀ with ⟨N, hNN₀ : N₀ ≤ N, hN⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
⊢ ¬Summable f
have rw : ¬Summable.{u_4, 0} (α := α) fun (n : ℕ) ↦ f (n + N)
Tactic: rw [← @summable_nat_add_iff α _ _ _ _ N]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
⊢ ¬Summable.{u_4, 0} (α := α) fun (n : ℕ) ↦ f (n + N)
have refine : ∀ (h' : Tendsto.{0, u_4} (β := α) (fun (n : ℕ) ↦ f (n + N)) atTop (𝓝 0)),
  Tendsto (α := ℕ) (β := ℝ) ((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) atTop atTop
Tactic: refine mt Summable.tendsto_atTop_zero
    fun h' ↦ not_tendsto_atTop_of_tendsto_nhds (tendsto_norm_zero.comp h') ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto.{0, u_4} (β := α) (fun (n : ℕ) ↦ f (n + N)) atTop (𝓝 0)
⊢ Tendsto (α := ℕ) (β := ℝ) ((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) atTop atTop
have convert_2 : LT.lt (α := ℝ) 0 (((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) 0)
Tactic: convert! tendsto_atTop_of_geom_le _ hr _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto.{0, u_4} (β := α) (fun (n : ℕ) ↦ f (n + N)) atTop (𝓝 0)
convert_2 : LT.lt (α := ℝ) 0 (((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) 0)
⊢ Tendsto (α := ℕ) (β := ℝ) ((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) atTop atTop
have convert_3 : ∀ (n : ℕ),
  r * ((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) n ≤ ((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) (n + 1)
Tactic: convert! tendsto_atTop_of_geom_le _ hr _
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto.{0, u_4} (β := α) (fun (n : ℕ) ↦ f (n + N)) atTop (𝓝 0)
⊢ LT.lt (α := ℝ) 0 (((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) 0)
have convert_2 : Ne (α := ℝ) 0 (((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) 0)
Tactic: refine lt_of_le_of_ne (norm_nonneg _) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto.{0, u_4} (β := α) (fun (n : ℕ) ↦ f (n + N)) atTop (𝓝 0)
h'' : Eq (α := ℝ) 0 (((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) 0)
⊢ False
have hN₁ : r * ‖f N‖ ≤ ‖f (N + 1)‖
Tactic: specialize hN₀ N hNN₀
Cleared hypotheses: hN₀
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0
N₀ N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
h' : Tendsto.{0, u_4} (β := α) (fun (n : ℕ) ↦ f (n + N)) atTop (𝓝 0)
h'' : Eq (α := ℝ) 0 (((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) 0)
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
⊢ False
have h''₁ : 0 = ‖f N‖
Tactic: simp only [comp_apply, zero_add] at h''
Cleared hypotheses: h''
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
have h₁ : ∀ (a : ℕ) (hn : 1 ≤ ‖f (a + 1)‖ / ‖f a‖) (hc : ‖f a‖ = 0), False
Tactic: filter_upwards [h.eventually_const_le hl] with _ hn hc
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a : ℕ
hn : 1 ≤ ‖f (a + 1)‖ / ‖f a‖
hc : ‖f a‖ = 0
⊢ False
have hn₁ : LE.le (α := ℝ) 1 0
Tactic: rw [hc, _root_.div_zero] at hn
Cleared hypotheses: hn, hc
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a : ℕ
hn : LE.le (α := ℝ) 1 0
hc : ‖f a‖ = 0
⊢ False
have linarith : -1 + HSub.hSub (α := ℝ) 1 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
⊢ ¬Summable f
have key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
Tactic: have key : ∀ᶠ n in atTop, ‖f n‖ ≠ 0 := by
    filter_upwards [h.eventually_const_le hl] with _ hn hc
    rw [hc, _root_.div_zero] at hn
    linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
⊢ ¬Summable f
have rcases : ∀ (r : ℝ) (hr₀ : 1 < r) (hr₁ : r < l), ¬Summable f
Tactic: rcases exists_between hl with ⟨r, hr₀, hr₁⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
⊢ ¬Summable f
have refine : ∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖
Tactic: refine not_summable_of_ratio_norm_eventually_ge hr₀ key.frequently ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
⊢ ∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖
have h₁ : ∀ (a : ℕ), r ≤ ‖f (a + 1)‖ / ‖f a‖ → ∀ (h₁ : ‖f a‖ ≠ 0), r * ‖f a‖ ≤ ‖f (a + 1)‖
Tactic: filter_upwards [h.eventually_const_le hr₁, key] with _ _ h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
⊢ Summable.{u_1, 0} (α := α) fun (n : ℕ) ↦ f n * z ^ n
have hw : 0 < ‖w‖
Tactic: have hw : 0 < ‖w‖ := (norm_nonneg z).trans_lt hz
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
⊢ Summable.{u_1, 0} (α := α) fun (n : ℕ) ↦ f n * z ^ n
have obtain : ∀ (C : ℝ) (hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C), Summable.{u_1, 0} (α := α) fun (n : ℕ) ↦ f n * z ^ n
Tactic: obtain ⟨C, hC⟩ := exists_norm_le_of_cauchySeq h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
⊢ Summable.{u_1, 0} (α := α) fun (n : ℕ) ↦ f n * z ^ n
have rw : CauchySeq.{u_1, 0} (α := α) fun (s : Finset ℕ) ↦ ∑ b ∈ s, f b * z ^ b
Tactic: rw [summable_iff_cauchySeq_finset]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
⊢ CauchySeq.{u_1, 0} (α := α) fun (s : Finset ℕ) ↦ ∑ b ∈ s, f b * z ^ b
have refine : ∀ (n : ℕ), ‖f n * z ^ n‖ ≤ C * (‖z‖ / ‖w‖) ^ n
Tactic: refine cauchySeq_finset_of_geometric_bound (r := ‖z‖ / ‖w‖) (C := C) ((div_lt_one hw).mpr hz)
    (fun n ↦ ?_)