-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem not_summable_of_ratio_test_tendsto_gt_one {α : Type*} [SeminormedAddCommGroup α]
    {f : ℕ → α} {l : ℝ} (hl : 1 < l) (h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)) :
    ¬Summable f

Proof state:
α : Type u_2
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
⊢ ¬Summable f

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

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

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

Tactic:
filter_upwards [h.eventually_const_le hr₁, key] with _ _ h₁

Result:
case h
α : Type u_2
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
a✝¹ : ℕ
a✝ : r ≤ ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖
h₁ : ‖f a✝¹‖ ≠ 0
⊢ r * ‖f a✝¹‖ ≤ ‖f (a✝¹ + 1)‖

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

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

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

Proof state:
α : Type u_2
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0

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

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

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

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

Result:
case h
α : Type u_2
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a✝ : ℕ
hn : 1 ≤ 0
hc : ‖f a✝‖ = 0
⊢ False

Proof state:
case h
α : Type u_2
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
a✝¹ : ℕ
a✝ : r ≤ ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖
h₁ : ‖f a✝¹‖ ≠ 0
⊢ r * ‖f a✝¹‖ ≤ ‖f (a✝¹ + 1)‖

Tactic:
rwa [← le_div_iff₀ (lt_of_le_of_ne (norm_nonneg _) h₁.symm)]

Result:
no goals

Proof state:
case h
α : Type u_2
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a✝ : ℕ
hn : 1 ≤ 0
hc : ‖f a✝‖ = 0
⊢ False

Tactic:
linarith

Result:
no goals

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

Tactic:
refine not_summable_of_ratio_norm_eventually_ge hr₀ key.frequently ?_

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