awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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_1 :
  ∀ (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)
h : f = 1
⊢ False

Tactic:
simp [h] at ha
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
suffices :
  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

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
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
⊢ Eq (α := ℝ) (Multiset.prod (Multiset.map (fun (x : K) ↦ (NormedField.toMulRingNorm K : (a : K) → ℝ) (a - x)) g.roots))
    (Multiset.prod (Multiset.map (fun (x : K) ↦ (NormedField.toMulRingNorm K : (a : K) → ℝ) (a - x)) g.roots))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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 :
  (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))
⊢ 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))

Tactic:
rw [g.roots.prod_hom' (NormedField.toMulRingNorm K) (fun x : K ↦ a - x)]

Premises used: Polynomial.roots, HSub.hSub, NormedField.toMulRingNorm, Multiset.prod_hom'
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
⊢ (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:
rfl
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
e_a : Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots) = eval a g
⊢ norm (E := K) (Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots)) = ‖eval a g‖

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
e_a 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))
⊢ Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots) = eval a g

Tactic:
rw [hg.eval_eq_prod_roots_of_monic hgm]

Premises used: Polynomial.Splits.eval_eq_prod_roots_of_monic
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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 g - eval a f‖ + ‖eval a f‖

Tactic:
norm_add_le (g.eval a - f.eval a) (f.eval a)

Premises used: Polynomial.eval, HSub.hSub, norm_add_le
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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 : eval a g = eval a g - eval a f + eval a f
⊢ ‖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)

Premises used: Polynomial.eval, HSub.hSub, norm_add_le
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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 (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))‖
⊢ ‖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))‖

Tactic:
rw [← eval_sub]

Premises used: Polynomial.eval_sub
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
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))‖
⊢ ‖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:
simp only [ha, norm_zero, add_zero]

Premises used: norm_zero, add_zero
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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))‖
rw₁ : (g - f).natDegree < g.natDegree + 1
⊢ ‖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:
rw [(g - f).as_sum_range' (g.natDegree + 1)]

Premises used: HSub.hSub, Polynomial.as_sum_range', HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
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)
⊢ ‖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:
congr
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
⊢ 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:
simp [← C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
⊢ (g - f).natDegree < g.natDegree + 1

Tactic:
simpa [hdeg, Nat.lt_succ_iff] using g.natDegree_sub_le f

Premises used: Nat.lt_succ_iff, Polynomial.natDegree_sub_le
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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.{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)
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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 :
  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))‖
⊢ ‖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‖

Tactic:
simpa [eval_mul, eval_finsetSum] using this

Premises used: Polynomial.eval_mul, Polynomial.eval_finsetSum
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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 :
  ∑ 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 : ℝ)
⊢ ∑ 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 : ℝ)

Tactic:
rw [hdeg]
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
⊢ LT.lt (α := ℝ) (∑ i ∈ Finset.range (f.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖)
    (∑ i ∈ Finset.range (f.natDegree + 1), (fun (i : ℕ) ↦ ε * max ‖a‖ 1 ^ f.natDegree) i)

Tactic:
Finset.sum_lt_sum_of_nonempty (g := fun i ↦ ε * (‖a‖ ⊔ 1) ^ ↑f.natDegree)
        (Finset.nonempty_range_add_one) ?_

Premises used: Finset.nonempty_range_add_one, Finset.sum_lt_sum_of_nonempty
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
convert_3 :
  ∀ i ∈ Finset.range (f.natDegree + 1),
    ‖(g.coeff i - f.coeff i) * a ^ i‖ < (fun (i : ℕ) ↦ ε * max ‖a‖ 1 ^ f.natDegree) i
⊢ ∑ 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:
convert!
      Finset.sum_lt_sum_of_nonempty (g := fun i ↦ ε * (‖a‖ ⊔ 1) ^ ↑f.natDegree)
        (Finset.nonempty_range_add_one) ?_

Premises used: Finset.nonempty_range_add_one, Finset.sum_lt_sum_of_nonempty
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
⊢ HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ) =
    ∑ i ∈ Finset.range (f.natDegree + 1), ε * max ‖a‖ 1 ^ f.natDegree

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
convert_3 : ∀ i < f.natDegree + 1, ‖g.coeff i - f.coeff i‖ * ‖a‖ ^ i < ε * max ‖a‖ 1 ^ f.natDegree
⊢ ∀ i ∈ Finset.range (f.natDegree + 1),
    ‖(g.coeff i - f.coeff i) * a ^ i‖ < (fun (i : ℕ) ↦ ε * max ‖a‖ 1 ^ f.natDegree) i

Tactic:
simp only [Finset.mem_range, norm_mul, norm_pow]

Premises used: norm_pow, norm_mul, Finset.mem_range
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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‖
convert_3₃ : 0 < max ‖a‖ 1 ^ f.natDegree
⊢ ‖g.coeff i - f.coeff i‖ * ‖a‖ ^ i < ε * max ‖a‖ 1 ^ f.natDegree

Tactic:
apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos

