awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : ∀ n ≥ N, u n = v n
apply : ℝ
apply₁ : ∀ (n : ℕ), ‖v n‖ ≤ C * r ^ n
⊢ CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ k ∈ Finset.range (n + 1), u k

Tactic:
apply cauchySeq_sum_of_eventually_eq this
    (NormedAddCommGroup.cauchy_series_of_le_geometric' hr₁ _)

Premises used: NormedAddCommGroup.cauchy_series_of_le_geometric', cauchySeq_sum_of_eventually_eq
-- 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
this : ∀ n ≥ N, u n = v n
⊢ ℝ

Tactic:
exact C
-- 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
this : ∀ n ≥ N, u n = v n
n : ℕ
simp : ‖if n < N then 0 else u n‖ ≤ C * r ^ n
⊢ ‖v n‖ ≤ C * r ^ n

Tactic:
simp only [v]
-- 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
this : ∀ n ≥ N, u n = v n
n : ℕ
pos : ∀ (H : n < N), norm.{u_1} (E := α) 0 ≤ C * r ^ n
neg : ∀ (H : ¬n < N), ‖u n‖ ≤ C * r ^ n
⊢ ‖if n < N then 0 else u n‖ ≤ C * r ^ n

Tactic:
split_ifs with H
-- 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
this : ∀ n ≥ N, u n = v n
n : ℕ
H : n < N
pos : 0 ≤ C * r ^ n
⊢ norm.{u_1} (E := α) 0 ≤ C * r ^ n

Tactic:
rw [norm_zero]

Premises used: norm_zero
-- 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
this : ∀ n ≥ N, u n = v n
n : ℕ
H : n < N
⊢ 0 ≤ C * r ^ n

Tactic:
mul_nonneg hC (pow_nonneg hr₀.le _)

Premises used: mul_nonneg, pow_nonneg, LT.lt.le
-- 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
this : ∀ n ≥ N, u n = v n
n : ℕ
H : n < N
⊢ 0 ≤ C * r ^ n

Tactic:
exact mul_nonneg hC (pow_nonneg hr₀.le _)

Premises used: mul_nonneg, pow_nonneg, LT.lt.le
-- 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
this : ∀ n ≥ N, u n = v n
n : ℕ
H : ¬n < N
⊢ N ≤ n

Tactic:
push Not at H

Premises used: Not
-- 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
this : ∀ n ≥ N, u n = v n
n : ℕ
H : N ≤ n
⊢ ‖u n‖ ≤ C * r ^ n

Tactic:
h _ H
-- 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
this : ∀ n ≥ N, u n = v n
n : ℕ
H : N ≤ n
⊢ ‖u n‖ ≤ C * r ^ n

Tactic:
exact h _ H
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : SeminormedAddCommGroup α
f : ℕ → α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, f k
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
⊢ ∃ (C : ℝ), ∀ (n : ℕ), ‖f n‖ ≤ C

Tactic:
obtain ⟨b, ⟨_, key, _⟩⟩ := cauchySeq_iff_le_tendsto_0.mp h

Premises used: cauchySeq_iff_le_tendsto_0, Iff.mp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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

Tactic:
⟨b 0, fun n ↦ ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
refine : ∀ (n : ℕ), ‖f n‖ ≤ b 0
⊢ ∃ (C : ℝ), ∀ (n : ℕ), ‖f n‖ ≤ C

Tactic:
refine ⟨b 0, fun n ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
n : ℕ
⊢ ‖f n‖ ≤ b 0

Tactic:
simpa only [dist_partial_sum'] using key n (n + 1) 0 zero_le zero_le

Premises used: zero_le, HAdd.hAdd, dist_partial_sum', OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
neg : ∀ (hr₀ : r < 0), Summable f
⊢ Summable f

Tactic:
by_cases! hr₀ : 0 ≤ r
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
⊢ ∃ (a : ℕ), ∀ b ≥ a, ‖f (b + 1)‖ ≤ r * ‖f b‖

Tactic:
rw [eventually_atTop] at h

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
h₁ : ∃ (a : ℕ), ∀ b ≥ a, ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ 0 ≤ r

Tactic:
rw [eventually_atTop] at h

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
pos : ∀ (N : ℕ) (hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖), Summable f
⊢ Summable f

Tactic:
rcases h with ⟨N, hN⟩
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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‖
pos : Summable.{u_4, 0} (α := α) fun (n : ℕ) ↦ f (n + N)
⊢ Summable f

Tactic:
rw [← @summable_nat_add_iff α _ _ _ _ N]

Premises used: summable_nat_add_iff
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)

Tactic:
.of_norm_bounded (g := fun n ↦ ‖f N‖ * r ^ n)
      (Summable.mul_left _ <| summable_geometric_of_lt_one hr₀ hr₁) fun n ↦ ?_

Premises used: Summable.mul_left, Summable.of_norm_bounded, summable_geometric_of_lt_one
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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‖
pos : ∀ (n : ℕ), ‖f (n + N)‖ ≤ (fun (n : ℕ) ↦ ‖f N‖ * r ^ n) n
⊢ Summable.{u_4, 0} (α := α) fun (n : ℕ) ↦ f (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 ↦ ?_
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 : ℕ
rw : r ^ n * ‖f (0 + N)‖
| ‖f N‖ * r ^ n

Tactic:
rw [mul_comm, ← zero_add N]

Premises used: zero_add, mul_comm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 : ℕ
pos : ‖f (n + N)‖ ≤ r ^ n * ‖f (0 + N)‖
⊢ ‖f (n + N)‖ ≤ ‖f N‖ * r ^ n

Tactic:
conv_rhs => rw [mul_comm, ← zero_add N]

Premises used: zero_add, mul_comm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)‖

Tactic:
le_geom (u := fun n ↦ ‖f (n + N)‖) hr₀ n fun i _ ↦ ?_

Premises used: le_geom
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 : ℕ
pos : ∀ i < n, (fun (n : ℕ) ↦ ‖f (n + N)‖) (i + 1) ≤ r * (fun (n : ℕ) ↦ ‖f (n + N)‖) i
⊢ ‖f (n + N)‖ ≤ r ^ n * ‖f (0 + N)‖

Tactic:
refine le_geom (u := fun n ↦ ‖f (n + N)‖) hr₀ n fun i _ ↦ ?_

Premises used: le_geom
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
⊢ ‖f (i + N + 1)‖ ≤ r * ‖f (i + N)‖

Tactic:
hN (i + N) (N.le_add_left i)

Premises used: Nat.le_add_left, HAdd.hAdd
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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_1 : i < n
h : i + 1 + N = i + N + 1
⊢ (fun (n : ℕ) ↦ ‖f (n + N)‖) (i + 1) ≤ r * (fun (n : ℕ) ↦ ‖f (n + N)‖) i

Tactic:
convert! hN (i + N) (N.le_add_left i) using 3

Premises used: Nat.le_add_left, HAdd.hAdd
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
⊢ i + 1 + N = i + N + 1

Tactic:
ac_rfl
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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

Tactic:
.of_norm_bounded_eventually_nat summable_zero ?_

Premises used: summable_zero, Summable.of_norm_bounded_eventually_nat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
neg : ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ 0
⊢ Summable f

Tactic:
refine .of_norm_bounded_eventually_nat summable_zero ?_
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
h₁ : ∀ (a : ℕ) (hn : ‖f (a + 1)‖ ≤ r * ‖f a‖), ‖f a‖ ≤ 0
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ 0

Tactic:
filter_upwards [h] with _ hn
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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‖
h₁ : ∀ (h : 0 < ‖f a‖), False
⊢ ‖f a‖ ≤ 0

Tactic:
by_contra! h
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h_1 : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a : ℕ
hn : ‖f (a + 1)‖ ≤ r * ‖f a‖
h : 0 < ‖f a‖
⊢ False

Tactic:
not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn <| mul_neg_of_neg_of_pos hr₀ h)

