awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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‖ < ε
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‖ < ε
⊢ ∃ (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

Premises used: Polynomial.natDegree
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
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‖ < ε
⊢ ∃ (g : K[X]), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ < ε

Tactic:
use 1
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
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‖ < ε
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‖ < ε

Tactic:
rw [hf.natDegree_eq_zero.mp]

Premises used: Polynomial.Monic.natDegree_eq_zero, Iff.mp
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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 ∧
    natDegree.{u_2} (R := L) 1 = natDegree.{u_1} (R := K) 1 ∧
      ∀ (n : ℕ), ‖coeff (map (algebraMap K L) 1) n - coeff 1 n‖ < ε

Tactic:
simp only [monic_one, natDegree_one, Polynomial.map_one, sub_self, norm_zero, hε,
      implies_true, and_self]

Premises used: Polynomial.map_one, sub_self, and_self, norm_zero, Polynomial.natDegree_one, implies_true, Polynomial.monic_one
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
⊢ f.natDegree = 0

Tactic:
h
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
⊢ f.natDegree = 0

Tactic:
exact h
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
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‖ < ε
⊢ ∃ (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ε

Premises used: Polynomial.coeff, Iff.mp, Metric.denseRange_iff
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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)) < ε
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
⊢ ((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:
apply Polynomial.natDegree_add_eq_left_of_natDegree_lt

Premises used: Polynomial.natDegree_add_eq_left_of_natDegree_lt
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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)) < ε
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
⊢ 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:
simp only [map_one, one_mul, natDegree_pow, natDegree_X, mul_one]

Premises used: Polynomial.natDegree_X, Polynomial.natDegree_pow, map_one, mul_one, one_mul
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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)) < ε
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
⊢ 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:
rw [← Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)]

Premises used: Nat.le_sub_one_iff_lt, Nat.pos_of_ne_zero
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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)) < ε
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
⊢ 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:
apply Polynomial.natDegree_sum_le_of_forall_le

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

Tactic:
fun i hi ↦ (Polynomial.natDegree_C_mul_X_pow_le _ _).trans ?_

Premises used: LE.le.trans, Polynomial.natDegree_C_mul_X_pow_le
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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)) < ε
h₁ : ∀ (i : ℕ) (hi : i ∈ Finset.Iio f.natDegree), i ≤ f.natDegree - 1
⊢ ∀ 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:
refine fun i hi ↦ (Polynomial.natDegree_C_mul_X_pow_le _ _).trans ?_

Premises used: LE.le.trans, Polynomial.natDegree_C_mul_X_pow_le
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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 : ℕ
hi : i ∈ Finset.Iio f.natDegree
⊢ i ≤ f.natDegree - 1

Tactic:
simpa [Nat.le_sub_one_iff_lt (Nat.pos_of_ne_zero h)] using hi

Premises used: Nat.le_sub_one_iff_lt, Nat.pos_of_ne_zero
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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).natDegree = f.natDegree

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

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

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
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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 ∧
    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‖ <
          ε
⊢ ∃ (g : K[X]), g.Monic ∧ f.natDegree = g.natDegree ∧ ∀ (n : ℕ), ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ < ε

Tactic:
use C 1 * X ^ f.natDegree + ∑ i < f.natDegree, C (c i) * X ^ i

Premises used: Polynomial.C, Polynomial.natDegree, OfNat.ofNat, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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‖ <
          ε

Tactic:
⟨?_, hdeg.symm, fun n ↦ ?_⟩

Premises used: And.intro, Eq.symm
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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
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‖ <
      ε
⊢ ((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:
refine ⟨?_, hdeg.symm, fun n ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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)).coeff
      f.natDegree =
    1
⊢ ((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:
rw [Monic, leadingCoeff, hdeg]

Premises used: Polynomial.leadingCoeff, Polynomial.Monic
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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)).coeff
      f.natDegree =
    1

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

Premises used: Polynomial.natDegree, lt_trichotomy
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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_1 : ¬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 : 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:
simpa [h, ne_of_lt h, ← dist_eq_norm_sub'] using hc n

Premises used: dist_eq_norm_sub', ne_of_lt
-- Module: Mathlib.Analysis.Normed.Field.Approximation
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_1 : ¬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 : 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:
simp [h, hf, hε]