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 : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
neg : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖ / ‖‖c n‖ * (↑r' : ℝ) ^ n‖) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖‖ / ‖‖‖c n‖ * (↑r' : ℝ) ^ n‖‖) atTop (𝓝 0)

Tactic:
simp only [norm_norm]

Premises used: norm_norm
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖ / ‖‖c n‖ * (↑r' : ℝ) ^ n‖) atTop (𝓝 0)

Tactic:
mul_zero (_ : ℝ) ▸ tendsto_succ_norm_div_norm _ hrz (NNReal.coe_zero ▸ hc')

Premises used: Eq.rec, MulZeroClass.mul_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 : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖ / ‖‖c n‖ * (↑r' : ℝ) ^ n‖) atTop (𝓝 0)

Tactic:
exact mul_zero (_ : ℝ) ▸ tendsto_succ_norm_div_norm _ hrz (NNReal.coe_zero ▸ hc')
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
⊢ ∀ (x : ℕ), c x ≠ 0 → ‖‖c x‖ * (↑r' : ℝ) ^ x‖ ≠ 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 : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
h :
  ∀ (n : ℕ) (hn : n ≠ 0),
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n‖ ≤
      ‖‖c n‖ * (↑r' : ℝ) ^ n‖
⊢ ∀ᶠ (i : ℕ) in cofinite,
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) E) (ofScalars E c i) * (↑r' : ℝ) ^ i‖ ≤
      (fun (n : ℕ) ↦ ‖‖c n‖ * (↑r' : ℝ) ^ n‖) i

Tactic:
filter_upwards [eventually_cofinite_ne 0] with n hn

Premises used: Filter.eventually_cofinite_ne, 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 : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
n : ℕ
hn : n ≠ 0
h :
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n ≤
    ‖c n‖ * (↑r' : ℝ) ^ n
⊢ ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n‖ ≤
    ‖‖c n‖ * (↑r' : ℝ) ^ n‖

Tactic:
simp only [norm_mul, norm_norm, norm_pow, NNReal.norm_eq]

Premises used: norm_pow, norm_mul, norm_norm, NNReal.norm_eq
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
n : ℕ
hn : n ≠ 0
h : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) ≤ ‖c n‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n ≤
    ‖c n‖ * (↑r' : ℝ) ^ n

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
n : ℕ
hn : n ≠ 0
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) ≤ ‖c n‖

Tactic:
ofScalars_norm_le E c n (Nat.pos_iff_ne_zero.mpr hn)

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, FormalMultilinearSeries.ofScalars_norm_le
-- Module: Mathlib.Analysis.Analytic.OfScalars
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
n : ℕ
hn : n ≠ 0
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) ≤ ‖c n‖

Tactic:
exact ofScalars_norm_le E c n (Nat.pos_iff_ne_zero.mpr hn)

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, FormalMultilinearSeries.ofScalars_norm_le
-- 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
hc : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
this : 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) = 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
hc : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
suffices : 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) = 0

Tactic:
suffices (ofScalars E c).radius ≤ 0 by 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
hc : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) ≤ 0

Tactic:
le_of_forall_nnreal_lt (fun r hr ↦ ?_)

Premises used: ENNReal.le_of_forall_nnreal_lt
-- 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
hc : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
refine :
  ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)), (↑r : ℝ≥0∞) ≤ 0
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) ≤ 0

Tactic:
refine le_of_forall_nnreal_lt (fun r hr ↦ ?_)

Premises used: ENNReal.le_of_forall_nnreal_lt
-- 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
hc : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
rw : r ≤ 0
⊢ (↑r : ℝ≥0∞) ≤ 0

Tactic:
rw [← coe_zero, coe_le_coe]

Premises used: ENNReal.coe_le_coe, ENNReal.coe_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
hc : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n

Tactic:
have := FormalMultilinearSeries.summable_norm_mul_pow _ 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
hc : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this :
  Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n
contrapose! :
  ∀ (this : 0 < r),
    ¬Summable (α := ℝ) fun (n : ℕ) ↦
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n
⊢ r ≤ 0

Tactic:
contrapose! this
-- 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
hc : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
⊢ LT.lt (α := ℝ) 1 2

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
hc : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
refine_1 :
  ∃ᶠ (n : ℕ) in atTop,
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n‖ ≠ 0
refine_2 :
  ∀ᶠ (n : ℕ) in atTop,
    2 * ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n‖ ≤
      ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (ofScalars E c (n + 1)) *
          (↑r : ℝ) ^ (n + 1)‖
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n

Tactic:
refine not_summable_of_ratio_norm_eventually_ge (r := 2) (by simp) ?_ ?_

Premises used: not_summable_of_ratio_norm_eventually_ge
-- 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
hc : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
refine_1 :
  ∀
    (hc :
      ∀ᶠ (x : ℕ) in atTop,
        ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin x) ↦ E) E) (ofScalars E c x) * (↑r : ℝ) ^ x‖ = 0),
    ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
