awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
rw :
  ‖HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (c n)
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)‖ =
    ‖c n‖ *
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) =
    ‖c n‖ *
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)
have rw₁ : ‖c n‖ * norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) =
  ‖c n‖ * norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)
Tactic: rw [ofScalars, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedRing E
inst_2 : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
hn : n > 0
⊢ norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) ≤ ‖c n‖
have simp : ‖c n‖ * norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) ≤
  ‖c n‖
Tactic: simp only [ofScalars_norm_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
c : ℕ → 𝕜
r r' : ℝ≥0
hr' : r' ≠ 0
hc : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ))
⊢ Tendsto (fun (n : ℕ) ↦ ‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖ / ‖‖c n‖ * (↑r' : ℝ) ^ n‖) atTop (𝓝 (↑(r' * r) : ℝ))
have simp_rw : Tendsto (fun (n : ℕ) ↦ ‖c (n + 1)‖ / ‖c n‖ * (↑r' : ℝ)) atTop (𝓝 (↑(r' * r) : ℝ))
Tactic: simp_rw [norm_mul, norm_norm, mul_div_mul_comm, ← norm_div, pow_succ, mul_div_right_comm,
    div_self (pow_ne_zero _ (NNReal.coe_ne_zero.mpr hr')), one_mul, norm_div, NNReal.norm_eq]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
have refine : ∀ (r' : ℝ≥0) (hr' : (↑r' : ℝ≥0∞) < (↑r⁻¹ : ℝ≥0∞)),
  (↑r' : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
Tactic: refine le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (hypothesis)
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' : ℝ≥0∞) < (↑r⁻¹ : ℝ≥0∞)
⊢ (↑r' : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
have hr'₁ : r' * r < 1
Tactic: rw [coe_lt_coe, NNReal.lt_inv_iff_mul_lt hr] at hr'
Cleared hypotheses: hr'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
⊢ (↑r' : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
have pos : ∀ (hrz : r' = 0), (↑r' : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
Tactic: by_cases hrz : r' = 0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
pos : ∀ (hrz : r' = 0), (↑r' : ℝ≥0∞) ≤ 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)
have neg : ∀ (hrz : ¬r' = 0), (↑r' : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
Tactic: by_cases hrz : r' = 0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
⊢ (↑r' : ℝ≥0∞) ≤ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)
have neg : Summable (α := ℝ) fun (n : ℕ) ↦
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
Tactic: apply FormalMultilinearSeries.le_radius_of_summable_norm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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 : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
have neg : Summable (α := ℝ) fun (n : ℕ) ↦ ‖‖c n‖ * (↑r' : ℝ) ^ n‖
Tactic: refine Summable.of_norm_bounded_eventually (g := fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
have 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
Tactic: refine Summable.of_norm_bounded_eventually (g := fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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‖
have neg : ∀ᶠ (n : ℕ) in atTop, ‖‖c n‖ * (↑r' : ℝ) ^ n‖ ≠ 0
Tactic: refine summable_of_ratio_test_tendsto_lt_one hr' ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖‖c n‖ * (↑r' : ℝ) ^ n‖
have neg₁ : Tendsto (fun (n : ℕ) ↦ ‖‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖‖ / ‖‖‖c n‖ * (↑r' : ℝ) ^ n‖‖) atTop (𝓝 (↑(r' * r) : ℝ))
Tactic: refine summable_of_ratio_test_tendsto_lt_one hr' ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
have neg : ∀ (x : ℕ), ‖c x.succ‖ / ‖c x‖ ≠ 0 → ‖‖c x‖ * (↑r' : ℝ) ^ x‖ ≠ 0
Tactic: refine (hc.eventually_ne (NNReal.coe_ne_zero.mpr hr)).mp (Eventually.of_forall ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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) : ℝ))
have neg : Tendsto (fun (n : ℕ) ↦ ‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖ / ‖‖c n‖ * (↑r' : ℝ) ^ n‖) atTop (𝓝 (↑(r' * r) : ℝ))
Tactic: simp_rw [norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
⊢ ∀ᶠ (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
have h : ∀ (n : ℕ) (hn : n ≠ 0),
  ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n‖ ≤
    ‖‖c n‖ * (↑r' : ℝ) ^ n‖
Tactic: filter_upwards [eventually_cofinite_ne 0] with n hn
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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) * (↑r' : ℝ) ^ n‖ ≤
    ‖‖c n‖ * (↑r' : ℝ) ^ n‖
have h : 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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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) * (↑r' : ℝ) ^ n ≤
    ‖c n‖ * (↑r' : ℝ) ^ n
have h : norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) ≤ ‖c n‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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∞)
have refine : 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)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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∞)
have refine : ∀ (r' : ℝ≥0) (hr' : (↑r' : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)),
  (↑r' : ℝ≥0∞) ≤ (↑r⁻¹ : ℝ≥0∞)
Tactic: refine le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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)
⊢ (↑r' : ℝ≥0∞) ≤ (↑r⁻¹ : ℝ≥0∞)
have rw : r' * r ≤ 1
Tactic: rw [coe_le_coe, NNReal.le_inv_iff_mul_le hr]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (hypothesis)
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)
⊢ r' * r ≤ 1
have this : 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'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
⊢ r' * r ≤ 1
have contrapose! : ∀ (this : 1 < r' * r),
  ¬Summable (α := ℝ) fun (n : ℕ) ↦
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
have 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) : ℝ))
Tactic: apply not_summable_of_ratio_test_tendsto_gt_one this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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 : ℕ) ↦
      ‖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) : ℝ))
have simp_rw : Tendsto (fun (n : ℕ) ↦ ‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖ / ‖‖c n‖ * (↑r' : ℝ) ^ n‖) atTop (𝓝 (↑(r' * r) : ℝ))
Tactic: simp_rw [ofScalars_norm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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∞)
have h : r = r⁻¹⁻¹
Tactic: convert! ofScalars_radius_eq_inv_of_tendsto E c (inv_ne_zero hr) this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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 : ℝ))
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = (↑r : ℝ≥0∞)
have suffices : Tendsto (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ)⁻¹)
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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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 (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 (↑r : ℝ)⁻¹)
have h : Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) fun (x : ℕ) ↦ (‖c x‖ / ‖c x.succ‖)⁻¹
Tactic: convert! hc.inv₀ (NNReal.coe_ne_zero.mpr hr) using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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) = ∞
have refine : ∀ (r' : ℝ≥0),
  Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
Tactic: refine radius_eq_top_of_summable_norm _ fun r' ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
have pos : ∀ (hrz : r' = 0),
  Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
Tactic: by_cases hrz : r' = 0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
have neg : ∀ (hrz : ¬r' = 0),
  Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
Tactic: by_cases hrz : r' = 0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
have pos : Summable (α := ℝ) fun (n : ℕ) ↦
  norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 1)) ↦ E) E) (ofScalars E c (n + 1)) * (↑r' : ℝ) ^ (n + 1)
Tactic: apply Summable.comp_nat_add (k := 1)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
have neg : Summable (α := ℝ) fun (n : ℕ) ↦ ‖‖c n‖ * (↑r' : ℝ) ^ n‖
Tactic: refine Summable.of_norm_bounded_eventually (g := fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n
have 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
Tactic: refine Summable.of_norm_bounded_eventually (g := fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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 : ℕ) ↦ ‖‖c n‖ * (↑r' : ℝ) ^ n‖
have neg : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖‖ / ‖‖‖c n‖ * (↑r' : ℝ) ^ n‖‖) atTop (𝓝 0)
Tactic: apply summable_of_ratio_test_tendsto_lt_one zero_lt_one (hc.mp (Eventually.of_forall ?_))
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖‖c n‖ * (↑r' : ℝ) ^ n‖
have apply : ∀ (x : ℕ), c x ≠ 0 → ‖‖c x‖ * (↑r' : ℝ) ^ x‖ ≠ 0
Tactic: apply summable_of_ratio_test_tendsto_lt_one zero_lt_one (hc.mp (Eventually.of_forall ?_))
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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)
have neg : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖‖c (n + 1)‖ * (↑r' : ℝ) ^ (n + 1)‖ / ‖‖c n‖ * (↑r' : ℝ) ^ n‖) atTop (𝓝 0)
Tactic: simp only [norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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
⊢ ∀ᶠ (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
have h : ∀ (n : ℕ) (hn : n ≠ 0),
  ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r' : ℝ) ^ n‖ ≤
    ‖‖c n‖ * (↑r' : ℝ) ^ n‖
Tactic: filter_upwards [eventually_cofinite_ne 0] with n hn
-- Lean 4 proof step from Mathlib.Analysis.Analytic.OfScalars (goal)
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) * (↑r' : ℝ) ^ n‖ ≤
    ‖‖c n‖ * (↑r' : ℝ) ^ n‖
have h : 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]