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 : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
neg : Summable (α := ℝ) fun (n : ℕ) ↦ ‖‖c n‖ * (↑r' : ℝ) ^ n‖
neg₁ :
  ∀ᶠ (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
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n

Tactic:
refine Summable.of_norm_bounded_eventually (g := fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_

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

Tactic:
summable_of_ratio_test_tendsto_lt_one hr' ?_ ?_

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

Tactic:
refine summable_of_ratio_test_tendsto_lt_one hr' ?_ ?_

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

Tactic:
(hc.eventually_ne (NNReal.coe_ne_zero.mpr hr)).mp (Eventually.of_forall ?_)

Premises used: Iff.mpr, Filter.Tendsto.eventually_ne, Filter.Eventually.of_forall, Filter.Eventually.mp, NNReal.coe_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 : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
neg : ∀ (x : ℕ), ‖c x.succ‖ / ‖c x‖ ≠ 0 → ‖‖c x‖ * (↑r' : ℝ) ^ x‖ ≠ 0
⊢ ∀ᶠ (n : ℕ) in atTop, ‖‖c n‖ * (↑r' : ℝ) ^ n‖ ≠ 0

Tactic:
refine (hc.eventually_ne (NNReal.coe_ne_zero.mpr hr)).mp (Eventually.of_forall ?_)

Premises used: Iff.mpr, Filter.Tendsto.eventually_ne, Filter.Eventually.of_forall, Filter.Eventually.mp, NNReal.coe_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 : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ ∀ (x : ℕ), ‖c x.succ‖ / ‖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 : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
neg : Tendsto (fun (n : ℕ) ↦ ‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖ / ‖‖c n‖ * (↑r' : ℝ) ^ n‖) atTop (𝓝 (↑(r' * r) : ℝ))
⊢ Tendsto (fun (n : ℕ) ↦ ‖‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖‖ / ‖‖‖c n‖ * (↑r' : ℝ) ^ n‖‖) atTop (𝓝 (↑(r' * r) : ℝ))

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

Tactic:
tendsto_succ_norm_div_norm c hrz hc

Premises used: _private.0.FormalMultilinearSeries.tendsto_succ_norm_div_norm, 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 : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ Tendsto (fun (n : ℕ) ↦ ‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖ / ‖‖c n‖ * (↑r' : ℝ) ^ n‖) atTop (𝓝 (↑(r' * r) : ℝ))

Tactic:
exact tendsto_succ_norm_div_norm c hrz hc

Premises used: _private.0.FormalMultilinearSeries.tendsto_succ_norm_div_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 : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
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 : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
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 : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
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 : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
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 : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : r' * r < 1
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
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = (↑r⁻¹ : ℝ≥0∞)

Tactic:
le_antisymm ?_ (inv_le_ofScalars_radius_of_tendsto E c hr hc)

Premises used: FormalMultilinearSeries.inv_le_ofScalars_radius_of_tendsto, le_antisymm
-- 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 (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
refine : radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) ≤ (↑r⁻¹ : ℝ≥0∞)
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = (↑r⁻¹ : ℝ≥0∞)

Tactic:
refine le_antisymm ?_ (inv_le_ofScalars_radius_of_tendsto E c hr hc)

Premises used: FormalMultilinearSeries.inv_le_ofScalars_radius_of_tendsto, le_antisymm
-- 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 (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) ≤ (↑r⁻¹ : ℝ≥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
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
refine :
  ∀ (r' : ℝ≥0) (hr' : (↑r' : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)),
    (↑r' : ℝ≥0∞) ≤ (↑r⁻¹ : ℝ≥0∞)
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) ≤ (↑r⁻¹ : ℝ≥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
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
rw : r' * r ≤ 1
⊢ (↑r' : ℝ≥0∞) ≤ (↑r⁻¹ : ℝ≥0∞)

Tactic:
rw [coe_le_coe, NNReal.le_inv_iff_mul_le hr]

Premises used: ENNReal.coe_le_coe, NNReal.le_inv_iff_mul_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
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
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
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
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 : 1 < r' * r),
    ¬Summable (α := ℝ) fun (n : ℕ) ↦
        norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
⊢ r' * r ≤ 1

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

Tactic:
apply not_summable_of_ratio_test_tendsto_gt_one this

Premises used: not_summable_of_ratio_test_tendsto_gt_one
-- 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 (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 1 < r' * r
simp_rw :
  Tendsto (fun (n : ℕ) ↦ ‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖ / ‖‖c n‖ * (↑r' : ℝ) ^ n‖) atTop (𝓝 (↑(r' * r) : ℝ))
⊢ Tendsto
    (fun (n : ℕ) ↦
      ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (ofScalars E c (n + 1)) *
            (↑r' : ℝ) ^ (n + 1)‖ /
        ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n‖)
    atTop (𝓝 (↑(r' * r) : ℝ))

Tactic:
simp_rw [ofScalars_norm]

Premises used: 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
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 1 < r' * r
⊢ r' ≠ 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
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
r' : ℝ≥0
hr' : (↑r' : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
this : 1 < r' * r
⊢ Tendsto (fun (n : ℕ) ↦ ‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖ / ‖‖c n‖ * (↑r' : ℝ) ^ n‖) atTop (𝓝 (↑(r' * r) : ℝ))

Tactic:
exact tendsto_succ_norm_div_norm c (by aesop) hc

Premises used: _private.0.FormalMultilinearSeries.tendsto_succ_norm_div_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
hc : Tendsto (fun (n : ℕ) ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 (↑r : ℝ))
this : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ)⁻¹)
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = (↑r⁻¹⁻¹ : ℝ≥0∞)

Tactic:
ofScalars_radius_eq_inv_of_tendsto E c (inv_ne_zero hr) this

Premises used: FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto, inv_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 ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 (↑r : ℝ))
this : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ)⁻¹)
h : r = r⁻¹⁻¹
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = (↑r : ℝ≥0∞)

Tactic:
convert! ofScalars_radius_eq_inv_of_tendsto E c (inv_ne_zero hr) this

Premises used: FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto, inv_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 ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 (↑r : ℝ))
this : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ)⁻¹)
⊢ r = r⁻¹⁻¹

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 (fun (n : ℕ) ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 (↑r : ℝ))
suffices : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ)⁻¹)
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = (↑r : ℝ≥0∞)

