awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Polynomial (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CommSemiring A
z : E
inst_4 : NormedCommRing B
inst_5 : NormedAlgebra 𝕜 B
inst_6 : Algebra A B
σ : Type u_5
f : E → σ → B
hf : ∀ (i : σ), AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ f x i) z
p_1 p : MvPolynomial σ A
i : σ
hp : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) p) z
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B) (fun (x : E) ↦ (aeval (f x) : (a : MvPolynomial σ A) → B) (p * X i)) z
have simp_rw : AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := B)
  (fun (x : E) ↦ HMul.hMul (α := B) ((aeval (f x) : (a : MvPolynomial σ A) → B) p : B) (f x i)) z
Tactic: simp_rw [map_mul, aeval_X]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
⊢ (↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1
have this : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have : 0 < (n : ℝ) := Nat.cast_pos.2 hn
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : LT.lt (α := ℝ) 0 (↑n : ℝ)
| (↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)
have rw : ‖p n‖₊ * r ^ n ≤ 1
Tactic: rw [one_div, ENNReal.le_inv_iff_mul_le, ← ENNReal.coe_mul, ENNReal.coe_le_one_iff, one_div, ←
        NNReal.rpow_one r, ← mul_inv_cancel₀ this.ne', NNReal.rpow_mul, ← NNReal.mul_rpow, ←
        NNReal.one_rpow n⁻¹, NNReal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm,
        NNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ (↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1
have conv_lhs : (↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1
Tactic: conv_lhs =>
      rw [one_div, ENNReal.le_inv_iff_mul_le, ← ENNReal.coe_mul, ENNReal.coe_le_one_iff, one_div, ←
        NNReal.rpow_one r, ← mul_inv_cancel₀ this.ne', NNReal.rpow_mul, ← NNReal.mul_rpow, ←
        NNReal.one_rpow n⁻¹, NNReal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm,
        NNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : LT.lt (α := ℝ) 0 (↑n : ℝ)
conv_lhs : (↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1
⊢ (↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1
have conv_lhs₁ : ‖p n‖₊ * r ^ n ≤ 1 ↔ ‖p n‖₊ * r ^ n ≤ 1
Tactic: conv_lhs =>
      rw [one_div, ENNReal.le_inv_iff_mul_le, ← ENNReal.coe_mul, ENNReal.coe_le_one_iff, one_div, ←
        NNReal.rpow_one r, ← mul_inv_cancel₀ this.ne', NNReal.rpow_mul, ← NNReal.mul_rpow, ←
        NNReal.one_rpow n⁻¹, NNReal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm,
        NNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ p.radius = liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
have this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
Tactic: have :
    ∀ (r : ℝ≥0) {n},
      0 < n → ((r : ℝ≥0∞) ≤ 1 / ↑(‖p n‖₊ ^ (1 / (n : ℝ))) ↔ ‖p n‖₊ * r ^ n ≤ 1) := by
    intro r n hn
    have : 0 < (n : ℝ) := Nat.cast_pos.2 hn
    conv_lhs =>
      rw [one_div, ENNReal.le_inv_iff_mul_le, ← ENNReal.coe_mul, ENNReal.coe_le_one_iff, one_div, ←
        NNReal.rpow_one r, ← mul_inv_cancel₀ this.ne', NNReal.rpow_mul, ← NNReal.mul_rpow, ←
        NNReal.one_rpow n⁻¹, NNReal.rpow_le_rpow_iff (inv_pos.2 this), mul_comm,
        NNReal.rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ p.radius = liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
have a : p.radius ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
a : p.radius ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
⊢ p.radius = liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
have a₁ : liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop ≤ p.radius
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ p.radius ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
have a : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < p.radius),
  (↑r : ℝ≥0∞) ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
Tactic: refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop ≤ p.radius
have a : ∀ (r : ℝ≥0) (hr : (↑r : ℝ≥0∞) < liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop),
  (↑r : ℝ≥0∞) ≤ p.radius
Tactic: refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
⊢ (↑r : ℝ≥0∞) ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
have this₁ : ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a ∧ ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
Tactic: have := ((TFAE_exists_lt_isLittleO_pow (fun n => ‖p n‖ * r ^ n) 1).out 1 7).1
      (p.isLittleO_of_lt_radius hr)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this_1 :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
this : ∃ (a : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a ∧ ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
⊢ (↑r : ℝ≥0∞) ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
have a : ∀ (a : ℝ) (ha : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a) (H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n),
  (↑r : ℝ≥0∞) ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
Tactic: obtain ⟨a, ha, H⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
⊢ (↑r : ℝ≥0∞) ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
have a₁ : autoParam
  (IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦
    1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞))
  le_liminf_of_le._auto_1
Tactic: apply le_liminf_of_le
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
a₁ :
  autoParam
    (IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦
      1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞))
    le_liminf_of_le._auto_1
⊢ (↑r : ℝ≥0∞) ≤ liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
have a₂ : ∀ᶠ (n : ℕ) in atTop, (↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)
Tactic: apply le_liminf_of_le
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) a
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n
⊢ ∀ᶠ (b : ℝ≥0∞) in map (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop, (↑r : ℝ≥0∞) ≤ b
have a₁ : ∀ (n : ℕ) (hn₀ : 0 < n) (hn : |‖p n‖ * (↑r : ℝ) ^ n| ≤ a ^ n), (↑(‖p n‖₊ * r ^ n) : ℝ) ≤ (↑1 : ℝ)
Tactic: refine
        H.mp ((eventually_gt_atTop 0).mono fun n hn₀ hn => (this _ hn₀).2 (NNReal.coe_le_coe.1 ?_))
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
⊢ (↑r : ℝ≥0∞) ≤ p.radius
have a : EventuallyLE (β := ℝ) atTop (fun (x : ℕ) ↦ ‖‖p x‖ * (↑r : ℝ) ^ x‖) fun (x : ℕ) ↦ 1
Tactic: refine p.le_radius_of_isBigO <| .of_norm_eventuallyLE ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.RadiusLiminf (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
this :
  ∀ (r : ℝ≥0) {n : ℕ},
    0 < n → ((↑r : ℝ≥0∞) ≤ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < liminf (fun (n : ℕ) ↦ 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) atTop
⊢ EventuallyLE (β := ℝ) atTop (fun (x : ℕ) ↦ ‖‖p x‖ * (↑r : ℝ) ^ x‖) fun (x : ℕ) ↦ 1
have h : ∀ (n : ℕ) (hn : (↑r : ℝ≥0∞) < 1 / (↑(‖p n‖₊ ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞)) (hn₀ : 0 < n),
  ‖‖p n‖ * (↑r : ℝ) ^ n‖ ≤ 1
Tactic: filter_upwards [eventually_lt_of_lt_liminf hr, eventually_gt_atTop 0] with n hn hn₀
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
⊢ Eq.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
have by_contra! : ∀ (hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)), False
Tactic: by_contra! hy
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ IsBigO.{u_1, u_1, u_3} (E := 𝕜) (F := F) (𝓝 0) (fun (c : 𝕜) ↦ c ^ n) fun (c : 𝕜) ↦
    HSMul.hSMul (β := F) (c ^ n) ((p : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ y : F)
have refine : IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : 𝕜) ↦ ‖x ^ n‖) fun (x : 𝕜) ↦
  ‖HSMul.hSMul (β := F) (x ^ n) ((p : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ y : F)‖
Tactic: refine .of_norm_norm ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : 𝕜) ↦ ‖x ^ n‖) fun (x : 𝕜) ↦
    ‖HSMul.hSMul (β := F) (x ^ n) ((p : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ y : F)‖
have simp : IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : 𝕜) ↦ ‖x ^ n‖) fun (x : 𝕜) ↦
  norm.{u_3} (E := F) ((p : (a : (i : Fin n) → E) → F) fun (i : Fin n) ↦ y : F) * ‖x ^ n‖
Tactic: simp only [norm_smul, mul_comm (‖_ ^ _‖)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ IsBigO (E := ℝ) (F := 𝕜) (𝓝 0) (fun (c : 𝕜) ↦ ‖c • y‖ ^ (n + 1)) fun (c : 𝕜) ↦ c ^ (n + 1)
have refine : IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (c : 𝕜) ↦ ‖c • y‖ ^ (n + 1)) fun (x : 𝕜) ↦ ‖x ^ (n + 1)‖
Tactic: refine .of_norm_right ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (c : 𝕜) ↦ ‖c • y‖ ^ (n + 1)) fun (x : 𝕜) ↦ ‖x ^ (n + 1)‖
have simp : IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (c : 𝕜) ↦ ‖y‖ ^ (n + 1) * ‖c‖ ^ (n + 1)) fun (x : 𝕜) ↦ ‖x‖ ^ (n + 1)
Tactic: simp only [norm_smul, mul_pow, mul_comm _ ‖y‖, norm_pow]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
⊢ False
have this : IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (c : 𝕜) ↦ c ^ n) fun (c : 𝕜) ↦ c ^ n
Tactic: have : (fun c : 𝕜 ↦ c ^ n) =o[𝓝 0] (fun c : 𝕜 ↦ c ^ n) := calc
    (fun c : 𝕜 ↦ c ^ n) =O[𝓝 0] fun c ↦ c ^ n • p fun i ↦ y := by
      refine .of_norm_norm ?_
      simp only [norm_smul, mul_comm (‖_ ^ _‖)]
      exact .const_mul_right (by simpa) (isBigO_refl ..)
    _ = fun c ↦ p fun _ ↦ c • y := by simp [p.map_smul_univ]
    _ =O[𝓝 0] fun c ↦ ‖c • y‖ ^ (n + 1) :=
      h.comp_tendsto <| Continuous.tendsto' (by fun_prop) _ _ (zero_smul _ _)
    _ =O[𝓝 0] fun c ↦ c ^ (n + 1) := by
      refine .of_norm_right ?_
      simp only [norm_smul, mul_pow, mul_comm _ ‖y‖, norm_pow]
      exact .const_mul_left (isBigO_refl ..) _
    _ =o[𝓝 0] (· ^ n) := isLittleO_pow_pow (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ
p : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin n) ↦ E) F
h :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 0) (fun (y : E) ↦ (p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    fun (y : E) ↦ ‖y‖ ^ (n + 1)
y : E
hy : Ne.{u_3 + 1} (α := F) ((p : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
this : IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 0) (fun (c : 𝕜) ↦ c ^ n) fun (c : 𝕜) ↦ c ^ n
⊢ False
have refine : ∃ᶠ (x : 𝕜) in 𝓝 0, x ≠ 0
Tactic: refine isLittleO_irrefl (.mono ?_ fun _ ↦ pow_ne_zero n) this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n : ℕ
⊢ ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) (0 : F)
have refine : ∀ (k : ℕ)
  (hk : ∀ m < k, ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F))
  (y : E), Eq.{u_3 + 1} (α := F) ((p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y : F) (0 : F)
Tactic: refine Nat.strong_induction_on n fun k hk => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)
⊢ p.partialSum (k + 1) = fun (y : E) ↦ (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y
have h₁ : ∀ (z : E), p.partialSum (k + 1) z = (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ z
Tactic: funext z
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)
z : E
⊢ p.partialSum (k + 1) z = (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ z
have h₁ : ∀ (b : ℕ) (hb : b ∈ Finset.range (k + 1)) (hnb : b ≠ k),
  Eq.{u_3 + 1} (α := F) ((p b : (a : (i : Fin b) → E) → F) fun (x : Fin b) ↦ z : F) (0 : F)
Tactic: refine Finset.sum_eq_single _ (fun b hb hnb => ?_) fun hn => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)
z : E
h₁ :
  ∀ (b : ℕ) (hb : b ∈ Finset.range (k + 1)) (hnb : b ≠ k),
    Eq.{u_3 + 1} (α := F) ((p b : (a : (i : Fin b) → E) → F) fun (x : Fin b) ↦ z : F) (0 : F)
⊢ p.partialSum (k + 1) z = (p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ z
have h₂ : ∀ (hn : k ∉ Finset.range (k + 1)),
  Eq.{u_3 + 1} (α := F) ((p k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ z : F) (0 : F)
Tactic: refine Finset.sum_eq_single _ (fun b hb hnb => ?_) fun hn => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Uniqueness (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)
z : E
b : ℕ
hb : b ∈ Finset.range (k + 1)
hnb : b ≠ k
⊢ Eq.{u_3 + 1} (α := F) ((p b : (a : (i : Fin b) → E) → F) fun (x : Fin b) ↦ z : F) (0 : F)
have this : b ≤ k
Tactic: have := Finset.mem_range_succ_iff.mp hb