Premises used: Iff.mpr, mul_neg_of_neg_of_pos, lt_of_le_of_lt, not_lt, norm_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
inst_1 : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h_1 : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a : ℕ
hn : ‖f (a + 1)‖ ≤ r * ‖f a‖
h : 0 < ‖f a‖
⊢ False

Tactic:
exact not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn <| mul_neg_of_neg_of_pos hr₀ h)

Premises used: Iff.mpr, mul_neg_of_neg_of_pos, lt_of_le_of_lt, not_lt, norm_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
rcases : ∀ (r : ℝ) (hr₀ : l < r) (hr₁ : r < 1), Summable f
⊢ Summable f

Tactic:
rcases exists_between hl₁ with ⟨r, hr₀, hr₁⟩

Premises used: exists_between
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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

Tactic:
summable_of_ratio_norm_eventually_le hr₁ ?_

Premises used: summable_of_ratio_norm_eventually_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
refine : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
⊢ Summable f

Tactic:
refine summable_of_ratio_norm_eventually_le hr₁ ?_

Premises used: summable_of_ratio_norm_eventually_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
a : ℕ
h₁ : ‖f (a + 1)‖ / ‖f a‖ ≤ r → f a ≠ 0 → ‖f (a + 1)‖ ≤ r * ‖f a‖
⊢ ‖f (a + 1)‖ / ‖f a‖ ≤ r → f a ≠ 0 → ‖f (a + 1)‖ ≤ r * ‖f a‖

Tactic:
_
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
h₁ : ∀ (a : ℕ), ‖f (a + 1)‖ / ‖f a‖ ≤ r → ∀ (h₁ : f a ≠ 0), ‖f (a + 1)‖ ≤ r * ‖f a‖
⊢ ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖

Tactic:
filter_upwards [h.eventually_le_const hr₀, hf] with _ _ h₁