Tactic:
suffices Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r⁻¹) by
    convert! ofScalars_radius_eq_inv_of_tendsto E c (inv_ne_zero hr) this
    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 (fun (n : ℕ) ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 (↑r : ℝ))
⊢ Tendsto (fun (x : ℕ) ↦ (‖c x‖ / ‖c x.succ‖)⁻¹) atTop (𝓝 (↑r : ℝ)⁻¹)

Tactic:
hc.inv₀ (NNReal.coe_ne_zero.mpr hr)

Premises used: Iff.mpr, Filter.Tendsto.inv₀, NNReal.coe_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 ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 (↑r : ℝ))
h : Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) fun (x : ℕ) ↦ (‖c x‖ / ‖c x.succ‖)⁻¹
⊢ Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ)⁻¹)

Tactic:
convert! hc.inv₀ (NNReal.coe_ne_zero.mpr hr) using 1

Premises used: Iff.mpr, Filter.Tendsto.inv₀, NNReal.coe_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 ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n‖ / ‖c n.succ‖) atTop (𝓝 (↑r : ℝ))
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) fun (x : ℕ) ↦ (‖c x‖ / ‖c x.succ‖)⁻¹

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 : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : 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:
radius_eq_top_of_summable_norm _ fun r' ↦ ?_

Premises used: FormalMultilinearSeries.radius_eq_top_of_summable_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)
refine :
  ∀ (r' : ℝ≥0),
    Summable (α := ℝ) fun (n : ℕ) ↦
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = ∞

Tactic:
refine radius_eq_top_of_summable_norm _ fun r' ↦ ?_

Premises used: FormalMultilinearSeries.radius_eq_top_of_summable_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
pos :
  ∀ (hrz : r' = 0),
    Summable (α := ℝ) fun (n : ℕ) ↦
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
neg :
  ∀ (hrz : ¬r' = 0),
    Summable (α := ℝ) fun (n : ℕ) ↦
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n

Tactic:
by_cases hrz : r' = 0
-- 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
pos :
  Summable (α := ℝ) fun (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:
apply Summable.comp_nat_add (k := 1)

Premises used: Summable.comp_nat_add
-- 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
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (ofScalars E c (n + 1)) * (↑r' : ℝ) ^ (n + 1)

Tactic:
simp [hrz]
-- 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
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n

Tactic:
Summable.of_norm_bounded_eventually (g := fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_

Premises used: Summable.of_norm_bounded_eventually
-- 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 : Summable (α := ℝ) fun (n : ℕ) ↦ ‖‖c n‖ * (↑r' : ℝ) ^ n‖
neg₁ :
  ∀ᶠ (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
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n

Tactic:
refine Summable.of_norm_bounded_eventually (g := fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_

Premises used: Summable.of_norm_bounded_eventually
-- 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)
apply : ∀ (x : ℕ), c x ≠ 0 → ‖‖c x‖ * (↑r' : ℝ) ^ x‖ ≠ 0
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖‖c n‖ * (↑r' : ℝ) ^ n‖

Tactic:
apply summable_of_ratio_test_tendsto_lt_one zero_lt_one (hc.mp (Eventually.of_forall ?_))

Premises used: summable_of_ratio_test_tendsto_lt_one, Filter.Eventually.of_forall, zero_lt_one, Filter.Eventually.mp