-- 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
_ :
  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‖
_₅ :
  ∑ 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 : ℝ)
⊢ Multiset.prod (Multiset.map (fun (x : K) ↦ ‖a - x‖) g.roots) <
    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

Premises used: Polynomial.eval, Polynomial.roots, Multiset.map, Multiset.prod, HSub.hSub, NormedField.toMulRingNorm, Finset.range, HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat, DFunLike.coe, rfl