awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : r = 0
inl :
  ∀ (hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)),
    radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = ∞
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹

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

Premises used: ENNReal.inv_zero
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
pos : ∀ (h : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0), radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = ∞
neg : ∀ (h : ¬∀ᶠ (n : ℕ) in atTop, c n ≠ 0), radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = ∞
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = ∞

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

Premises used: Filter.Eventually, Ne, Filter.atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
apply : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = ∞

Tactic:
apply ofScalars_radius_eq_top_of_tendsto E c h ?_

Premises used: FormalMultilinearSeries.ofScalars_radius_eq_top_of_tendsto
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (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:
Tendsto.congr' ?_ <| (tendsto_toReal zero_ne_top).comp hc'

Premises used: ENNReal.tendsto_toReal, ENNReal.zero_ne_top, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
refine :
  (ENNReal.toReal ∘ fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) =ᶠ[atTop] fun (n : ℕ) ↦
    ‖c n.succ‖ / ‖c n‖
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)

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

Premises used: ENNReal.tendsto_toReal, ENNReal.zero_ne_top, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
h₁ :
  ∀ (a : ℕ),
    c a ≠ 0 → (ENNReal.toReal ∘ fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) a = ‖c a.succ‖ / ‖c a‖
⊢ (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]
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (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
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ¬∀ᶠ (n : ℕ) in atTop, c n ≠ 0
neg : ∀ᶠ (n : ℕ) in atTop, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = ∞

Tactic:
apply (ofScalars E c).radius_eq_top_of_eventually_eq_zero

Premises used: FormalMultilinearSeries.ofScalars, FormalMultilinearSeries.radius_eq_top_of_eventually_eq_zero
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ¬∀ᶠ (n : ℕ) in atTop, c n ≠ 0
neg :
  ∀ (h : ∀ (x : ℕ), ∃ (x_1 : ℕ) (_ : x_1 ≥ x), c x_1 = 0),
    ∃ (a : ℕ), ∀ b ≥ a, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin b) ↦ E) E) (ofScalars E c b) 0
⊢ ∀ᶠ (n : ℕ) in atTop, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0

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

Premises used: Classical.not_not, not_exists, Filter.eventually_atTop, Classical.not_forall
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ (x : ℕ), ∃ (x_1 : ℕ) (_ : x_1 ≥ x), c x_1 = 0
neg :
  ∀ (ti : ℕ) (hti : ∀ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ ≠ ∞),
    ∃ (a : ℕ), ∀ b ≥ a, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin b) ↦ E) E) (ofScalars E c b) 0
⊢ ∃ (a : ℕ), ∀ b ≥ a, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin b) ↦ E) E) (ofScalars E c b) 0

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

Premises used: Filter.Tendsto.eventually_ne, ENNReal.zero_ne_top, Iff.mp, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (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‖ ≠ ∞
neg :
  ∀ (zi : ℕ) (hzi : zi ≥ ti) (z : c zi = 0),
    ∃ (a : ℕ), ∀ b ≥ a, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin b) ↦ E) E) (ofScalars E c b) 0
⊢ ∃ (a : ℕ), ∀ b ≥ a, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin b) ↦ E) E) (ofScalars E c b) 0

Tactic:
obtain ⟨zi, hzi, z⟩ := h ti
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (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, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin b) ↦ E) E) (ofScalars E c b) 0

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

Premises used: Nat.le_induction, Exists.intro
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (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
neg :
  ∀ (n : ℕ) (hmn : zi ≤ n) (a : Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0),
    Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (ofScalars E c (n + 1)) 0
⊢ ∃ (a : ℕ), ∀ b ≥ a, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin b) ↦ E) E) (ofScalars E c b) 0

Tactic:
refine ⟨zi, Nat.le_induction (ofScalars_eq_zero_of_scalar_zero E z) fun n hmn a ↦ ?_⟩
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (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 : Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0
⊢ Nontrivial E

Tactic:
nontriviality E
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (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 : Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0
h_1 : Nontrivial E
simp : ∀ (a : c n = 0), c (n + 1) = 0
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (ofScalars E c (n + 1)) 0

Tactic:
simp only [ofScalars_eq_zero] at a ⊢

Premises used: FormalMultilinearSeries.ofScalars_eq_zero
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (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
h_1 : Nontrivial E
a : c n = 0
contrapose! : ∀ (hti : c (n + 1) ≠ 0), ∃ b ≥ ti, ENNReal.ofReal ‖c b.succ‖ / ENNReal.ofReal ‖c b‖ = ∞
⊢ c (n + 1) = 0

Tactic:
contrapose! hti
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (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
h_1 : 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]
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = 0
hc' : Tendsto (β := ℝ≥0∞) (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
h_1 : 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])⟩
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : r = ∞
inr :
  ∀ (hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ∞)),
    radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = 0
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹

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

Premises used: ENNReal.inv_top
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = ∞
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ∞)
apply : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c (n + 1).succ‖ / ‖c (n + 1)‖) atTop atTop
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = 0

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