Premises used: mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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‖ < ε

Tactic:
simpa [← map_sub] using hcoeff i

Premises used: map_sub
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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

Tactic:
(pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_

Premises used: Norm.norm, pow_le_pow_left₀, LE.le.trans, OfNat.ofNat, le_max_left, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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 : max ‖a‖ 1 ^ i ≤ max ‖a‖ 1 ^ f.natDegree
⊢ ‖a‖ ^ i ≤ max ‖a‖ 1 ^ f.natDegree

Tactic:
refine (pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_

Premises used: Norm.norm, pow_le_pow_left₀, LE.le.trans, OfNat.ofNat, le_max_left, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
⊢ max ‖a‖ 1 ^ i ≤ max ‖a‖ 1 ^ f.natDegree

Tactic:
pow_le_pow_right₀ (le_max_right ‖a‖ 1) (Nat.le_of_lt_succ hi)

Premises used: le_max_right, Norm.norm, pow_le_pow_right₀, Nat.le_of_lt_succ, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
⊢ max ‖a‖ 1 ^ i ≤ max ‖a‖ 1 ^ f.natDegree

Tactic:
exact pow_le_pow_right₀ (le_max_right ‖a‖ 1) (Nat.le_of_lt_succ hi)

Premises used: le_max_right, Norm.norm, pow_le_pow_right₀, Nat.le_of_lt_succ, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
⊢ 0 ≤ ‖g.coeff i - f.coeff i‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
⊢ 0 < max ‖a‖ 1 ^ f.natDegree

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
f g : K[X]
ε : ℝ
hε : 0 < ε
a : L
ha : Eq.{u_2 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : Splits (map (algebraMap K L) g)
⊢ eval a (map (algebraMap K L) f) = 0

Tactic:
simpa using ha
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
f g : K[X]
ε : ℝ
hε : 0 < ε
a : L
ha : Eq.{u_2 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : Splits (map (algebraMap K L) g)
⊢ natDegree (map (algebraMap K L) g) = natDegree (map (algebraMap K L) f)

Tactic:
simpa using hdeg
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
f g : K[X]
ε : ℝ
hε : 0 < ε
a : L
ha : Eq.{u_2 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : Splits (map (algebraMap K L) g)
⊢ ∀ (i : ℕ), ‖coeff (map (algebraMap K L) g) i - coeff (map (algebraMap K L) f) i‖ < ε

Tactic:
simpa [← map_sub] using hcoeff

Premises used: map_sub
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
f g : K[X]
ε : ℝ
hε : 0 < ε
a : L
ha : Eq.{u_2 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : Splits (map (algebraMap K L) g)
obtain :
  ∀ (b : L) (h1 : b ∈ roots (map (algebraMap K L) g))
    (h2 :
      ‖a - b‖ <
        HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑(natDegree (map (algebraMap K L) f)) : ℝ) 1 * ε)
            (↑(natDegree (map (algebraMap K L) f)) : ℝ)⁻¹ *
          max ‖a‖ 1),
    ∃ b ∈ g.aroots L,
      ‖a - b‖ < HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1
⊢ ∃ b ∈ g.aroots L,
    ‖a - b‖ < HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1

Tactic:
obtain ⟨b, h1, h2⟩ := exists_roots_norm_sub_lt_of_norm_coeff_sub_lt hε
      (f := f.map (algebraMap K L)) (by simpa using ha) (hfm.map _) (hgm.map _)
      (by simpa using hdeg) (by simpa [← map_sub] using hcoeff) hg

Premises used: Polynomial.exists_roots_norm_sub_lt_of_norm_coeff_sub_lt, Polynomial.Monic.map
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
f g : K[X]
ε : ℝ
hε : 0 < ε
a : L
ha : Eq.{u_2 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : Splits (map (algebraMap K L) g)
b : L
h1 : b ∈ roots (map (algebraMap K L) g)
h2 :
  ‖a - b‖ <
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑(natDegree (map (algebraMap K L) f)) : ℝ) 1 * ε)
        (↑(natDegree (map (algebraMap K L) f)) : ℝ)⁻¹ *
      max ‖a‖ 1
right : ‖a - b‖ < HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1
⊢ ∃ b ∈ g.aroots L,
    ‖a - b‖ < HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1

Tactic:
use b, h1
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
L : Type u_2
inst : NormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
f g : K[X]
ε : ℝ
hε : 0 < ε
a : L
ha : Eq.{u_2 + 1} (α := L) ((aeval a : (a : K[X]) → L) f : L) (0 : L)
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : Splits (map (algebraMap K L) g)
b : L
h1 : b ∈ roots (map (algebraMap K L) g)
h2 :
  ‖a - b‖ <
    HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑(natDegree (map (algebraMap K L) f)) : ℝ) 1 * ε)
        (↑(natDegree (map (algebraMap K L) f)) : ℝ)⁻¹ *
      max ‖a‖ 1
⊢ ‖a - b‖ < HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1

Tactic:
simpa using h2