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 : 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) ≤ ‖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
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
have suffices : 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
-- 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
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
have refine : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c)), (↑r : ℝ≥0∞) ≤ 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
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)
⊢ (↑r : ℝ≥0∞) ≤ 0
have rw : r ≤ 0
Tactic: rw [← coe_zero, coe_le_coe]
-- 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
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)
⊢ r ≤ 0
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
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
⊢ r ≤ 0
have contrapose! : ∀ (this : 0 < 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
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
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n
have refine_1 : ∃ᶠ (n : ℕ) in atTop,
  ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n‖ ≠ 0
Tactic: refine not_summable_of_ratio_norm_eventually_ge (r := 2) (by 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
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
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n
have 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)‖
Tactic: refine not_summable_of_ratio_norm_eventually_ge (r := 2) (by 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
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
⊢ ∃ᶠ (n : ℕ) in atTop,
    ‖norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) * (↑r : ℝ) ^ n‖ ≠ 0
have 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
Tactic: contrapose! hc
Cleared hypotheses: 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∞) < 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
⊢ ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
have refine_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
Tactic: apply not_tendsto_atTop_of_tendsto_nhds (a := 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 : ℕ → 𝕜
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
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
have apply : EventuallyEq (β := ℝ) atTop (fun (x : ℕ) ↦ 0) fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖
Tactic: apply Tendsto.congr' ?_ tendsto_const_nhds
-- 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∞) < 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
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℕ) ↦ 0) fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖
have 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‖
Tactic: filter_upwards [hc] with n hc'
-- 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∞) < 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
⊢ 0 = ‖c n.succ‖ / ‖c n‖
have hc'₁ : ‖c n‖ = 0 ∨ ‖(↑r : ℝ) ^ n‖ = 0
Tactic: rw [ofScalars_norm, norm_mul, norm_norm, mul_eq_zero] at hc'
Cleared hypotheses: 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∞) < 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
⊢ 0 = ‖c n.succ‖ / ‖c n‖
have h : ‖c n‖ = 0 → 0 = ‖c n.succ‖ / ‖c n‖
Tactic: cases hc'
Cleared hypotheses: 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∞) < 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‖
⊢ 0 = ‖c n.succ‖ / ‖c n‖
have h₁ : ‖(↑r : ℝ) ^ n‖ = 0 → 0 = ‖c n.succ‖ / ‖c n‖
Tactic: cases hc'
Cleared hypotheses: 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
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
⊢ ∀ᶠ (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)‖
have 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)‖
Tactic: filter_upwards [hc.eventually_ge_atTop (2 * r⁻¹), eventually_ne_atTop 0] with n hc 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 : ℕ → 𝕜
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 * ‖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)‖
have h : 2 * (‖c n‖ * (↑r : ℝ) ^ n) ≤ ‖c (n + 1)‖ * (↑r : ℝ) ^ (n + 1)
Tactic: simp only [ofScalars_norm, 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 : ℕ → 𝕜
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 * (‖c n‖ * (↑r : ℝ) ^ n) ≤ ‖c (n + 1)‖ * (↑r : ℝ) ^ (n + 1)
have h : 2 * ((↑r : ℝ) ^ n / (↑r : ℝ) ^ (n + 1)) ≤ ‖c (n + 1)‖ / ‖c n‖
Tactic: rw [mul_comm ‖c n‖, ← mul_assoc, ← div_le_div_iff₀, mul_div_assoc]
-- 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
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‖
⊢ 2 * (‖c n‖ * (↑r : ℝ) ^ n) ≤ ‖c (n + 1)‖ * (↑r : ℝ) ^ (n + 1)
have h₁ : 0 < (↑r : ℝ) ^ (n + 1)
Tactic: rw [mul_comm ‖c n‖, ← mul_assoc, ← div_le_div_iff₀, mul_div_assoc]
-- 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
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)
⊢ 2 * (‖c n‖ * (↑r : ℝ) ^ n) ≤ ‖c (n + 1)‖ * (↑r : ℝ) ^ (n + 1)
have h₂ : 0 < ‖c n‖
Tactic: rw [mul_comm ‖c n‖, ← mul_assoc, ← div_le_div_iff₀, mul_div_assoc]
-- 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
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 : ℝ) ^ n / (↑r : ℝ) ^ (n + 1)) ≤ ‖c (n + 1)‖ / ‖c n‖
have h : (↑r : ℝ) ^ n / (↑r : ℝ) ^ (n + 1) = (↑r⁻¹ : ℝ)
Tactic: convert! 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
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 / (↑r : ℝ) ^ (n + 1) = (↑r⁻¹ : ℝ)
have h : (↑r : ℝ) ^ n ≠ 0
Tactic: rw [pow_succ, div_mul_cancel_left₀, NNReal.coe_inv]
-- 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
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‖
have h : ∀ (hr' : 0 = ‖c n‖), ¬2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / ‖c n‖
Tactic: refine Ne.lt_of_le (fun hr' ↦ Not.elim ?_ hc) (norm_nonneg _)
-- 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
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‖ / ‖c n‖
have h : ¬2 * (↑r⁻¹ : ℝ) ≤ ‖c n.succ‖ / 0
Tactic: rw [← 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∞
hc' : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
have inl : ∀ (hr : r = 0), radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
Tactic: rcases ENNReal.trichotomy r with (hr | hr | 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∞
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⁻¹
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
have inr : ∀ (hr : 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)
-- 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∞
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⁻¹
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
have inr₁ : ∀ (hr : 0 < r.toReal), radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
Tactic: rcases ENNReal.trichotomy r with (hr | hr | 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∞
hc' : Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 r)
hr : r = 0
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = r⁻¹
have 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) = ∞
Tactic: simp_rw [hr, inv_zero] at hc' ⊢
Cleared hypotheses: 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 (β := ℝ≥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) = ∞
have pos : ∀ (h : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0), radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = ∞
Tactic: by_cases h : (∀ᶠ (n : ℕ) in atTop, c n ≠ 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 : ℕ → 𝕜
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) = ∞
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = ∞
have neg : ∀ (h : ¬∀ᶠ (n : ℕ) in atTop, c n ≠ 0), radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = ∞
Tactic: by_cases h : (∀ᶠ (n : ℕ) in atTop, c n ≠ 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 : ℕ → 𝕜
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
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = ∞
have apply : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
Tactic: apply ofScalars_radius_eq_top_of_tendsto E c h ?_
-- 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 (β := ℝ≥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)
have refine : (ENNReal.toReal ∘ fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) =ᶠ[atTop] fun (n : ℕ) ↦
  ‖c n.succ‖ / ‖c n‖
Tactic: refine Tendsto.congr' ?_ <| (tendsto_toReal zero_ne_top).comp 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 (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
⊢ (ENNReal.toReal ∘ fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) =ᶠ[atTop] fun (n : ℕ) ↦
    ‖c n.succ‖ / ‖c n‖
have h₁ : ∀ (a : ℕ),
  c a ≠ 0 → (ENNReal.toReal ∘ fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) a = ‖c a.succ‖ / ‖c a‖
Tactic: filter_upwards [h]
-- 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 (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ¬∀ᶠ (n : ℕ) in atTop, c n ≠ 0
⊢ radius.{u_1, u_2, u_2} (𝕜 := 𝕜) (E := E) (F := E) (ofScalars E c) = ∞
have neg : ∀ᶠ (n : ℕ) in atTop, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0
Tactic: apply (ofScalars E c).radius_eq_top_of_eventually_eq_zero
-- 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 (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖c n.succ‖ / ENNReal.ofReal ‖c n‖) atTop (𝓝 0)
h : ¬∀ᶠ (n : ℕ) in atTop, c n ≠ 0
⊢ ∀ᶠ (n : ℕ) in atTop, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) E) (ofScalars E c n) 0
have 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
Tactic: simp only [eventually_atTop, not_exists, not_forall, not_not] at h ⊢
Cleared hypotheses: h
-- 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 (β := ℝ≥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
⊢ ∃ (a : ℕ), ∀ b ≥ a, Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin b) ↦ E) E) (ofScalars E c b) 0
have 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
Tactic: obtain ⟨ti, hti⟩ := eventually_atTop.mp (hc'.eventually_ne zero_ne_top)