Premises used: FormalMultilinearSeries.ofScalars_radius_eq_zero_of_tendsto, Iff.mp, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = ∞
hc' : Tendsto (β := ℝ≥0∞) (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:
tendsto_ofReal_nhds_top.mp (Tendsto.congr' ?_ ((tendsto_add_atTop_iff_nat 1).mpr hc'))

Premises used: Iff.mpr, Iff.mp, Filter.tendsto_add_atTop_iff_nat, Filter.Tendsto.congr', OfNat.ofNat, ENNReal.tendsto_ofReal_nhds_top
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = ∞
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ∞)
refine :
  EventuallyEq (β := ℝ≥0∞) atTop (fun (n : ℕ) ↦ ENNReal.ofReal ‖c (n + 1).succ‖ / ENNReal.ofReal ‖c (n + 1)‖)
    fun (x : ℕ) ↦ ENNReal.ofReal (‖c (x + 1).succ‖ / ‖c (x + 1)‖)
⊢ 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'))

Premises used: Iff.mpr, Iff.mp, Filter.tendsto_add_atTop_iff_nat, Filter.Tendsto.congr', OfNat.ofNat, ENNReal.tendsto_ofReal_nhds_top
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = ∞
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ∞)
h :
  ∀ (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)‖)
⊢ EventuallyEq (β := ℝ≥0∞) atTop (fun (n : ℕ) ↦ ENNReal.ofReal ‖c (n + 1).succ‖ / ENNReal.ofReal ‖c (n + 1)‖)
    fun (x : ℕ) ↦ ENNReal.ofReal (‖c (x + 1).succ‖ / ‖c (x + 1)‖)

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

Premises used: Filter.Tendsto.eventually_ne, ENNReal.top_ne_zero
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = ∞
hc' : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 ∞)
n : ℕ
hn : ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖ ≠ 0
apply : ‖c (n + 1)‖ ≠ 0
⊢ ENNReal.ofReal ‖c (n + 1).succ‖ / ENNReal.ofReal ‖c (n + 1)‖ = ENNReal.ofReal (‖c (n + 1).succ‖ / ‖c (n + 1)‖)

Tactic:
apply (ofReal_div_of_pos (Ne.lt_of_le (Ne.symm ?_) (norm_nonneg _))).symm

Premises used: ENNReal.ofReal_div_of_pos, Ne.symm, Eq.symm, Ne.lt_of_le, norm_nonneg
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hr : r = ∞
hc' : Tendsto (β := ℝ≥0∞) (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:
simp_all
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : NormOneClass E
r : ℝ≥0∞
hc' : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : 0 < r.toReal
⊢ r ≠ 0 ∧ r ≠ ∞

Tactic:
have hr' := toReal_ne_zero.mp hr.ne.symm
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : 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 ≠ ∞
⊢ r.toNNReal ≠ 0

Tactic:
have hr'' := toNNReal_ne_zero.mpr hr'
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : 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
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = (↑r.toNNReal⁻¹ : ℝ≥0∞)

Tactic:
ofScalars_radius_eq_inv_of_tendsto E c hr'' ?_

Premises used: FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : 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
h : r⁻¹ = (↑r.toNNReal⁻¹ : ℝ≥0∞)
inr : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r.toNNReal : ℝ))
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹

Tactic:
convert! ofScalars_radius_eq_inv_of_tendsto E c hr'' ?_

Premises used: FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : 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⁻¹ : ℝ≥0∞)

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

Premises used: ENNReal.coe_toNNReal, ENNReal.coe_inv, Ne.symm, And.right, Iff.mp, ENNReal.toReal_ne_zero, LT.lt.ne
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : 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:
Tendsto.congr' ?_ <| (tendsto_toReal hr'.2).comp hc'

Premises used: ENNReal.tendsto_toReal, And.right, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : 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
inr :
  (ENNReal.toReal ∘ fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) =ᶠ[atTop] fun (n : ℕ) ↦
    ‖c n.succ‖ / ‖c n‖
⊢ Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r.toReal)

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

Premises used: ENNReal.tendsto_toReal, And.right, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : 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
h :
  ∀ (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‖
⊢ (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]

Premises used: Filter.Tendsto.eventually_ne, And.right, And.left
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst_3 : 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
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : ¬AnalyticAt 𝕜 f z₀
⊢ analyticOrderAt f z₀ = 0

Tactic:
dif_neg hf

Premises used: dif_neg, analyticOrderAt
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : ¬AnalyticAt 𝕜 f z₀
⊢ analyticOrderNatAt f z₀ = 0

Tactic:
simp [analyticOrderNatAt, hf]

Premises used: analyticOrderNatAt
-- Module: Mathlib.Analysis.Analytic.Order
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : analyticOrderAt f z₀ ≠ ⊤
⊢ (↑(analyticOrderNatAt f z₀) : ℕ∞) = analyticOrderAt f z₀

Tactic:
ENat.coe_toNat hf

Premises used: analyticOrderNatAt, ENat.coe_toNat