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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
⊢ ∃ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
      IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x
have rw : ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
Tactic: rw [this]
-- 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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
⊢ ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
have h₁ : ∃ (i : ℝ≥0) (i_1 : ℝ) (_ : ∀ (n : ℕ), ‖p n‖ * (↑i : ℝ) ^ n ≤ i_1), (↑r : ℝ≥0∞) < (↑i : ℝ≥0∞)
Tactic: simp only [radius, lt_iSup_iff] at h
Cleared hypotheses: 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
r : ℝ≥0
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
h : ∃ (i : ℝ≥0) (i_1 : ℝ) (_ : ∀ (n : ℕ), ‖p n‖ * (↑i : ℝ) ^ n ≤ i_1), (↑r : ℝ≥0∞) < (↑i : ℝ≥0∞)
⊢ ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
have rcases : ∀ (t : ℝ≥0) (C : ℝ) (hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C) (rt : (↑r : ℝ≥0∞) < (↑t : ℝ≥0∞)),
  ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
Tactic: rcases h with ⟨t, C, hC, rt⟩
Cleared hypotheses: h
-- 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
r : ℝ≥0
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ≥0∞) < (↑t : ℝ≥0∞)
⊢ ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
have rt₁ : (↑r : ℝ) < (↑t : ℝ)
Tactic: rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at rt
Cleared hypotheses: rt
-- 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
r : ℝ≥0
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) < (↑t : ℝ)
⊢ ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
have this₁ : 0 < (↑t : ℝ)
Tactic: have : 0 < (t : ℝ) := r.coe_nonneg.trans_lt rt
-- 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
r : ℝ≥0
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) < (↑t : ℝ)
this : 0 < (↑t : ℝ)
⊢ ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
have rt₁ : (↑r : ℝ) / (↑t : ℝ) < 1
Tactic: rw [← div_lt_one this] at rt
Cleared hypotheses: rt, 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 : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) / (↑t : ℝ) < 1
this : 0 < (↑t : ℝ)
⊢ ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
have refine : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * ((↑r : ℝ) / (↑t : ℝ)) ^ n
Tactic: refine ⟨_, rt, C, Or.inr zero_lt_one, 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
r : ℝ≥0
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) / (↑t : ℝ) < 1
this : 0 < (↑t : ℝ)
n : ℕ
⊢ ‖p n‖ * (↑t : ℝ) ^ n * ((↑r : ℝ) / (↑t : ℝ)) ^ n ≤ C * ((↑r : ℝ) / (↑t : ℝ)) ^ n
have hbc : ‖p n‖ * (↑t : ℝ) ^ n ≤ C
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
r : ℝ≥0
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) / (↑t : ℝ) < 1
this : 0 < (↑t : ℝ)
n : ℕ
⊢ |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * ((↑r : ℝ) / (↑t : ℝ)) ^ n
have n₁ : |‖p n‖ * (↑r : ℝ) ^ n| = ‖p n‖ * (↑t : ℝ) ^ n * ((↑r : ℝ) / (↑t : ℝ)) ^ n
Tactic: calc
    |‖p n‖ * (r : ℝ) ^ n| = ‖p n‖ * (t : ℝ) ^ n * (r / t : ℝ) ^ n := by
      simp [field, abs_mul, div_pow]
    _ ≤ C * (r / t : ℝ) ^ n := by gcongr; apply 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
        IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ a < 1, ∃ (C : ℝ), (0 < C ∨ LT.lt (α := ℝ) 0 1) ∧ ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * (↑t : ℝ) ^ n ≤ C
