awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 - 1
have h₁ : ∀ 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 ≤ f.natDegree - 1
Tactic: apply Polynomial.natDegree_sum_le_of_forall_le
-- 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)) < ε
⊢ ∀ 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 ≤ f.natDegree - 1
have h₁ : ∀ (i : ℕ) (hi : i ∈ Finset.Iio f.natDegree), i ≤ f.natDegree - 1
Tactic: refine fun i hi ↦ (Polynomial.natDegree_C_mul_X_pow_le _ _).trans ?_
-- 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 =
    f.natDegree
have _ : ((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
Tactic: calc
      _ = (C (1 : K) * X ^ f.natDegree).natDegree := by
        apply Polynomial.natDegree_add_eq_left_of_natDegree_lt
        simp only [map_one, one_mul, natDegree_pow, natDegree_X, mul_one]
        rw [← Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)]
        apply Polynomial.natDegree_sum_le_of_forall_le
        refine fun i hi ↦ (Polynomial.natDegree_C_mul_X_pow_le _ _).trans ?_
        simpa [Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)] using hi
      _ = f.natDegree := by
        simp
-- 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
⊢ ((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 =
    f.natDegree
have _₁ : ((C : (a : K) → K[X]) 1 * HPow.hPow (α := K[X]) X f.natDegree).natDegree = f.natDegree
Tactic: calc
      _ = (C (1 : K) * X ^ f.natDegree).natDegree := by
        apply Polynomial.natDegree_add_eq_left_of_natDegree_lt
        simp only [map_one, one_mul, natDegree_pow, natDegree_X, mul_one]
        rw [← Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)]
        apply Polynomial.natDegree_sum_le_of_forall_le
        refine fun i hi ↦ (Polynomial.natDegree_C_mul_X_pow_le _ _).trans ?_
        simpa [Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)] using hi
      _ = f.natDegree := by
        simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Approximation (hypothesis)
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)) < ε
⊢ ∃ (g : K[X]), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ < ε
have hdeg : ((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 =
  f.natDegree
Tactic: have hdeg : (C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i).natDegree
      = f.natDegree := by
    calc
      _ = (C (1 : K) * X ^ f.natDegree).natDegree := by
        apply Polynomial.natDegree_add_eq_left_of_natDegree_lt
        simp only [map_one, one_mul, natDegree_pow, natDegree_X, mul_one]
        rw [← Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)]
        apply Polynomial.natDegree_sum_le_of_forall_le
        refine fun i hi ↦ (Polynomial.natDegree_C_mul_X_pow_le _ _).trans ?_
        simpa [Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)] using hi
      _ = f.natDegree := by
        simp
