-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_radius_eq_inv_of_tendsto_ENNReal [NormOneClass E] {r : ℝ≥0∞}
    (hc' : Tendsto (fun n ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)) :
      (ofScalars E c).radius = r⁻¹

Proof state:
case neg.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ x_1, ∃ (_ : x_1 ≥ x), c x_1 = 0
ti : ℕ
hti : ∀ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ⊤
zi : ℕ
hzi : zi ≥ ti
z : c zi = 0
n : ℕ
hmn : zi ≤ n
a : ofScalars E c n = 0
⊢ ofScalars E c (n + 1) = 0

Tactic:
nontriviality E

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ x_1, ∃ (_ : x_1 ≥ x), c x_1 = 0
ti : ℕ
hti : ∀ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ⊤
zi : ℕ
hzi : zi ≥ ti
z : c zi = 0
n : ℕ
hmn : zi ≤ n
a : ofScalars E c n = 0
a✝ : Nontrivial E
⊢ ofScalars E c (n + 1) = 0

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 = 0
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ x_1, ∃ (_ : x_1 ≥ x), c x_1 = 0
ti zi : ℕ
hzi : zi ≥ ti
z : c zi = 0
n : ℕ
hmn : zi ≤ n
a✝ : Nontrivial E
a : c n = 0
hti : c (n + 1) ≠ 0
⊢ ENNReal.ofReal ‖c n.succ‖ ≠ 0 ∧ ENNReal.ofReal ‖c n‖ = 0 ∨ ENNReal.ofReal ‖c n.succ‖ = ⊤ ∧ ENNReal.ofReal ‖c n‖ ≠ ⊤

Tactic:
simp [a, hti]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ¬∀ᶠ (n : ℕ) in atTop, c n ≠ 0
⊢ ∀ᶠ (n : ℕ) in atTop, ofScalars E c n = 0

Tactic:
simp only [eventually_atTop, not_exists, not_forall, Classical.not_imp, not_not] at h ⊢

Result:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ x_1, ∃ (_ : x_1 ≥ x), c x_1 = 0
⊢ ∃ a, ∀ b ≥ a, ofScalars E c b = 0

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

Tactic:
rcases ENNReal.trichotomy r with (hr | hr | hr)

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : r = 0
⊢ (ofScalars E c).radius = r⁻¹

case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : r = ⊤
⊢ (ofScalars E c).radius = r⁻¹

case inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : 0 < r.toReal
⊢ (ofScalars E c).radius = r⁻¹

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 = ⊤
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ⊤)
n : ℕ
hn : ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖ ≠ 0
⊢ ‖c (n + 1)‖ ≠ 0

Tactic:
aesop

Result:
no goals

Proof state:
case neg.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ x_1, ∃ (_ : x_1 ≥ x), c x_1 = 0
ti : ℕ
hti : ∀ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ⊤
⊢ ∃ a, ∀ b ≥ a, ofScalars E c b = 0

Tactic:
obtain ⟨zi, hzi, z⟩ := h ti

Result:
case neg.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ x_1, ∃ (_ : x_1 ≥ x), c x_1 = 0
ti : ℕ
hti : ∀ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ⊤
zi : ℕ
hzi : zi ≥ ti
z : c zi = 0
⊢ ∃ a, ∀ b ≥ a, ofScalars E c b = 0

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 = ⊤
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ⊤)
⊢ Tendsto (fun n => ‖c (n + 1).succ‖ / ‖c (n + 1)‖) atTop atTop

Tactic:
refine tendsto_ofReal_nhds_top.mp (Tendsto.congr' ?_ ((tendsto_add_atTop_iff_nat 1).mpr hc'))

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = ⊤
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ⊤)
⊢ (fun n => ENNReal.ofReal ‖c (n + 1).succ‖ / ENNReal.ofReal ‖c (n + 1)‖) =ᶠ[atTop] fun x =>
    ENNReal.ofReal (‖c (x + 1).succ‖ / ‖c (x + 1)‖)

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 = 0
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ x_1, ∃ (_ : x_1 ≥ x), c x_1 = 0
ti zi : ℕ
hzi : zi ≥ ti
z : c zi = 0
n : ℕ
hmn : zi ≤ n
a✝ : Nontrivial E
a : c n = 0
hti : c (n + 1) ≠ 0
⊢ ∃ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ = ⊤

Tactic:
exact ⟨n, hzi.trans hmn, ENNReal.div_eq_top.mpr (by simp [a, hti])⟩

Result:
no goals

Proof state:
case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = ⊤
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ⊤)
⊢ (ofScalars E c).radius = 0

Tactic:
apply ofScalars_radius_eq_zero_of_tendsto E c ((tendsto_add_atTop_iff_nat 1).mp ?_)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0∞
hr : r = ⊤
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ⊤)
⊢ Tendsto (fun n => ‖c (n + 1).succ‖ / ‖c (n + 1)‖) atTop atTop