-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem summable_of_ratio_norm_eventually_le {α : Type*} [SeminormedAddCommGroup α]
    [CompleteSpace α] {f : ℕ → α} {r : ℝ} (hr₁ : r < 1)
    (h : ∀ᶠ n in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖) : Summable f

Proof state:
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
⊢ Summable f

Tactic:
by_cases hr₀ : 0 ≤ r

Result:
case pos
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : 0 ≤ r
⊢ Summable f

case neg
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : ¬0 ≤ r
⊢ Summable f

Proof state:
case pos.intro
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : 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:
refine le_geom (u := fun n ↦ ‖f (n + N)‖) hr₀ n fun i _ ↦ ?_

Result:
case pos.intro
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
n i : ℕ
x✝ : i < n
⊢ (fun n => ‖f (n + N)‖) (i + 1) ≤ r * (fun n => ‖f (n + N)‖) i

Proof state:
case pos.intro
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable f

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

Result:
case pos.intro
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable fun n => f (n + N)

Proof state:
case neg
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ Summable f

Tactic:
refine .of_norm_bounded_eventually_nat 0 summable_zero ?_

Result:
case neg
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : 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 i

Proof state:
case pos
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∃ a, ∀ b ≥ a, ‖f (b + 1)‖ ≤ r * ‖f b‖
hr₀ : 0 ≤ r
⊢ Summable f

Tactic:
rcases h with ⟨N, hN⟩

Result:
case pos.intro
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable f

Proof state:
case h
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : 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 : 0 a✝ < ‖f a✝‖
⊢ False

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

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : 0 ≤ r
⊢ Summable f

Tactic:
rw [eventually_atTop] at h

Result:
case pos
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∃ a, ∀ b ≥ a, ‖f (b + 1)‖ ≤ r * ‖f b‖
hr₀ : 0 ≤ r
⊢ Summable f

Proof state:
case h.e'_3.h.e'_3.h.e'_1
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
n i : ℕ
x✝ : i < n
⊢ i + 1 + N = i + N + 1

Tactic:
ac_rfl

Result:
no goals

Proof state:
case neg
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : ¬0 ≤ r
⊢ Summable f

Tactic:
push_neg at hr₀

Result:
case neg
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ Summable f

Proof state:
case pos.intro
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : 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

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

Result:
case pos.intro
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : 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)‖

Proof state:
case pos.intro
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
n i : ℕ
x✝ : i < n
⊢ (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

Result:
case h.e'_3.h.e'_3.h.e'_1
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
n i : ℕ
x✝ : i < n
⊢ i + 1 + N = i + N + 1

Proof state:
case neg
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : 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 i

Tactic:
filter_upwards [h] with _ hn

Result:
case h
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : 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 a✝

Proof state:
case pos.intro
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ (fun n => ‖f N‖ * r ^ n) n

Tactic:
simp only

Result:
case pos.intro
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : 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

Proof state:
case h
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : 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 a✝

Tactic:
by_contra! h

Result:
case h
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : 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 : 0 a✝ < ‖f a✝‖
⊢ False

Proof state:
case pos.intro
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable fun n => f (n + N)

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

Result:
case pos.intro
α : Type u_2
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ b ≥ N, ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ (fun n => ‖f N‖ * r ^ n) n