-- 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)) < ε
hdeg :
  ((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 =
    f.natDegree
⊢ ∃ (g : K[X]), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ < ε
have h₁ : ((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)).Monic ∧
  f.natDegree =
      ((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 ∧
    ∀ (n : ℕ),
      ‖coeff
              (map (algebraMap K L)
                ((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)))
              n -
            f.coeff n‖ <
        ε
Tactic: use C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i
-- 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)) < ε
hdeg :
  ((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 =
    f.natDegree
⊢ ((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)).Monic ∧
    f.natDegree =
        ((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 ∧
      ∀ (n : ℕ),
        ‖coeff
                (map (algebraMap K L)
                  ((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)))
                n -
              f.coeff n‖ <
          ε
have h₁ : ((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)).Monic
Tactic: refine ⟨?_, hdeg.symm, fun n ↦ ?_⟩
-- 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)) < ε
hdeg :
  ((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 =
    f.natDegree
h₁ :
  ((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)).Monic
⊢ ((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)).Monic ∧
    f.natDegree =
        ((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 ∧
      ∀ (n : ℕ),
        ‖coeff
                (map (algebraMap K L)
                  ((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)))
                n -
              f.coeff n‖ <
          ε
have h₂ : ∀ (n : ℕ),
  ‖coeff
          (map (algebraMap K L)
            ((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)))
          n -
        f.coeff n‖ <
    ε
Tactic: refine ⟨?_, hdeg.symm, fun n ↦ ?_⟩
-- 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)) < ε
hdeg :
  ((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 =
    f.natDegree
⊢ ((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)).Monic
have h₁ : ((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)).coeff
    f.natDegree =
  1
Tactic: rw [Monic, leadingCoeff, hdeg]
-- 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)) < ε
hdeg :
  ((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 =
    f.natDegree
n : ℕ
⊢ ‖coeff
          (map (algebraMap K L)
            ((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)))
          n -
        f.coeff n‖ <
    ε
have h₁ : ∀ (h : n < f.natDegree),
  ‖coeff
          (map (algebraMap K L)
            ((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)))
          n -
        f.coeff n‖ <
    ε
Tactic: rcases lt_trichotomy n f.natDegree with h | h | 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)) < ε
hdeg :
  ((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 =
    f.natDegree
n : ℕ
h₁ :
  ∀ (h : n < f.natDegree),
    ‖coeff
            (map (algebraMap K L)
              ((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)))
            n -
          f.coeff n‖ <
      ε
⊢ ‖coeff
          (map (algebraMap K L)
            ((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)))
          n -
        f.coeff n‖ <
    ε
have h₂ : ∀ (h : n = f.natDegree),
  ‖coeff
          (map (algebraMap K L)
            ((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)))
          n -
        f.coeff n‖ <
    ε
Tactic: rcases lt_trichotomy n f.natDegree with h | h | 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)) < ε
hdeg :
  ((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 =
    f.natDegree
n : ℕ
h₁ :
  ∀ (h : n < f.natDegree),
    ‖coeff
            (map (algebraMap K L)
              ((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)))
            n -
          f.coeff n‖ <
      ε
h₂ :
  ∀ (h : n = f.natDegree),
    ‖coeff
            (map (algebraMap K L)
              ((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)))
            n -
          f.coeff n‖ <
      ε
⊢ ‖coeff
          (map (algebraMap K L)
            ((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)))
          n -
        f.coeff n‖ <
    ε
have h₃ : ∀ (h : f.natDegree < n),
  ‖coeff
          (map (algebraMap K L)
            ((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)))
          n -
        f.coeff n‖ <
    ε
Tactic: rcases lt_trichotomy n f.natDegree with h | h | h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : NormedDivisionRing α
a b : α
⊢ norm.{u_2} (E := α) 1 * norm.{u_2} (E := α) 1 = norm.{u_2} (E := α) 1 * 1
have rw : ‖HMul.hMul (α := α) 1 1‖ = norm.{u_2} (E := α) 1 * 1
Tactic: rw [← norm_mul, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : NormedDivisionRing α
a b : α
rw : ‖HMul.hMul (α := α) 1 1‖ = norm.{u_2} (E := α) 1 * 1
⊢ norm.{u_2} (E := α) 1 * norm.{u_2} (E := α) 1 = norm.{u_2} (E := α) 1 * 1
have rw₁ : norm.{u_2} (E := α) 1 = norm.{u_2} (E := α) 1 * 1
Tactic: rw [← norm_mul, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : NormedDivisionRing α
a b : α
rw : ‖HMul.hMul (α := α) 1 1‖ = norm.{u_2} (E := α) 1 * 1
rw₁ : norm.{u_2} (E := α) 1 = norm.{u_2} (E := α) 1 * 1
⊢ norm.{u_2} (E := α) 1 * norm.{u_2} (E := α) 1 = norm.{u_2} (E := α) 1 * 1
have rw₂ : norm.{u_2} (E := α) 1 = norm.{u_2} (E := α) 1
Tactic: rw [← norm_mul, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
have rw : ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
Tactic: rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
rw : ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
have rw₁ : ‖z⁻¹ * (w - z) * w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
Tactic: rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
rw : ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₁ : ‖z⁻¹ * (w - z) * w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
have rw₂ : ‖z⁻¹ * (w - z)‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
Tactic: rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
rw : ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₁ : ‖z⁻¹ * (w - z) * w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₂ : ‖z⁻¹ * (w - z)‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
have rw₃ : ‖z⁻¹‖ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
Tactic: rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
rw : ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₁ : ‖z⁻¹ * (w - z) * w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₂ : ‖z⁻¹ * (w - z)‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₃ : ‖z⁻¹‖ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
have rw₄ : ‖z‖⁻¹ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
Tactic: rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
rw : ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₁ : ‖z⁻¹ * (w - z) * w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₂ : ‖z⁻¹ * (w - z)‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₃ : ‖z⁻¹‖ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₄ : ‖z‖⁻¹ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
have rw₅ : ‖z‖⁻¹ * ‖w - z‖ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
Tactic: rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
rw : ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₁ : ‖z⁻¹ * (w - z) * w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₂ : ‖z⁻¹ * (w - z)‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₃ : ‖z⁻¹‖ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₄ : ‖z‖⁻¹ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₅ : ‖z‖⁻¹ * ‖w - z‖ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
have rw₆ : ‖w - z‖ * ‖z‖⁻¹ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
Tactic: rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
rw : ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₁ : ‖z⁻¹ * (w - z) * w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₂ : ‖z⁻¹ * (w - z)‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₃ : ‖z⁻¹‖ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₄ : ‖z‖⁻¹ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₅ : ‖z‖⁻¹ * ‖w - z‖ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
rw₆ : ‖w - z‖ * ‖z‖⁻¹ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
have rw₇ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = dist z w / (‖z‖ * ‖w‖)
Tactic: rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Basic (goal)
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
rw : ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₁ : ‖z⁻¹ * (w - z) * w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₂ : ‖z⁻¹ * (w - z)‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₃ : ‖z⁻¹‖ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₄ : ‖z‖⁻¹ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₅ : ‖z‖⁻¹ * ‖w - z‖ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
rw₆ : ‖w - z‖ * ‖z‖⁻¹ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
rw₇ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = dist z w / (‖z‖ * ‖w‖)
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
have rw₈ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ / (‖z‖ * ‖w‖)
Tactic: rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]