-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_radius_eq_zero_of_tendsto [NormOneClass E]
    (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop) : (ofScalars E c).radius = 0

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ¬‖‖ofScalars E c x‖ * ↑r ^ x‖ ≠ 0
n : ℕ
hc' : ¬‖‖ofScalars E c n‖ * ↑r ^ n‖ ≠ 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖

Tactic:
rw [ofScalars_norm, norm_mul, norm_norm, not_ne_iff, mul_eq_zero] at hc'

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ¬‖‖ofScalars E c x‖ * ↑r ^ x‖ ≠ 0
n : ℕ
hc' : ‖c n‖ = 0 ∨ ‖↑r ^ n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖

Proof state:
case h.hd
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 0 < ‖c n‖

Tactic:
refine Ne.lt_of_le (fun hr' ↦ Not.elim ?_ hc) (norm_nonneg _)

Result:
case h.hd
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
hr' : 0 = ‖c n‖
⊢ ¬2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ¬‖‖ofScalars E c x‖ * ↑r ^ x‖ ≠ 0
n : ℕ
hc' : ‖c n‖ = 0 ∨ ‖↑r ^ n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖

Tactic:
cases hc' <;> aesop

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
this : (ofScalars E c).radius ≤ 0
⊢ (ofScalars E c).radius = 0

Tactic:
aesop

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
⊢ ↑r ≤ 0

Tactic:
rw [← coe_zero, coe_le_coe]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
⊢ r ≤ 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
⊢ (ofScalars E c).radius = 0

Tactic:
suffices (ofScalars E c).radius ≤ 0 by aesop

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
⊢ (ofScalars E c).radius ≤ 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : Summable fun n => ‖ofScalars E c n‖ * ↑r ^ n
⊢ r ≤ 0

Tactic:
contrapose! this

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
⊢ ¬Summable fun n => ‖ofScalars E c n‖ * ↑r ^ n

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ¬‖‖ofScalars E c x‖ * ↑r ^ x‖ ≠ 0
⊢ (fun x => 0) =ᶠ[atTop] fun n => ‖c n.succ‖ / ‖c n‖

Tactic:
filter_upwards [hc] with n hc'

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ¬‖‖ofScalars E c x‖ * ↑r ^ x‖ ≠ 0
n : ℕ
hc' : ¬‖‖ofScalars E c n‖ * ↑r ^ n‖ ≠ 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖

Proof state:
case h.hb
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 0 < ↑r ^ (n + 1)

Tactic:
aesop

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
⊢ ¬Summable fun n => ‖ofScalars E c n‖ * ↑r ^ n

Tactic:
apply not_summable_of_ratio_norm_eventually_ge one_lt_two

Result:
case hf
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
⊢ ∃ᶠ (n : ℕ) in atTop, ‖‖ofScalars E c n‖ * ↑r ^ n‖ ≠ 0

case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
⊢ ∀ᶠ (n : ℕ) in atTop, 2 * ‖‖ofScalars E c n‖ * ↑r ^ n‖ ≤ ‖‖ofScalars E c (n + 1)‖ * ↑r ^ (n + 1)‖

Proof state:
case hf
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ¬∃ᶠ (n : ℕ) in atTop, ‖‖ofScalars E c n‖ * ↑r ^ n‖ ≠ 0
⊢ Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)

Tactic:
rw [not_frequently] at hc

Result:
case hf
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ¬‖‖ofScalars E c x‖ * ↑r ^ x‖ ≠ 0
⊢ Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)

Proof state:
case h.e'_3.h.e'_6.ha
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ ↑r ^ n ≠ 0

Tactic:
aesop

Result:
no goals