rt : (↑r : ℝ) / (↑t : ℝ) < 1
this : 0 < (↑t : ℝ)
n : ℕ
n₁ : |‖p n‖ * (↑r : ℝ) ^ n| = ‖p n‖ * (↑t : ℝ) ^ n * ((↑r : ℝ) / (↑t : ℝ)) ^ n
⊢ |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * ((↑r : ℝ) / (↑t : ℝ)) ^ n
have n₂ : ‖p n‖ * (↑t : ℝ) ^ n * ((↑r : ℝ) / (↑t : ℝ)) ^ n ≤ C * ((↑r : ℝ) / (↑t : ℝ)) ^ n
Tactic: calc
    |‖p n‖ * (r : ℝ) ^ n| = ‖p n‖ * (t : ℝ) ^ n * (r / t : ℝ) ^ n := by
      simp [field, abs_mul, div_pow]
    _ ≤ C * (r / t : ℝ) ^ n := by gcongr; apply hC
-- 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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
⊢ ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
have this : ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
Tactic: have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 1 5).mp
    (p.isLittleO_of_lt_radius 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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
this : ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
⊢ ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
have rcases : ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a) (C : ℝ) (hC : C > 0)
  (H : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n),
  ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * (↑r : ℝ) ^ n ≤ C * a ^ n
Tactic: rcases this with ⟨a, ha, C, hC, H⟩
Cleared hypotheses: this
-- 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
r : ℝ≥0
h₀ : r ≠ 0
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a
hp : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x
⊢ (↑r : ℝ≥0∞) < p.radius
have this : (∃ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
      IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
  ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
Tactic: have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * (r : ℝ) ^ n) 1).out 2 5)
-- 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
r : ℝ≥0
h₀ : r ≠ 0
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a
hp : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
⊢ (↑r : ℝ≥0∞) < p.radius
have rcases : ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a) (C : ℝ) (hC : C > 0)
  (hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n), (↑r : ℝ≥0∞) < p.radius
Tactic: rcases this.mp ⟨a, ha, hp⟩ with ⟨a, ha, C, hC, 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
r : ℝ≥0
h₀ : r ≠ 0
a_1 : ℝ
ha_1 : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a_1
hp_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a_1 ^ x
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
⊢ (↑r : ℝ≥0∞) < p.radius
have rw : ∀ (h₀ : 0 < (↑r : ℝ)) {a : ℝ} (ha : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a)
  (hp : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x)
  (this :
    (∃ (a : ℝ),
        Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
          IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
      ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n)
  (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a) (C : ℝ) (hC : C > 0)
  (hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n), (↑r : ℝ≥0∞) < p.radius
Tactic: rw [← pos_iff_ne_zero, ← NNReal.coe_pos] at h₀
Cleared hypotheses: h₀, a_1, ha_1, hp_1, this, a, ha, C, hC, 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
r : ℝ≥0
h₀ : 0 < (↑r : ℝ)
a_1 : ℝ
ha_1 : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a_1
hp_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a_1 ^ x
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
⊢ (↑r : ℝ≥0∞) < p.radius
have lift : ∀ (a : ℝ≥0) (ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) (↑a : ℝ))
  (hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * (↑a : ℝ) ^ n), (↑r : ℝ≥0∞) < p.radius
Tactic: lift a to ℝ≥0 using ha.1.le
Cleared hypotheses: a, ha, hp
-- 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
r : ℝ≥0
h₀ : 0 < (↑r : ℝ)
a_1 : ℝ
ha_1 : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a_1
hp_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a_1 ^ x
this :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) (↑a : ℝ)
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * (↑a : ℝ) ^ n
⊢ (↑r : ℝ≥0∞) < p.radius
have this₁ : (↑r : ℝ) < (↑r : ℝ) / (↑a : ℝ)
Tactic: have : (r : ℝ) < r / a := by
    simpa only [div_one] using (div_lt_div_iff_of_pos_left h₀ zero_lt_one ha.1).2 ha.2
