awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.UnitizationL1 (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖y.ofLp.toProd.1 • x.ofLp.toProd.2 + x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖
have h₂ : ‖y.ofLp.toProd.1 • x.ofLp.toProd.2‖ + ‖x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
  ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖
Tactic: apply (norm_add_le _ _).trans
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.UnitizationL1 (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
⊢ ‖y.ofLp.toProd.1 • x.ofLp.toProd.2‖ + ‖x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖
have h₂ : ‖y.ofLp.toProd.1 • x.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.UnitizationL1 (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
x y : WithLp 1 (Unitization 𝕜 A)
h₂ : ‖y.ofLp.toProd.1 • x.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖
⊢ ‖y.ofLp.toProd.1 • x.ofLp.toProd.2‖ + ‖x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤
    ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.1‖ + ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖
have h₃ : ‖x.ofLp.toProd.2 * y.ofLp.toProd.2‖ ≤ ‖x.ofLp.toProd.2‖ * ‖y.ofLp.toProd.2‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.UnitizationL1 (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : NormedSpace 𝕜 A
inst_3 : IsScalarTower 𝕜 A A
inst_4 : SMulCommClass 𝕜 A A
r : 𝕜
x : WithLp 1 (Unitization 𝕜 A)
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
have simp_rw : ‖r‖ * ‖x.ofLp.toProd.1‖ + ‖r‖ * ‖x.ofLp.toProd.2‖ ≤ ‖r‖ * ‖x.ofLp.toProd.1‖ + ‖r‖ * ‖x.ofLp.toProd.2‖
Tactic: simp_rw [unitization_norm_def, ofLp_smul, fst_smul, snd_smul, norm_smul, mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
⊢ ∃ b ∈ g.roots,
    ‖a - b‖ < HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1
have by_contra! : ∀
  (h :
    ∀ (b : K) (_ : b ∈ g.roots),
      HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖),
  False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (hypothesis)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
⊢ False
have this₁ : LE.le (α := ℝ)
  (Multiset.prod
    (Multiset.map
      (fun (b : K) ↦ HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1)
      g.roots))
  (Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots))
Tactic: have := Multiset.prod_map_le_prod_map₀ (fun b ↦ ((f.natDegree + 1) * ε) ^ (f.natDegree : ℝ)⁻¹ *
        (‖a‖ ⊔ 1)) (fun b ↦ ‖a - b‖) (by intros; positivity) h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (hypothesis)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this_1 :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  LE.le (α := ℝ)
    (Multiset.prod
      (Multiset.map
        (fun (b : K) ↦
          HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1)
        g.roots))
    (Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots))
⊢ False
have this₁ : (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) ^ HMul.hMul (α := ℝ) (↑f.natDegree : ℝ)⁻¹ (↑f.natDegree : ℝ) *
    HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) ≤
  Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)
Tactic: simp only [Multiset.map_const', hg.natDegree_eq_card_roots.symm ▸ hdeg, Multiset.prod_replicate,
      mul_pow, ← Real.rpow_natCast,
      ← Real.rpow_mul (by positivity : ((f.natDegree + 1) * ε) > 0).le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this_1 :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) ^ HMul.hMul (α := ℝ) (↑f.natDegree : ℝ)⁻¹ (↑f.natDegree : ℝ) *
      HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) ≤
    Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)
⊢ False
have rw : ∀
  (this :
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) ≤
      Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)),
  False
Tactic: rw [inv_mul_cancel₀, Real.rpow_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this_1 :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) ^ HMul.hMul (α := ℝ) (↑f.natDegree : ℝ)⁻¹ (↑f.natDegree : ℝ) *
      HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) ≤
    Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)
rw :
  ∀
    (this :
      HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) ≤
        Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)),
    False
⊢ False
have rw₁ : Ne (α := ℝ) (↑f.natDegree : ℝ) 0
Tactic: rw [inv_mul_cancel₀, Real.rpow_one] at this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this_1 :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) ≤
    Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)
⊢ False
have linarith : Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) -
      HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) +
    (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) -
      Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)) =
  0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this_1 :
  Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
h :
  ∀ (b : K) (_ : b ∈ g.roots),
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) ^ HMul.hMul (α := ℝ) (↑f.natDegree : ℝ)⁻¹ (↑f.natDegree : ℝ) *
      HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) ≤
    Multiset.prod (Multiset.map (fun (b : K) ↦ ‖a - b‖) g.roots)
