-- 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 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 = ⊤

Tactic:
apply ofScalars_radius_eq_top_of_tendsto E c h ?_

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
⊢ Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)

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∞
hc' : Tendsto (fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : r = ⊤
⊢ (ofScalars E c).radius = r⁻¹

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

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

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 (𝓝 ⊤)
⊢ (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)‖)

Tactic:
filter_upwards [hc'.eventually_ne top_ne_zero] with n hn

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 = ⊤
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
⊢ ENNReal.ofReal ‖c (n + 1).succ‖ / ENNReal.ofReal ‖c (n + 1)‖ = ENNReal.ofReal (‖c (n + 1).succ‖ / ‖c (n + 1)‖)

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.toNNReal)

Tactic:
simp_rw [ENNReal.coe_toNNReal_eq_toReal]

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
⊢ Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r.toReal)

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
⊢ (ENNReal.toReal ∘ fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) =ᶠ[atTop] fun n => ‖c n.succ‖ / ‖c n‖

Tactic:
filter_upwards [hc'.eventually_ne hr'.1, hc'.eventually_ne hr'.2]

Result:
case h
𝕜 : 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
⊢ ∀ (a : ℕ),
    ENNReal.ofReal ‖c a.succ‖ / ENNReal.ofReal ‖c a‖ ≠ 0 →
      ENNReal.ofReal ‖c a.succ‖ / ENNReal.ofReal ‖c a‖ ≠ ⊤ →
        (ENNReal.toReal ∘ fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) a = ‖c a.succ‖ / ‖c a‖

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 = 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‖

Tactic:
simp

Result:
no goals

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
⊢ ∃ a, ∀ b ≥ a, ofScalars E c b = 0

Tactic:
refine ⟨zi, Nat.le_induction (ofScalars_eq_zero_of_scalar_zero E z) fun n hmn a ↦ ?_⟩

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
n : ℕ
hmn : zi ≤ n
a : ofScalars E c n = 0
⊢ ofScalars E c (n + 1) = 0

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

Tactic:
simp [ENNReal.coe_inv hr'', ENNReal.coe_toNNReal (toReal_ne_zero.mp hr.ne.symm).2]

Result:
no goals

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∞
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
⊢ ∀ (a : ℕ),
    ENNReal.ofReal ‖c a.succ‖ / ENNReal.ofReal ‖c a‖ ≠ 0 →
      ENNReal.ofReal ‖c a.succ‖ / ENNReal.ofReal ‖c a‖ ≠ ⊤ →
        (ENNReal.toReal ∘ fun n => ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) a = ‖c a.succ‖ / ‖c a‖

Tactic:
simp

Result:
no goals