-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem not_summable_of_ratio_norm_eventually_ge {α : Type*} [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

Proof state:
case intro
α : Type u_2
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

Tactic:
rcases hf N₀ with ⟨N, hNN₀ : N₀ ≤ N, hN⟩

Result:
case intro.intro.intro
α : Type u_2
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

Proof state:
case h.e'_4.h.e'_3.h.e'_1
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ i + 1 + N = i + N + 1

Tactic:
ac_rfl

Result:
no goals

Proof state:
case intro.intro.intro.convert_2
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
h'' : 0 = ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
⊢ False

Tactic:
specialize hN₀ N hNN₀

Result:
case intro.intro.intro.convert_2
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
h'' : 0 = ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
⊢ False

Proof state:
case intro.intro.intro.convert_3
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ r * ((fun a => ‖a‖) ∘ fun n => f (n + N)) i ≤ ((fun a => ‖a‖) ∘ fun n => f (n + N)) (i + 1)

Tactic:
dsimp only [comp_apply]

Result:
case intro.intro.intro.convert_3
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ r * ‖f (i + N)‖ ≤ ‖f (i + 1 + N)‖

Proof state:
case intro.intro.intro.convert_3
α : Type u_2
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 (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:
intro i

Result:
case intro.intro.intro.convert_3
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
i : ℕ
⊢ r * ((fun a => ‖a‖) ∘ fun n => f (n + N)) i ≤ ((fun a => ‖a‖) ∘ fun n => f (n + N)) (i + 1)

Proof state:
case intro.intro.intro
α : Type u_2
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

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

Result:
case intro.intro.intro
α : Type u_2
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 fun n => f (n + N)

Proof state:
case intro.intro.intro.convert_2
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
⊢ 0 ≠ ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0

Tactic:
intro h''

Result:
case intro.intro.intro.convert_2
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
h'' : 0 = ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
⊢ False

Proof state:
case intro.intro.intro.convert_2
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
⊢ 0 < ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0

Tactic:
refine lt_of_le_of_ne (norm_nonneg _) ?_

Result:
case intro.intro.intro.convert_2
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
⊢ 0 ≠ ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0

Proof state:
case intro.intro.intro.convert_2
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
h'' : 0 = ‖f N‖
⊢ False

Tactic:
exact hN h''.symm

Result:
no goals

Proof state:
case intro
α : Type u_2
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

Tactic:
rw [frequently_atTop] at hf

Result:
case intro
α : Type u_2
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

Proof state:
case intro.intro.intro.convert_2
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
h'' : 0 = ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
⊢ False

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

Result:
case intro.intro.intro.convert_2
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
hN₀ : r * ‖f N‖ ≤ ‖f (N + 1)‖
h'' : 0 = ‖f N‖
⊢ False

Proof state:
case intro.intro.intro
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
⊢ Tendsto ((fun a => ‖a‖) ∘ fun n => f (n + N)) atTop atTop

Tactic:
convert tendsto_atTop_of_geom_le _ hr _

Result:
case intro.intro.intro.convert_2
α : Type u_2
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 (fun n => f (n + N)) atTop (𝓝 0)
⊢ 0 < ((fun a => ‖a‖) ∘ fun n => f (n + N)) 0

case intro.intro.intro.convert_3
α : Type u_2
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 (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)