awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
have _ : 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: calc
  _ = (g.roots.map (fun x ↦ NormedField.toMulRingNorm K (a - x))).prod := rfl
  _ = ‖(g.roots.map (fun x ↦ a - x)).prod‖ := by
    rw [g.roots.prod_hom' (NormedField.toMulRingNorm K) (fun x : K ↦ a - x)]
    rfl
  _ = ‖g.eval a‖ := by
    congr
    rw [hg.eval_eq_prod_roots_of_monic hgm]
  _ ≤ ‖g.eval a - f.eval a‖ + ‖f.eval a‖ := by
    convert! norm_add_le (g.eval a - f.eval a) (f.eval a)
    simp
  _ = ‖(∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i - f.coeff i) * X ^ i).eval a‖ := by
    rw [← eval_sub]
    simp only [ha, norm_zero, add_zero]
    rw [(g - f).as_sum_range' (g.natDegree + 1)]
    · congr
      simp [← C_mul_X_pow_eq_monomial]
    · simpa [hdeg, Nat.lt_succ_iff] using g.natDegree_sub_le f
  _ ≤ ∑ i ∈ Finset.range (g.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ := by
    have := norm_sum_le (Finset.range (g.natDegree + 1))
        (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
    simpa [eval_mul, eval_finsetSum] using this
    -- The following tactic does not work here:
    -- simpa [eval_mul, eval_finsetSum] using norm_sum_le (Finset.range (g.natDegree + 1))
    --     (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
  _ < _ := by
    rw [hdeg]
    convert!
      Finset.sum_lt_sum_of_nonempty (g := fun i ↦ ε * (‖a‖ ⊔ 1) ^ ↑f.natDegree)
        (Finset.nonempty_range_add_one) ?_
    · simp [mul_assoc]
    · simp only [Finset.mem_range, norm_mul, norm_pow]
      intro i hi
      apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
      · simpa [← map_sub] using hcoeff i
      · refine (pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_
        exact pow_le_pow_right₀ (le_max_right ‖a‖ 1) (Nat.le_of_lt_succ hi)
      all_goals positivity
-- 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))
⊢ Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
have _₁ : norm (E := K) (Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots)) = ‖eval a g‖
Tactic: calc
  _ = (g.roots.map (fun x ↦ NormedField.toMulRingNorm K (a - x))).prod := rfl
  _ = ‖(g.roots.map (fun x ↦ a - x)).prod‖ := by
    rw [g.roots.prod_hom' (NormedField.toMulRingNorm K) (fun x : K ↦ a - x)]
    rfl
  _ = ‖g.eval a‖ := by
    congr
    rw [hg.eval_eq_prod_roots_of_monic hgm]
  _ ≤ ‖g.eval a - f.eval a‖ + ‖f.eval a‖ := by
    convert! norm_add_le (g.eval a - f.eval a) (f.eval a)
    simp
  _ = ‖(∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i - f.coeff i) * X ^ i).eval a‖ := by
    rw [← eval_sub]
    simp only [ha, norm_zero, add_zero]
    rw [(g - f).as_sum_range' (g.natDegree + 1)]
    · congr
      simp [← C_mul_X_pow_eq_monomial]
    · simpa [hdeg, Nat.lt_succ_iff] using g.natDegree_sub_le f
  _ ≤ ∑ i ∈ Finset.range (g.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ := by
    have := norm_sum_le (Finset.range (g.natDegree + 1))
        (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
    simpa [eval_mul, eval_finsetSum] using this
    -- The following tactic does not work here:
    -- simpa [eval_mul, eval_finsetSum] using norm_sum_le (Finset.range (g.natDegree + 1))
    --     (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
  _ < _ := by
    rw [hdeg]
    convert!
      Finset.sum_lt_sum_of_nonempty (g := fun i ↦ ε * (‖a‖ ⊔ 1) ^ ↑f.natDegree)
        (Finset.nonempty_range_add_one) ?_
    · simp [mul_assoc]
    · simp only [Finset.mem_range, norm_mul, norm_pow]
      intro i hi
      apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
      · simpa [← map_sub] using hcoeff i
      · refine (pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_
        exact pow_le_pow_right₀ (le_max_right ‖a‖ 1) (Nat.le_of_lt_succ hi)
      all_goals positivity
-- 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))
_₁ : norm (E := K) (Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots)) = ‖eval a g‖
⊢ Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
have _₂ : ‖eval a g‖ ≤ ‖eval a g - eval a f‖ + ‖eval a f‖
Tactic: calc
  _ = (g.roots.map (fun x ↦ NormedField.toMulRingNorm K (a - x))).prod := rfl
  _ = ‖(g.roots.map (fun x ↦ a - x)).prod‖ := by
    rw [g.roots.prod_hom' (NormedField.toMulRingNorm K) (fun x : K ↦ a - x)]
    rfl
  _ = ‖g.eval a‖ := by
    congr
    rw [hg.eval_eq_prod_roots_of_monic hgm]
  _ ≤ ‖g.eval a - f.eval a‖ + ‖f.eval a‖ := by
    convert! norm_add_le (g.eval a - f.eval a) (f.eval a)
    simp
  _ = ‖(∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i - f.coeff i) * X ^ i).eval a‖ := by
    rw [← eval_sub]
    simp only [ha, norm_zero, add_zero]
    rw [(g - f).as_sum_range' (g.natDegree + 1)]
    · congr
      simp [← C_mul_X_pow_eq_monomial]
    · simpa [hdeg, Nat.lt_succ_iff] using g.natDegree_sub_le f
  _ ≤ ∑ i ∈ Finset.range (g.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ := by
    have := norm_sum_le (Finset.range (g.natDegree + 1))
        (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
    simpa [eval_mul, eval_finsetSum] using this
    -- The following tactic does not work here:
    -- simpa [eval_mul, eval_finsetSum] using norm_sum_le (Finset.range (g.natDegree + 1))
    --     (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
  _ < _ := by
    rw [hdeg]
    convert!
      Finset.sum_lt_sum_of_nonempty (g := fun i ↦ ε * (‖a‖ ⊔ 1) ^ ↑f.natDegree)
        (Finset.nonempty_range_add_one) ?_
    · simp [mul_assoc]
    · simp only [Finset.mem_range, norm_mul, norm_pow]
      intro i hi
      apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
      · simpa [← map_sub] using hcoeff i
      · refine (pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_
        exact pow_le_pow_right₀ (le_max_right ‖a‖ 1) (Nat.le_of_lt_succ hi)
      all_goals positivity
-- 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))
_₁ : norm (E := K) (Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots)) = ‖eval a g‖
_₂ : ‖eval a g‖ ≤ ‖eval a g - eval a f‖ + ‖eval a f‖
⊢ Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
have _₃ : ‖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: calc
  _ = (g.roots.map (fun x ↦ NormedField.toMulRingNorm K (a - x))).prod := rfl
  _ = ‖(g.roots.map (fun x ↦ a - x)).prod‖ := by
    rw [g.roots.prod_hom' (NormedField.toMulRingNorm K) (fun x : K ↦ a - x)]
    rfl
  _ = ‖g.eval a‖ := by
    congr
    rw [hg.eval_eq_prod_roots_of_monic hgm]
  _ ≤ ‖g.eval a - f.eval a‖ + ‖f.eval a‖ := by
    convert! norm_add_le (g.eval a - f.eval a) (f.eval a)
    simp
  _ = ‖(∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i - f.coeff i) * X ^ i).eval a‖ := by
    rw [← eval_sub]
    simp only [ha, norm_zero, add_zero]
    rw [(g - f).as_sum_range' (g.natDegree + 1)]
    · congr
      simp [← C_mul_X_pow_eq_monomial]
    · simpa [hdeg, Nat.lt_succ_iff] using g.natDegree_sub_le f
  _ ≤ ∑ i ∈ Finset.range (g.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ := by
    have := norm_sum_le (Finset.range (g.natDegree + 1))
        (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
    simpa [eval_mul, eval_finsetSum] using this
    -- The following tactic does not work here:
    -- simpa [eval_mul, eval_finsetSum] using norm_sum_le (Finset.range (g.natDegree + 1))
    --     (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
  _ < _ := by
    rw [hdeg]
    convert!
      Finset.sum_lt_sum_of_nonempty (g := fun i ↦ ε * (‖a‖ ⊔ 1) ^ ↑f.natDegree)
        (Finset.nonempty_range_add_one) ?_
    · simp [mul_assoc]
    · simp only [Finset.mem_range, norm_mul, norm_pow]
      intro i hi
      apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
      · simpa [← map_sub] using hcoeff i
      · refine (pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_
        exact pow_le_pow_right₀ (le_max_right ‖a‖ 1) (Nat.le_of_lt_succ hi)
      all_goals positivity
-- 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))
_₁ : norm (E := K) (Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots)) = ‖eval a g‖
_₂ : ‖eval a g‖ ≤ ‖eval a g - eval a f‖ + ‖eval a f‖
_₃ :
  ‖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))‖
⊢ Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
have _₄ : ‖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: calc
  _ = (g.roots.map (fun x ↦ NormedField.toMulRingNorm K (a - x))).prod := rfl
  _ = ‖(g.roots.map (fun x ↦ a - x)).prod‖ := by
    rw [g.roots.prod_hom' (NormedField.toMulRingNorm K) (fun x : K ↦ a - x)]
    rfl
  _ = ‖g.eval a‖ := by
    congr
    rw [hg.eval_eq_prod_roots_of_monic hgm]
  _ ≤ ‖g.eval a - f.eval a‖ + ‖f.eval a‖ := by
    convert! norm_add_le (g.eval a - f.eval a) (f.eval a)
    simp
  _ = ‖(∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i - f.coeff i) * X ^ i).eval a‖ := by
    rw [← eval_sub]
    simp only [ha, norm_zero, add_zero]
    rw [(g - f).as_sum_range' (g.natDegree + 1)]
    · congr
      simp [← C_mul_X_pow_eq_monomial]
    · simpa [hdeg, Nat.lt_succ_iff] using g.natDegree_sub_le f
  _ ≤ ∑ i ∈ Finset.range (g.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ := by
    have := norm_sum_le (Finset.range (g.natDegree + 1))
        (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
    simpa [eval_mul, eval_finsetSum] using this
    -- The following tactic does not work here:
    -- simpa [eval_mul, eval_finsetSum] using norm_sum_le (Finset.range (g.natDegree + 1))
    --     (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
  _ < _ := by
    rw [hdeg]
    convert!
      Finset.sum_lt_sum_of_nonempty (g := fun i ↦ ε * (‖a‖ ⊔ 1) ^ ↑f.natDegree)
        (Finset.nonempty_range_add_one) ?_
    · simp [mul_assoc]
    · simp only [Finset.mem_range, norm_mul, norm_pow]
      intro i hi
      apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
      · simpa [← map_sub] using hcoeff i
      · refine (pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_
        exact pow_le_pow_right₀ (le_max_right ‖a‖ 1) (Nat.le_of_lt_succ hi)
      all_goals positivity
-- 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))
_₁ : norm (E := K) (Multiset.prod (Multiset.map (fun (x : K) ↦ a - x) g.roots)) = ‖eval a g‖
_₂ : ‖eval a g‖ ≤ ‖eval a g - eval a f‖ + ‖eval a f‖
_₃ :
  ‖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))‖
_₄ :
  ‖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‖
⊢ Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε * HPow.hPow (β := ℝ) (max ‖a‖ 1) (↑f.natDegree : ℝ)
have _₅ : ∑ 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: calc
  _ = (g.roots.map (fun x ↦ NormedField.toMulRingNorm K (a - x))).prod := rfl
  _ = ‖(g.roots.map (fun x ↦ a - x)).prod‖ := by
    rw [g.roots.prod_hom' (NormedField.toMulRingNorm K) (fun x : K ↦ a - x)]
    rfl
  _ = ‖g.eval a‖ := by
    congr
    rw [hg.eval_eq_prod_roots_of_monic hgm]
  _ ≤ ‖g.eval a - f.eval a‖ + ‖f.eval a‖ := by
    convert! norm_add_le (g.eval a - f.eval a) (f.eval a)
    simp
  _ = ‖(∑ i ∈ Finset.range (g.natDegree + 1), C (g.coeff i - f.coeff i) * X ^ i).eval a‖ := by
    rw [← eval_sub]
    simp only [ha, norm_zero, add_zero]
    rw [(g - f).as_sum_range' (g.natDegree + 1)]
    · congr
      simp [← C_mul_X_pow_eq_monomial]
    · simpa [hdeg, Nat.lt_succ_iff] using g.natDegree_sub_le f
  _ ≤ ∑ i ∈ Finset.range (g.natDegree + 1), ‖(g.coeff i - f.coeff i) * a ^ i‖ := by
    have := norm_sum_le (Finset.range (g.natDegree + 1))
        (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
    simpa [eval_mul, eval_finsetSum] using this
    -- The following tactic does not work here:
    -- simpa [eval_mul, eval_finsetSum] using norm_sum_le (Finset.range (g.natDegree + 1))
    --     (fun i ↦ (C (g.coeff i - f.coeff i) * X ^ i).eval a)
  _ < _ := by
    rw [hdeg]
    convert!
      Finset.sum_lt_sum_of_nonempty (g := fun i ↦ ε * (‖a‖ ⊔ 1) ^ ↑f.natDegree)
        (Finset.nonempty_range_add_one) ?_
    · simp [mul_assoc]
    · simp only [Finset.mem_range, norm_mul, norm_pow]
      intro i hi
      apply mul_lt_mul_of_lt_of_le_of_nonneg_of_pos
      · simpa [← map_sub] using hcoeff i
      · refine (pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_
        exact pow_le_pow_right₀ (le_max_right ‖a‖ 1) (Nat.le_of_lt_succ hi)
      all_goals positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
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 ∈ g.aroots L,
    ‖a - b‖ < HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
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
⊢ ∃ b ∈ g.aroots L,
    ‖a - b‖ < HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1
have right : ‖a - b‖ < HPow.hPow (β := ℝ) (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 * ε) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1
Tactic: use b, h1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NormedField L
inst_2 : Algebra K L
hd : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
⊢ ∃ (g : K[X]), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ < ε
have pos : ∀ (h : f.natDegree = 0),
  ∃ (g : K[X]), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ < ε
Tactic: by_cases h : f.natDegree = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NormedField L
inst_2 : Algebra K L
hd : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
pos :
  ∀ (h : f.natDegree = 0),
    ∃ (g : K[X]), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ < ε
⊢ ∃ (g : K[X]), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ < ε
have neg : ∀ (h : ¬f.natDegree = 0),
  ∃ (g : K[X]), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ < ε
Tactic: by_cases h : f.natDegree = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NormedField L
inst_2 : Algebra K L
hd : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h : f.natDegree = 0
⊢ ∃ (g : K[X]), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ < ε
have h₁ : Monic.{u_1} (R := K) 1 ∧
  f.natDegree = natDegree.{u_1} (R := K) 1 ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) 1) n - f.coeff n‖ < ε
Tactic: use 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NormedField L
inst_2 : Algebra K L
hd : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h : f.natDegree = 0
⊢ Monic.{u_1} (R := K) 1 ∧
    f.natDegree = natDegree.{u_1} (R := K) 1 ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) 1) n - f.coeff n‖ < ε
have h₁ : Monic.{u_1} (R := K) 1 ∧
  natDegree.{u_2} (R := L) 1 = natDegree.{u_1} (R := K) 1 ∧
    ∀ (n : ℕ), ‖coeff (map (algebraMap K L) 1) n - coeff 1 n‖ < ε
Tactic: rw [hf.natDegree_eq_zero.mp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NormedField L
inst_2 : Algebra K L
hd : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h : ¬f.natDegree = 0
⊢ ∃ (g : K[X]), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ < ε
have neg : ∀ (c : (i : ℕ) → K) (hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L : (a : K) → L) (c i)) < ε),
  ∃ (g : K[X]), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ < ε
Tactic: choose c hc using fun i ↦ Metric.denseRange_iff.mp hd (f.coeff i) ε hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NormedField L
inst_2 : Algebra K L
hd : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h : ¬f.natDegree = 0
c : (i : ℕ) → K
hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L : (a : K) → L) (c i)) < ε
⊢ ((C : (a : K) → K[X]) 1 * HPow.hPow (α := K[X]) X f.natDegree +
        ∑ i ∈ Finset.Iio f.natDegree,
          HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (c i) : K[X]) (HPow.hPow (α := K[X]) X i)).natDegree =
    ((C : (a : K) → K[X]) 1 * HPow.hPow (α := K[X]) X f.natDegree).natDegree
have h₁ : natDegree.{u_1} (R := K)
    (∑ i ∈ Finset.Iio f.natDegree,
      HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (c i) : K[X]) (HPow.hPow (α := K[X]) X i)) <
  ((C : (a : K) → K[X]) 1 * HPow.hPow (α := K[X]) X f.natDegree).natDegree
Tactic: apply Polynomial.natDegree_add_eq_left_of_natDegree_lt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NormedField L
inst_2 : Algebra K L
hd : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h : ¬f.natDegree = 0
c : (i : ℕ) → K
hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L : (a : K) → L) (c i)) < ε
⊢ natDegree.{u_1} (R := K)
      (∑ i ∈ Finset.Iio f.natDegree,
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (c i) : K[X]) (HPow.hPow (α := K[X]) X i)) <
    ((C : (a : K) → K[X]) 1 * HPow.hPow (α := K[X]) X f.natDegree).natDegree
have h₁ : natDegree.{u_1} (R := K)
    (∑ i ∈ Finset.Iio f.natDegree,
      HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (c i) : K[X]) (HPow.hPow (α := K[X]) X i)) <
  f.natDegree
Tactic: simp only [map_one, one_mul, natDegree_pow, natDegree_X, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NormedField L
inst_2 : Algebra K L
hd : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h : ¬f.natDegree = 0
c : (i : ℕ) → K
hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L : (a : K) → L) (c i)) < ε
⊢ natDegree.{u_1} (R := K)
      (∑ i ∈ Finset.Iio f.natDegree,
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (c i) : K[X]) (HPow.hPow (α := K[X]) X i)) <
    f.natDegree
have h₁ : natDegree.{u_1} (R := K)
    (∑ i ∈ Finset.Iio f.natDegree,
      HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (c i) : K[X]) (HPow.hPow (α := K[X]) X i)) ≤
  f.natDegree - 1
Tactic: rw [← Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)]