⊢ Ne (α := ℝ) (↑f.natDegree : ℝ) 0
have simp : ¬f = 1
Tactic: simp only [ne_eq, Nat.cast_eq_zero, hfm, Monic.natDegree_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ∃ b ∈ g.roots,
    ‖a - b‖ < HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1
have suffices : Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
  HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
Tactic: suffices this : (g.roots.map fun x => ‖a - x‖).prod <
      ((f.natDegree + 1) * ε) * (max ‖a‖ 1) ^ (f.natDegree : ℝ) by
    by_contra! h
    have := Multiset.prod_map_le_prod_map₀ (fun b ↦ ((f.natDegree + 1) * ε) ^ (f.natDegree : ℝ)⁻¹ *
        (‖a‖ ⊔ 1)) (fun b ↦ ‖a - b‖) (by intros; positivity) h
    simp only [Multiset.map_const', hg.natDegree_eq_card_roots.symm ▸ hdeg, Multiset.prod_replicate,
      mul_pow, ← Real.rpow_natCast,
      ← Real.rpow_mul (by positivity : ((f.natDegree + 1) * ε) > 0).le] at this
    rw [inv_mul_cancel₀, Real.rpow_one] at this
    · linarith
    · simp only [ne_eq, Nat.cast_eq_zero, hfm, Monic.natDegree_eq_zero]
      intro h
      simp [h] at ha
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ Multiset.prod (Multiset.map (fun (x : K) ↦ (NormedField.toMulRingNorm K : (a : K) → ℝ) (a - x)) g.roots) =
    norm (E := K) (Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots))
have rw : (NormedField.toMulRingNorm K : (a : K) → ℝ) (Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots)) =
  norm (E := K) (Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots))
Tactic: rw [g.roots.prod_hom' (NormedField.toMulRingNorm K) (fun x : K ↦ a - x)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ norm (E := K) (Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots)) = ‖eval a g‖
have e_a : Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots) = eval a g
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots) = eval a g
have e_a : Eq (α := K) (Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots))
  (Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots))
Tactic: rw [hg.eval_eq_prod_roots_of_monic hgm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ‖eval a g‖ ≤ ‖eval a g - eval a f‖ + ‖eval a f‖
have h : eval a g = eval a g - eval a f + eval a f
Tactic: convert! norm_add_le (g.eval a - f.eval a) (f.eval a)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ‖eval a g - eval a f‖ + ‖eval a f‖ =
    ‖eval a
        (∑ i ∈ Finset.range (g.natDegree + 1),
          HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i))‖
have rw : ‖eval a (g - f)‖ + ‖eval a f‖ =
  ‖eval a
      (∑ i ∈ Finset.range (g.natDegree + 1),
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i))‖
Tactic: rw [← eval_sub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ‖eval a (g - f)‖ + ‖eval a f‖ =
    ‖eval a
        (∑ i ∈ Finset.range (g.natDegree + 1),
          HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i))‖
have simp : ‖eval a (g - f)‖ =
  ‖eval a
      (∑ i ∈ Finset.range (g.natDegree + 1),
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i))‖
Tactic: simp only [ha, norm_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ‖eval a (g - f)‖ =
    ‖eval a
        (∑ i ∈ Finset.range (g.natDegree + 1),
          HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i))‖
have rw : ‖eval a (∑ i ∈ Finset.range (g.natDegree + 1), (monomial i : (a : K) → K[X]) ((g - f).coeff i))‖ =
  ‖eval a
      (∑ i ∈ Finset.range (g.natDegree + 1),
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i))‖
Tactic: rw [(g - f).as_sum_range' (g.natDegree + 1)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
rw :
  ‖eval a (∑ i ∈ Finset.range (g.natDegree + 1), (monomial i : (a : K) → K[X]) ((g - f).coeff i))‖ =
    ‖eval a
        (∑ i ∈ Finset.range (g.natDegree + 1),
          HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i))‖
⊢ ‖eval a (g - f)‖ =
    ‖eval a
        (∑ i ∈ Finset.range (g.natDegree + 1),
          HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i))‖
have rw₁ : (g - f).natDegree < g.natDegree + 1
Tactic: rw [(g - f).as_sum_range' (g.natDegree + 1)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ‖eval a (∑ i ∈ Finset.range (g.natDegree + 1), (monomial i : (a : K) → K[X]) ((g - f).coeff i))‖ =
    ‖eval a
        (∑ i ∈ Finset.range (g.natDegree + 1),
          HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i))‖
