awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : p.radius = ∞
r : ℝ≥0
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
have mp : ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a) (C : ℝ) (hp : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n),
  Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
Tactic: obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius
      (show (r : ℝ≥0∞) < p.radius from h.symm ▸ ENNReal.coe_lt_top)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : p.radius = ∞
r : ℝ≥0
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
have mp : ∀ (n : ℕ), ‖‖p n‖ * (↑r : ℝ) ^ n‖ ≤ (fun (n : ℕ) ↦ C * a ^ n) n
Tactic: refine .of_norm_bounded
      (g := fun n ↦ (C : ℝ) * a ^ n) ((summable_geometric_of_lt_one ha.1.le ha.2).mul_left _)
      fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : p.radius = ∞
r : ℝ≥0
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hp : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
n : ℕ
⊢ ‖‖p n‖ * (↑r : ℝ) ^ n‖ ≤ (fun (n : ℕ) ↦ C * a ^ n) n
have hp₁ : ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
Tactic: specialize hp n
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
⊢ ∃ (C : ℝ) (r : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
have rcases : ∀ (r : ℝ≥0) (r0 : 0 < (↑r : ℝ≥0∞)) (rlt : (↑r : ℝ≥0∞) < p.radius),
  ∃ (C : ℝ) (r : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
Tactic: rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨r, r0, rlt⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < (↑r : ℝ≥0∞)
rlt : (↑r : ℝ≥0∞) < p.radius
⊢ ∃ (C : ℝ) (r : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
have rpos : 0 < (↑r : ℝ)
Tactic: have rpos : 0 < (r : ℝ) := by simp [ENNReal.coe_pos.1 r0]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < (↑r : ℝ≥0∞)
rlt : (↑r : ℝ≥0∞) < p.radius
rpos : 0 < (↑r : ℝ)
⊢ ∃ (C : ℝ) (r : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
have rcases : ∀ (C : ℝ) (Cpos : C > 0) (hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / (↑r : ℝ) ^ n),
  ∃ (C : ℝ) (r : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
Tactic: rcases norm_le_div_pow_of_pos_of_lt_radius p rpos rlt with ⟨C, Cpos, hCp⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < (↑r : ℝ≥0∞)
rlt : (↑r : ℝ≥0∞) < p.radius
rpos : 0 < (↑r : ℝ)
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / (↑r : ℝ) ^ n
⊢ ∃ (C : ℝ) (r : ℝ) (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
have refine : ∀ (n : ℕ), ‖p n‖ ≤ C * (↑r : ℝ)⁻¹ ^ n
Tactic: refine ⟨C, r⁻¹, Cpos, by simp only [inv_pos, rpos], fun n => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < (↑r : ℝ≥0∞)
rlt : (↑r : ℝ≥0∞) < p.radius
rpos : 0 < (↑r : ℝ)
C : ℝ
Cpos : C > 0
hCp : ∀ (n : ℕ), ‖p n‖ ≤ C / (↑r : ℝ) ^ n
n : ℕ
⊢ ‖p n‖ ≤ C * (↑r : ℝ)⁻¹ ^ n
have rw : ‖p n‖ ≤ C / (↑r : ℝ) ^ n
Tactic: rw [inv_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
E' : Type u_6
F' : Type u_7
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜' E'
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜' F'
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜' E' F'
h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖
⊢ q.radius ≤ p.radius
have apply : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < q.radius), (↑r : ℝ≥0∞) ≤ p.radius
Tactic: apply le_of_forall_nnreal_lt (fun r hr ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
E' : Type u_6
F' : Type u_7
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜' E'
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜' F'
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜' E' F'
h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < q.radius
⊢ (↑r : ℝ≥0∞) ≤ p.radius
have rcases : ∀ (C : ℝ) (hC : ∀ (n : ℕ), ‖q n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞) ≤ p.radius
Tactic: rcases norm_mul_pow_le_of_lt_radius _ hr with ⟨C, -, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
E' : Type u_6
F' : Type u_7
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜' E'
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜' F'
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜' E' F'
h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < q.radius
C : ℝ
hC : ∀ (n : ℕ), ‖q n‖ * (↑r : ℝ) ^ n ≤ C
⊢ (↑r : ℝ≥0∞) ≤ p.radius
have apply : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
Tactic: apply le_radius_of_bound _ C (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
E' : Type u_6
F' : Type u_7
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜' E'
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜' F'
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜' E' F'
h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < q.radius
C : ℝ
hC : ∀ (n : ℕ), ‖q n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p n‖ * (↑r : ℝ) ^ n ≤ C
have apply : ‖p n‖ * (↑r : ℝ) ^ n ≤ ‖q n‖ * (↑r : ℝ) ^ n
Tactic: apply le_trans _ (hC n)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
E' : Type u_6
F' : Type u_7
inst_5 : NontriviallyNormedField 𝕜'
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜' E'
inst_8 : NormedAddCommGroup F'
inst_9 : NormedSpace 𝕜' F'
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜' E' F'
h : ∀ (n : ℕ), ‖p n‖ ≤ ‖q n‖
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < q.radius
C : ℝ
hC : ∀ (n : ℕ), ‖q n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p n‖ * (↑r : ℝ) ^ n ≤ ‖q n‖ * (↑r : ℝ) ^ n
have hbc : ‖p n‖ ≤ ‖q n‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
⊢ min p.radius q.radius ≤ (p + q).radius
have refine : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < min p.radius q.radius), (↑r : ℝ≥0∞) ≤ (p + q).radius
Tactic: refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < min p.radius q.radius
⊢ (↑r : ℝ≥0∞) ≤ (p + q).radius
have hr₁ : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
Tactic: rw [lt_min_iff] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
⊢ (↑r : ℝ≥0∞) ≤ (p + q).radius
have this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖p x‖ * (↑r : ℝ) ^ x + ‖q x‖ * (↑r : ℝ) ^ x) fun (x : ℕ) ↦ 1
Tactic: have := ((p.isLittleO_one_of_lt_radius hr.1).add (q.isLittleO_one_of_lt_radius hr.2)).isBigO
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖p x‖ * (↑r : ℝ) ^ x + ‖q x‖ * (↑r : ℝ) ^ x) fun (x : ℕ) ↦ 1
⊢ (↑r : ℝ≥0∞) ≤ (p + q).radius
have refine : ∀ (n : ℕ), ‖‖(p + q) n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ * (↑r : ℝ) ^ n + ‖q n‖ * (↑r : ℝ) ^ n‖
Tactic: refine (p + q).le_radius_of_isBigO ((isBigO_of_le _ fun n => ?_).trans this)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖p x‖ * (↑r : ℝ) ^ x + ‖q x‖ * (↑r : ℝ) ^ x) fun (x : ℕ) ↦ 1
n : ℕ
⊢ ‖‖(p + q) n‖ * (↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ * (↑r : ℝ) ^ n + ‖q n‖ * (↑r : ℝ) ^ n‖
have rw : ‖(p + q) n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ + ‖q n‖‖ * ‖(↑r : ℝ) ^ n‖
Tactic: rw [← add_mul, norm_mul, norm_mul, norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p q : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius ∧ (↑r : ℝ≥0∞) < q.radius
this : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖p x‖ * (↑r : ℝ) ^ x + ‖q x‖ * (↑r : ℝ) ^ x) fun (x : ℕ) ↦ 1
n : ℕ
⊢ ‖(p + q) n‖ * ‖(↑r : ℝ) ^ n‖ ≤ ‖‖p n‖ + ‖q n‖‖ * ‖(↑r : ℝ) ^ n‖
have hbc : ‖(p + q) n‖ ≤ ‖‖p n‖ + ‖q n‖‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_5
c : 𝕜'
inst_5 : NormedRing 𝕜'
inst_6 : Module 𝕜' F
inst_7 : SMulCommClass 𝕜 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
⊢ LE.le (α := ℝ≥0∞) (⨆ (r : ℝ≥0), ⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))
    (⨆ (r : ℝ≥0), ⨆ (C : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖c • p n‖ * (↑r : ℝ) ^ n ≤ C), (↑r : ℝ≥0∞))
have refine : ∀ (r : ℝ≥0) (C : ℝ) (h : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C),
  ∃ (_ : ∀ (n : ℕ), ‖c • p n‖ * (↑r : ℝ) ^ n ≤ ‖c‖ * C), (↑r : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)
Tactic: refine iSup_mono fun r ↦ iSup_mono' fun C ↦ ⟨‖c‖ * C, iSup_mono' fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_5
c : 𝕜'
inst_5 : NormedRing 𝕜'
inst_6 : Module 𝕜' F
inst_7 : SMulCommClass 𝕜 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
⊢ ∃ (_ : ∀ (n : ℕ), ‖c • p n‖ * (↑r : ℝ) ^ n ≤ ‖c‖ * C), (↑r : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)
have simp : ∀ (n : ℕ), ‖c • p n‖ * (↑r : ℝ) ^ n ≤ ‖c‖ * C
Tactic: simp only [le_refl, exists_prop, and_true]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
𝕜' : Type u_5
c : 𝕜'
inst_5 : NormedDivisionRing 𝕜'
inst_6 : Module 𝕜' F
inst_7 : NormSMulClass 𝕜' F
inst_8 : SMulCommClass 𝕜 𝕜' F
hc : c ≠ 0
⊢ (c • p).radius = p.radius
have apply : (c • p).radius ≤ p.radius
Tactic: apply eq_of_le_of_ge _ radius_le_smul
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
n : ℕ
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin n) ↦ E) G)
      ((p n).compContinuousLinearMap (M₁ := fun (i : Fin n) ↦ E) (M₁' := fun (i : Fin n) ↦ F) fun (x : Fin n) ↦ u) ≤
    ‖p n‖ * ‖u‖ ^ n
have apply : ‖p n‖ * ∏ i : Fin n, ‖u‖ ≤ ‖p n‖ * ‖u‖ ^ n
Tactic: apply le_trans (ContinuousMultilinearMap.norm_compContinuousLinearMap_le _ _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
n : ℕ
⊢ ‖p.compContinuousLinearMap u n‖ₑ ≤ ‖p n‖ₑ * ‖u‖ₑ ^ n
have rw : ENNReal.ofReal ‖p.compContinuousLinearMap u n‖ ≤ ENNReal.ofReal (‖p n‖ * ‖u‖ ^ n)
Tactic: rw [← ofReal_norm, ← ofReal_norm, ← ofReal_norm,
    ← ENNReal.ofReal_pow (by simp), ← ENNReal.ofReal_mul (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
n : ℕ
⊢ ENNReal.ofReal ‖p.compContinuousLinearMap u n‖ ≤ ENNReal.ofReal (‖p n‖ * ‖u‖ ^ n)
have h : ‖p.compContinuousLinearMap u n‖ ≤ ‖p n‖ * ‖u‖ ^ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
⊢ p.radius / ‖u‖ₑ ≤ radius (p.compContinuousLinearMap u)
have inl : p.radius / enorm (E := E →L[𝕜] F) 0 ≤ radius.{u_1, u_2, u_4} (E := E) (p.compContinuousLinearMap 0)
Tactic: obtain (rfl | h_zero) := eq_zero_or_nnnorm_pos u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
inl : p.radius / enorm (E := E →L[𝕜] F) 0 ≤ radius.{u_1, u_2, u_4} (E := E) (p.compContinuousLinearMap 0)
⊢ p.radius / ‖u‖ₑ ≤ radius (p.compContinuousLinearMap u)
have inr : ∀ (h_zero : 0 < ‖u‖₊), p.radius / ‖u‖ₑ ≤ radius (p.compContinuousLinearMap u)
Tactic: obtain (rfl | h_zero) := eq_zero_or_nnnorm_pos u
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
⊢ p.radius / ‖u‖ₑ ≤ radius (p.compContinuousLinearMap u)
have inr : p.radius ≤ radius (p.compContinuousLinearMap u) * ‖u‖ₑ
Tactic: rw [ENNReal.div_le_iff (by simpa using h_zero) (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
⊢ p.radius ≤ radius (p.compContinuousLinearMap u) * ‖u‖ₑ
have inr : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < p.radius), (↑r : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u) * ‖u‖ₑ
Tactic: refine le_of_forall_nnreal_lt fun r hr ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
⊢ (↑r : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u) * ‖u‖ₑ
have inr : (↑(r / ‖u‖₊) : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u)
Tactic: rw [← ENNReal.div_le_iff (by simpa using h_zero) (by simp), enorm_eq_nnnorm, ← coe_div h_zero.ne']
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
⊢ (↑(r / ‖u‖₊) : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u)
have inr : ∀ (C : ℝ) (hC_pos : C > 0) (hC : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C),
  (↑(r / ‖u‖₊) : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u)
Tactic: obtain ⟨C, hC_pos, hC⟩ := p.norm_mul_pow_le_of_lt_radius hr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
⊢ (↑(r / ‖u‖₊) : ℝ≥0∞) ≤ radius (p.compContinuousLinearMap u)
have inr : ∀ (n : ℕ), ‖p.compContinuousLinearMap u n‖ * (↑(r / ‖u‖₊) : ℝ) ^ n ≤ C
Tactic: refine le_radius_of_bound _ C fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p.compContinuousLinearMap u n‖ * (↑(r / ‖u‖₊) : ℝ) ^ n ≤ ‖p n‖ * ‖u‖ ^ n * (↑(r / ‖u‖₊) : ℝ) ^ n
have hbc : ‖p.compContinuousLinearMap u n‖ ≤ ‖p n‖ * ‖u‖ ^ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p n‖ * ‖u‖ ^ n * (↑(r / ‖u‖₊) : ℝ) ^ n = ‖p n‖ * (↑r : ℝ) ^ n
have simp : ‖p n‖ * (‖u‖ ^ n * ((↑r : ℝ) ^ n / ‖u‖ ^ n)) = ‖p n‖ * (↑r : ℝ) ^ n
Tactic: simp only [NNReal.coe_div, coe_nnnorm, div_pow, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖p n‖ * (‖u‖ ^ n * ((↑r : ℝ) ^ n / ‖u‖ ^ n)) = ‖p n‖ * (↑r : ℝ) ^ n
have hb : ‖u‖ ^ n ≠ 0
Tactic: rw [mul_div_cancel₀]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ConvergenceRadius (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
C : ℝ
hC_pos : C > 0
hC : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C
n : ℕ
⊢ ‖u‖ ^ n ≠ 0
have hb : ∀ (h_zero : 0 < (↑‖u‖₊ : ℝ)) (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < p.radius) (C : ℝ) (hC_pos : C > 0)
  (hC : ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C) (n : ℕ), ‖u‖ ^ n ≠ 0
Tactic: rw [← NNReal.coe_pos] at h_zero
Cleared hypotheses: h_zero, r, hr, C, hC_pos, hC, n