⊢ ∃ᶠ (n : ℕ) in atTop,
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n‖ ≠ 0

Tactic:
contrapose! hc
-- 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∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
hc :
  ∀ᶠ (x : ℕ) in atTop,
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin x) ↦ E) E) (ofScalars E c x) * (↑r : ℝ) ^ x‖ = 0
refine_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
⊢ ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop

Tactic:
apply not_tendsto_atTop_of_tendsto_nhds (a := 0)

Premises used: not_tendsto_atTop_of_tendsto_nhds
-- 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∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
hc :
  ∀ᶠ (x : ℕ) in atTop,
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin x) ↦ E) E) (ofScalars E c x) * (↑r : ℝ) ^ x‖ = 0
apply : EventuallyEq (β := ℝ) atTop (fun (x : ℕ) ↦ 0) fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)

Tactic:
apply Tendsto.congr' ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, 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∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
hc :
  ∀ᶠ (x : ℕ) in atTop,
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin x) ↦ E) E) (ofScalars E c x) * (↑r : ℝ) ^ x‖ = 0
h :
  ∀ (n : ℕ)
    (hc' : ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n‖ = 0),
    0 = ‖c n.succ‖ / ‖c n‖
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℕ) ↦ 0) fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖

Tactic:
filter_upwards [hc] with n hc'
-- 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∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
hc :
  ∀ᶠ (x : ℕ) in atTop,
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin x) ↦ E) E) (ofScalars E c x) * (↑r : ℝ) ^ x‖ = 0
n : ℕ
hc' : ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n‖ = 0
⊢ ‖c n‖ = 0 ∨ ‖(↑r : ℝ) ^ n‖ = 0

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

Premises used: norm_mul, norm_norm, mul_eq_zero, FormalMultilinearSeries.ofScalars_norm
-- 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∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
hc :
  ∀ᶠ (x : ℕ) in atTop,
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin x) ↦ E) E) (ofScalars E c x) * (↑r : ℝ) ^ x‖ = 0
n : ℕ
hc' : ‖c n‖ = 0 ∨ ‖(↑r : ℝ) ^ n‖ = 0
h : ‖c n‖ = 0 → 0 = ‖c n.succ‖ / ‖c n‖
h₁ : ‖(↑r : ℝ) ^ n‖ = 0 → 0 = ‖c n.succ‖ / ‖c n‖
⊢ 0 = ‖c n.succ‖ / ‖c n‖

Tactic:
cases hc'
-- 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∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
hc :
  ∀ᶠ (x : ℕ) in atTop,
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin x) ↦ E) E) (ofScalars E c x) * (↑r : ℝ) ^ x‖ = 0
n : ℕ
h : ‖c n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖

Tactic:
aesop
-- 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∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
hc :
  ∀ᶠ (x : ℕ) in atTop,
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin x) ↦ E) E) (ofScalars E c x) * (↑r : ℝ) ^ x‖ = 0
n : ℕ
h : ‖(↑r : ℝ) ^ n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖

Tactic:
aesop
-- 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
hc : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
h :
  ∀ (n : ℕ) (hc : 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖) (hn : n ≠ 0),
    2 * ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n‖ ≤
      ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (ofScalars E c (n + 1)) *
          (↑r : ℝ) ^ (n + 1)‖