have e_a : Eq.{u_1 + 1} (α := ℕ → K[X]) (fun (i : ℕ) ↦ (monomial i : (a : K) → K[X]) ((g - f).coeff i)) fun (i : ℕ) ↦
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (hypothesis)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ‖eval a
        (∑ i ∈ Finset.range (g.natDegree + 1),
          HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i))‖ ≤
    ∑ i ∈ Finset.range (g.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖
have this : norm.{u_1} (E := K)
    (∑ i ∈ Finset.range (g.natDegree + 1),
      eval a
        (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i))) ≤
  ∑ i ∈ Finset.range (g.natDegree + 1),
    ‖eval a (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g.coeff i - f.coeff i) : K[X]) (HPow.hPow (α := K[X]) X i))‖
Tactic: have := norm_sum_le (Finset.range (g.natDegree + 1))
        (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ∑ i ∈ Finset.range (g.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
have rw : ∑ i ∈ Finset.range (f.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ <
  HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
Tactic: rw [hdeg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ∑ i ∈ Finset.range (f.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
have h : HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) =
  ∑ i ∈ Finset.range (f.natDegree + 1), ε * max ‖a‖ 1 ^ f.natDegree
Tactic: convert!
      Finset.sum_lt_sum_of_nonempty (g := fun i ↦ ε * (‖a‖ ⊔ 1) ^ ↑f.natDegree)
        (Finset.nonempty_range_add_one) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
h :
  HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) =
    ∑ i ∈ Finset.range (f.natDegree + 1), ε * max ‖a‖ 1 ^ f.natDegree
⊢ ∑ i ∈ Finset.range (f.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
have convert_3 : ∀ i ∈ Finset.range (f.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ < (fun (i : ℕ) ↦ ε * max ‖a‖ 1 ^ f.natDegree) i
Tactic: convert!
      Finset.sum_lt_sum_of_nonempty (g := fun i ↦ ε * (‖a‖ ⊔ 1) ^ ↑f.natDegree)
        (Finset.nonempty_range_add_one) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
⊢ ∀ i ∈ Finset.range (f.natDegree + 1),
    ‖(g.coeff i - f.coeff i) * a ^ i‖ < (fun (i : ℕ) ↦ ε * max ‖a‖ 1 ^ f.natDegree) i
have convert_3 : ∀ i < f.natDegree + 1, ‖g.coeff i - f.coeff i‖ * ‖a‖ ^ i < ε * max ‖a‖ 1 ^ f.natDegree
Tactic: simp only [Finset.mem_range, norm_mul, norm_pow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
i : ℕ
hi : i < f.natDegree + 1
⊢ ‖g.coeff i - f.coeff i‖ * ‖a‖ ^ i < ε * max ‖a‖ 1 ^ f.natDegree
have convert_3 : ‖g.coeff i - f.coeff i‖ < ε
Tactic: apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
i : ℕ
hi : i < f.natDegree + 1
convert_3 : ‖g.coeff i - f.coeff i‖ < ε
⊢ ‖g.coeff i - f.coeff i‖ * ‖a‖ ^ i < ε * max ‖a‖ 1 ^ f.natDegree
have convert_3₁ : ‖a‖ ^ i ≤ max ‖a‖ 1 ^ f.natDegree
Tactic: apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
i : ℕ
hi : i < f.natDegree + 1
convert_3 : ‖g.coeff i - f.coeff i‖ < ε
convert_3₁ : ‖a‖ ^ i ≤ max ‖a‖ 1 ^ f.natDegree
⊢ ‖g.coeff i - f.coeff i‖ * ‖a‖ ^ i < ε * max ‖a‖ 1 ^ f.natDegree
have convert_3₂ : 0 ≤ ‖g.coeff i - f.coeff i‖
Tactic: apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
i : ℕ
hi : i < f.natDegree + 1
convert_3 : ‖g.coeff i - f.coeff i‖ < ε
convert_3₁ : ‖a‖ ^ i ≤ max ‖a‖ 1 ^ f.natDegree
convert_3₂ : 0 ≤ ‖g.coeff i - f.coeff i‖
⊢ ‖g.coeff i - f.coeff i‖ * ‖a‖ ^ i < ε * max ‖a‖ 1 ^ f.natDegree
have convert_3₃ : 0 < max ‖a‖ 1 ^ f.natDegree
Tactic: apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
inst : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
i : ℕ
hi : i < f.natDegree + 1
⊢ ‖a‖ ^ i ≤ max ‖a‖ 1 ^ f.natDegree
have convert_3 : max ‖a‖ 1 ^ i ≤ max ‖a‖ 1 ^ f.natDegree
Tactic: refine (pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_