-- 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 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
hr' : r ≠ 0 ∧ r ≠ ⊤
hr'' : r.toNNReal ≠ 0
⊢ (ofScalars E c).radius = r⁻¹

Tactic:
convert ofScalars_radius_eq_inv_of_tendsto E c hr'' ?_

Result:
case h.e'_3
𝕜 : 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
hr' : r ≠ 0 ∧ r ≠ ⊤
hr'' : r.toNNReal ≠ 0
⊢ r⁻¹ = ↑r.toNNReal⁻¹

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
hr' : r ≠ 0 ∧ r ≠ ⊤
hr'' : r.toNNReal ≠ 0
⊢ Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r.toNNReal)

Proof state:
case inl
𝕜 : 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)
⊢ (ofScalars E c).radius = ⊤

Tactic:
by_cases h : (∀ᶠ (n : ℕ) in atTop, c n ≠ 0)

Result:
case pos
𝕜 : 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
⊢ (ofScalars E c).radius = ⊤

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
⊢ (ofScalars E c).radius = ⊤

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 : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
⊢ Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)

Tactic:
refine Tendsto.congr' ?_ <| (tendsto_toReal zero_ne_top).comp 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 = 0
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
⊢ (ENNReal.toReal ∘ fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) =ᶠ[atTop] fun n => ‖c n.succ‖ / ‖c n‖

Proof state:
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
hr' : r ≠ 0 ∧ r ≠ ⊤
hr'' : r.toNNReal ≠ 0
⊢ Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r.toReal)

Tactic:
refine Tendsto.congr' ?_ <| (tendsto_toReal hr'.2).comp hc'

Result:
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
hr' : r ≠ 0 ∧ r ≠ ⊤
hr'' : r.toNNReal ≠ 0
⊢ (ENNReal.toReal ∘ fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) =ᶠ[atTop] fun n => ‖c n.succ‖ / ‖c n‖

Proof state:
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⁻¹

Tactic:
have hr' := toReal_ne_zero.mp hr.ne.symm

Result:
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
hr' : r ≠ 0 ∧ r ≠ ⊤
⊢ (ofScalars E c).radius = r⁻¹

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 : ∀ (x : ℕ), ∃ x_1, ∃ (_ : x_1 ≥ x), c x_1 = 0
⊢ ∃ a, ∀ b ≥ a, ofScalars E c b = 0

Tactic:
obtain ⟨ti, hti⟩ := eventually_atTop.mp (hc'.eventually_ne zero_ne_top)

Result:
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

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
⊢ (ofScalars E c).radius = ⊤

Tactic:
apply (ofScalars E c).radius_eq_top_of_eventually_eq_zero

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 : ¬∀ᶠ (n : ℕ) in atTop, c n ≠ 0
⊢ ∀ᶠ (n : ℕ) in atTop, ofScalars E c n = 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 : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
⊢ (ENNReal.toReal ∘ fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) =ᶠ[atTop] fun n => ‖c n.succ‖ / ‖c n‖

Tactic:
filter_upwards [h]

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 = 0
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
⊢ ∀ (a : ℕ),
    c a ≠ 0 → (ENNReal.toReal ∘ fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) a = ‖c a.succ‖ / ‖c a‖

Proof state:
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⁻¹

Tactic:
simp_rw [hr, inv_zero] at hc' ⊢

Result:
case inl
𝕜 : 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)
⊢ (ofScalars E c).radius = ⊤