Premises used: Filter.Tendsto.eventually_le_const
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
a : ℕ
h_1 : ‖f (a + 1)‖ / ‖f a‖ ≤ r
h₁ : f a ≠ 0
h₂ h₃ h₄ h₅ : ‖f (a + 1)‖ / ‖f a‖ ≤ r
⊢ ‖f (a + 1)‖ ≤ r * ‖f a‖

Tactic:
rwa [← div_le_iff₀ (norm_pos_iff.mpr h₁)]

Premises used: Iff.mpr, div_le_iff₀, norm_pos_iff
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)‖
⊢ ∃ (a : ℕ), ∀ b ≥ a, r * ‖f b‖ ≤ ‖f (b + 1)‖

Tactic:
rw [eventually_atTop] at h

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)‖
rcases : ∀ (N₀ : ℕ) (hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖), ¬Summable f
⊢ ¬Summable f

Tactic:
rcases h with ⟨N₀, hN₀⟩
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)‖
rw : ∀ (hf : ∀ (a : ℕ), ∃ b ≥ a, ‖f b‖ ≠ 0) (N₀ : ℕ) (hN₀ : ∀ b ≥ N₀, r * ‖f b‖ ≤ ‖f (b + 1)‖), ¬Summable f
⊢ ¬Summable f

Tactic:
rw [frequently_atTop] at hf

Premises used: Filter.frequently_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)‖
rcases : ∀ (N : ℕ) (hNN₀ : N₀ ≤ N) (hN : ‖f N‖ ≠ 0), ¬Summable f
⊢ ¬Summable f

Tactic:
rcases hf N₀ with ⟨N, hNN₀ : N₀ ≤ N, hN⟩
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
rw : ¬Summable.{u_4, 0} (α := α) fun (n : ℕ) ↦ f (n + N)
⊢ ¬Summable f

Tactic:
rw [← @summable_nat_add_iff α _ _ _ _ N]

Premises used: summable_nat_add_iff
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)

Tactic:
mt Summable.tendsto_atTop_zero
    fun h' ↦ not_tendsto_atTop_of_tendsto_nhds (tendsto_norm_zero.comp h') ?_

Premises used: Summable.tendsto_atTop_zero, mt, not_tendsto_atTop_of_tendsto_nhds, Filter.Tendsto.comp, tendsto_norm_zero
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
refine :
  ∀ (h' : Tendsto.{0, u_4} (β := α) (fun (n : ℕ) ↦ f (n + N)) atTop (𝓝 0)),
    Tendsto (α := ℕ) (β := ℝ) ((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) atTop atTop
⊢ ¬Summable.{u_4, 0} (α := α) fun (n : ℕ) ↦ f (n + N)

Tactic:
refine mt Summable.tendsto_atTop_zero
    fun h' ↦ not_tendsto_atTop_of_tendsto_nhds (tendsto_norm_zero.comp h') ?_

Premises used: Summable.tendsto_atTop_zero, mt, not_tendsto_atTop_of_tendsto_nhds, Filter.Tendsto.comp, tendsto_norm_zero
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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

Tactic:
tendsto_atTop_of_geom_le _ hr _

Premises used: tendsto_atTop_of_geom_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
convert_3 :
  ∀ (n : ℕ),
    r * ((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) n ≤ ((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) (n + 1)
⊢ Tendsto (α := ℕ) (β := ℝ) ((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) atTop atTop

Tactic:
convert! tendsto_atTop_of_geom_le _ hr _

Premises used: tendsto_atTop_of_geom_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)

Tactic:
lt_of_le_of_ne (norm_nonneg _) ?_

Premises used: norm_nonneg, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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 : Ne (α := ℝ) 0 (((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) 0)
⊢ LT.lt (α := ℝ) 0 (((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) 0)

Tactic:
refine lt_of_le_of_ne (norm_nonneg _) ?_

Premises used: norm_nonneg, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
⊢ r * ‖f N‖ ≤ ‖f (N + 1)‖

Tactic:
specialize hN₀ N hNN₀
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)‖
⊢ 0 = ‖f N‖

Tactic:
simp only [comp_apply, zero_add] at h''

Premises used: zero_add, Function.comp_apply
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
h'' : 0 = ‖f N‖
⊢ False

Tactic:
hN h''.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
h'' : 0 = ‖f N‖
⊢ False

Tactic:
exact hN h''.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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)
⊢ ∀ (n : ℕ),
    r * ((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) n ≤ ((fun (a : α) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ f (n + N)) (n + 1)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
h₁ : ∀ (a : ℕ) (hn : 1 ≤ ‖f (a + 1)‖ / ‖f a‖) (hc : ‖f a‖ = 0), False
⊢ ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0

Tactic:
filter_upwards [h.eventually_const_le hl] with _ hn hc

Premises used: Filter.Tendsto.eventually_const_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
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
⊢ LE.le (α := ℝ) 1 0

Tactic:
rw [hc, _root_.div_zero] at hn

Premises used: div_zero