⊢ ∀ᶠ (n : ℕ) in atTop,
    2 * ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n‖ ≤
      ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (ofScalars E c (n + 1)) *
          (↑r : ℝ) ^ (n + 1)‖

Tactic:
filter_upwards [hc.eventually_ge_atTop (2 * r⁻¹), eventually_ne_atTop 0] with n hc hn

Premises used: HMul.hMul, Filter.eventually_ne_atTop, Inv.inv, OfNat.ofNat, Filter.Tendsto.eventually_ge_atTop, NNReal.toReal
-- 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
hc_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
n : ℕ
hc : 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
h : 2 * (‖c n‖ * (↑r : ℝ) ^ n) ≤ ‖c (n + 1)‖ * (↑r : ℝ) ^ (n + 1)
⊢ 2 * ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n‖ ≤
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (ofScalars E c (n + 1)) * (↑r : ℝ) ^ (n + 1)‖

Tactic:
simp only [ofScalars_norm, norm_mul, norm_norm, norm_pow, NNReal.norm_eq]

Premises used: norm_pow, norm_mul, norm_norm, NNReal.norm_eq, FormalMultilinearSeries.ofScalars_norm
-- 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
hc_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
n : ℕ
hc : 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
h : 2 * ((↑r : ℝ) ^ n / (↑r : ℝ) ^ (n + 1)) ≤ ‖c (n + 1)‖ / ‖c n‖
h₁ : 0 < (↑r : ℝ) ^ (n + 1)
h₂ : 0 < ‖c n‖
⊢ 2 * (‖c n‖ * (↑r : ℝ) ^ n) ≤ ‖c (n + 1)‖ * (↑r : ℝ) ^ (n + 1)

Tactic:
rw [mul_comm ‖c n‖, ← mul_assoc, ← div_le_div_iff₀, mul_div_assoc]

Premises used: Norm.norm, mul_assoc, mul_div_assoc, div_le_div_iff₀, mul_comm
-- 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
hc_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
n : ℕ
hc : 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖

Tactic:
hc
-- 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
hc_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
n : ℕ
hc : 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
h : (↑r : ℝ) ^ n / (↑r : ℝ) ^ (n + 1) = (↑r⁻¹ : ℝ)
⊢ 2 * ((↑r : ℝ) ^ n / (↑r : ℝ) ^ (n + 1)) ≤ ‖c (n + 1)‖ / ‖c n‖

Tactic:
convert! hc
-- 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
hc_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
n : ℕ
hc : 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
h : (↑r : ℝ) ^ n ≠ 0
⊢ (↑r : ℝ) ^ n / (↑r : ℝ) ^ (n + 1) = (↑r⁻¹ : ℝ)

Tactic:
rw [pow_succ, div_mul_cancel_left₀, NNReal.coe_inv]

Premises used: div_mul_cancel_left₀, pow_succ, NNReal.coe_inv
-- 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
hc_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
n : ℕ
hc : 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ (↑r : ℝ) ^ n ≠ 0

Tactic:
aesop
-- 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
hc_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
n : ℕ
hc : 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 0 < (↑r : ℝ) ^ (n + 1)

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
hc_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
n : ℕ
hc : 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 0 < ‖c n‖

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

Premises used: Not.elim, 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
hc_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
n : ℕ
hc : 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
h : ∀ (hr' : 0 = ‖c n‖), ¬2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
⊢ 0 < ‖c n‖

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

Premises used: Not.elim, 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
hc_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
n : ℕ
hc : 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
hr' : 0 = ‖c n‖
h : ¬2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / 0
⊢ ¬2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖

Tactic:
rw [← 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
hc_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 0 < r
n : ℕ
hc : 2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
hr' : 0 = ‖c n‖
⊢ ¬2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / 0

Tactic:
simp [this]
-- 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)
inl : ∀ (hr : r = 0), radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
inr : ∀ (hr : r = ∞), radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
inr₁ : ∀ (hr : 0 < r.toReal), radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹

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

Premises used: ENNReal.trichotomy