-- 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
r : ℝ≥0
h₀ : 0 < (↑r : ℝ)
a_1 : ℝ
ha_1 : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a_1
hp_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a_1 ^ x
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) (↑a : ℝ)
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * (↑a : ℝ) ^ n
this : (↑r : ℝ) < (↑r : ℝ) / (↑a : ℝ)
⊢ (↑r : ℝ≥0∞) < p.radius
have this₁ : r < r / a
Tactic: norm_cast at this
Cleared hypotheses: this
-- 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
r : ℝ≥0
h₀ : 0 < (↑r : ℝ)
a_1 : ℝ
ha_1 : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a_1
hp_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a_1 ^ x
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) (↑a : ℝ)
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * (↑a : ℝ) ^ n
this : r < r / a
⊢ (↑r : ℝ≥0∞) < p.radius
have this₁ : (↑r : ℝ≥0∞) < (↑(r / a) : ℝ≥0∞)
Tactic: rw [← ENNReal.coe_lt_coe] at this
Cleared hypotheses: 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 : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h₀ : 0 < (↑r : ℝ)
a_1 : ℝ
ha_1 : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a_1
hp_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a_1 ^ x
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) (↑a : ℝ)
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * (↑a : ℝ) ^ n
this : (↑r : ℝ≥0∞) < (↑(r / a) : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) < p.radius
have refine : ∀ (n : ℕ), ‖p n‖ * (↑(r / a) : ℝ) ^ n ≤ C
Tactic: refine this.trans_le (p.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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h₀ : 0 < (↑r : ℝ)
a_1 : ℝ
ha_1 : Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a_1
hp_1 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a_1 ^ x
this_1 :
  (∃ (a : ℝ),
      Membership.mem (γ := Set ℝ) (Ioo (-1) 1) a ∧
        IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) fun (x : ℕ) ↦ a ^ x) ↔
    ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧ ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * a ^ n
C : ℝ
hC : C > 0
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) (↑a : ℝ)
hp : ∀ (n : ℕ), |‖p n‖ * (↑r : ℝ) ^ n| ≤ C * (↑a : ℝ) ^ n
this : (↑r : ℝ≥0∞) < (↑(r / a) : ℝ≥0∞)
n : ℕ
⊢ ‖p n‖ * (↑(r / a) : ℝ) ^ n ≤ C
have rw : ‖p n‖ * (↑r : ℝ) ^ n ≤ C * (↑a : ℝ) ^ n
Tactic: rw [NNReal.coe_div, div_pow, ← mul_div_assoc, div_le_iff₀ (pow_pos ha.1 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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
have obtain : ∀ (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 h
-- 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
x : E
hx : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm.{u_3} (E := F) ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ x : F)
have hx₁ : ‖x‖ₑ < p.radius
Tactic: rw [mem_eball_zero_iff] at hx
Cleared hypotheses: hx
-- 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
x : E
hx : ‖x‖ₑ < p.radius
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ norm.{u_3} (E := F) ((p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ x : F)
have refine : ∀ (n : ℕ), ‖p n‖ * ∏ i : Fin n, ‖x‖ = ‖p n‖ * (↑‖x‖₊ : ℝ) ^ n
Tactic: refine .of_nonneg_of_le
    (fun _ ↦ norm_nonneg _) (fun n ↦ ((p n).le_opNorm _).trans_eq ?_) (p.summable_norm_mul_pow hx)
-- 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
r : ℝ≥0
h : (↑r : ℝ≥0∞) < p.radius
⊢ Summable (α := ℝ≥0) fun (n : ℕ) ↦ ‖p n‖₊ * r ^ n
have rw : Summable (α := ℝ) fun (a : ℕ) ↦ (↑(‖p a‖₊ * r ^ a) : ℝ)
Tactic: rw [← NNReal.summable_coe]
-- 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
⊢ p.radius = ∞ ↔ ∀ (r : ℝ≥0), Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
have mp : p.radius = ∞ → ∀ (r : ℝ≥0), Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
Tactic: constructor
-- 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
mp : p.radius = ∞ → ∀ (r : ℝ≥0), Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
⊢ p.radius = ∞ ↔ ∀ (r : ℝ≥0), Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n
have mpr : (∀ (r : ℝ≥0), Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r : ℝ) ^ n) → p.radius = ∞
Tactic: constructor