awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
this_1 : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
x : ℕ
hx : (0 ≤ x ∧ x < q) ∧ q ≤ x ∧ x < p.natDegree + 1
⊢ False

Tactic:
hx.1.2.not_ge hx.2.1

Premises used: And.right, And.left, LT.lt.not_ge
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial A
inst_4 : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p0 : p ≠ 0
c : (k : ℕ) → R[X] :=
  fun (k : ℕ) ↦
    if hk : q ≤ k then
      Exists.choose (p := fun (gp : R[X]) ↦
        gp.natDegree ≤ p.natDegree - k ∧
          ∀ (r : A),
            (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
              HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) gp : A))
        ⋯
    else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc :
  ∀ (k : ℕ) (hk : q ≤ k) (r : A),
    (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[k] p) =
      HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c k) : A)
r : A
p' : A[X]
hp : map (algebraMap R A) p = HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) r : A[X]) ^ (q - 1) * p'
this_1 : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
x : ℕ
hx : (0 ≤ x ∧ x < q) ∧ q ≤ x ∧ x < p.natDegree + 1
⊢ False

Tactic:
exact hx.1.2.not_ge hx.2.1

Premises used: And.right, And.left, LT.lt.not_ge
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
p : R[X]
q : ℕ
hq : 0 < q
⊢ ∃ (gp : R[X]),
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : R) {p' : R[X]},
        p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ (q - 1) * p' →
          eval r ((sumIDeriv : (a : R[X]) → R[X]) p) = (q - 1)! • eval r p' + q ! • eval r gp

Tactic:
simpa using aeval_sumIDeriv_of_pos R p hq Function.injective_id

Premises used: Function.injective_id, Polynomial.aeval_sumIDeriv_of_pos
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r_1 : R
f_1 : R[X]
r c : R
f : R[X]
⊢ (c • f).comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R)
      (f.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])))

Tactic:
simp only [smul_eq_C_mul, C_mul_comp, RingHom.id_apply]

Premises used: RingHom.id_apply, Polynomial.smul_eq_C_mul, Polynomial.C_mul_comp
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
⊢ (taylor r : (a : R[X]) → R[X]) f = f.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))

Tactic:
rfl

Premises used: Polynomial.comp, rfl
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ (taylor r : (a : R[X]) → R[X]) X = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])

Tactic:
X_comp

Premises used: Polynomial.X_comp, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
⊢ (taylor r : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X n) =
    HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ n

Tactic:
X_pow_comp

Premises used: Polynomial.X_pow_comp, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r x : R
⊢ Eq (α := R[X]) ((taylor r : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) x) : R[X]) ((C : (a : R) → R[X]) x : R[X])

Tactic:
C_comp

Premises used: Polynomial.C_comp, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : f.comp (HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 0)) = f
rw₁ : f.comp (HAdd.hAdd (α := R[X]) X 0) = f
rw₂ : f.comp X = f
rw₃ rw₄ : f = f
⊢ (taylor 0 : (a : R[X]) → R[X]) f = f

Tactic:
rw [taylor_apply, C_0, add_zero, comp_X]

Premises used: Polynomial.C_0, Polynomial.taylor_apply, Polynomial.comp_X, add_zero
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X] →ₗ[R] R[X]) (taylor 0) LinearMap.id

Tactic:
LinearMap.ext taylor_zero

Premises used: LinearMap.ext, Polynomial.taylor_zero
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ Eq (α := R[X]) ((taylor r : (a : R[X]) → R[X]) 1) ((C : (a : R) → R[X]) 1)

Tactic:
taylor_C r 1

Premises used: OfNat.ofNat, Polynomial.taylor_C
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
i : ℕ
k : R
⊢ (taylor r : (a : R[X]) → R[X]) ((monomial i : (a : R) → R[X]) k) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i)

Tactic:
simp [taylor_apply]

Premises used: Polynomial.taylor_apply
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
n : ℕ
e_a : lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n
⊢ Eq (α := R) ((lcoeff R n ∘ₗ taylor r : (a : R[X]) → R) f : R) ((leval r ∘ₗ hasseDeriv n : (a : R[X]) → R) f : R)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
e_a :
  ∀ (i : ℕ),
    Eq (α := R) (((lcoeff R n ∘ₗ taylor r) ∘ₗ monomial i : (a : R) → R) 1 : R)
      (((leval r ∘ₗ hasseDeriv n) ∘ₗ monomial i : (a : R) → R) 1 : R)
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
n i : ℕ
e_a :
  ∑ x ∈ Finset.range (i + 1),
      (lcoeff R n : (a : R[X]) → R)
        (HPow.hPow (α := R[X]) X x * HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (i - x) *
          (↑(i.choose x) : R[X])) =
    (↑(i.choose n) : R) * r ^ (i - n)
⊢ Eq (α := R) (((lcoeff R n ∘ₗ taylor r) ∘ₗ monomial i : (a : R) → R) 1 : R)
    (((leval r ∘ₗ hasseDeriv n) ∘ₗ monomial i : (a : R) → R) 1 : R)

Tactic:
simp only [leval_apply, mul_one, one_mul, eval_monomial, LinearMap.comp_apply, map_sum,
      hasseDeriv_monomial, taylor_apply, monomial_comp, C_1, (commute_X (C r)).add_pow i]

Premises used: Polynomial.C, Polynomial.C_1, LinearMap.comp_apply, Commute.add_pow, Polynomial.taylor_apply, map_sum, Polynomial.hasseDeriv_monomial, Polynomial.commute_X, Polynomial.leval_apply, mul_one, DFunLike.coe, one_mul, Polynomial.monomial_comp, Polynomial.eval_monomial
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
n i : ℕ
e_a : (if n < i + 1 then r ^ (i - n) * (↑(i.choose n) : R) else 0) = r ^ (i - n) * (↑(i.choose n) : R)
⊢ ∑ x ∈ Finset.range (i + 1),
      (lcoeff R n : (a : R[X]) → R)
        (HPow.hPow (α := R[X]) X x * HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (i - x) *
          (↑(i.choose x) : R[X])) =
    (↑(i.choose n) : R) * r ^ (i - n)

Tactic:
simp only [lcoeff_apply, ← C_eq_natCast, mul_assoc, ← C_pow, ← C_mul, coeff_mul_C,
      (Nat.cast_commute _ _).eq, coeff_X_pow, boole_mul, Finset.sum_ite_eq, Finset.mem_range]

Premises used: Polynomial.C_eq_natCast, Polynomial.coeff_X_pow, mul_assoc, Finset.mem_range, Polynomial.lcoeff_apply, Polynomial.coeff_mul_C, Polynomial.C_mul, boole_mul, Commute.eq, Polynomial.C_pow, Finset.sum_ite_eq, Nat.cast_commute
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
n i : ℕ
pos : ∀ (h : n < i + 1), r ^ (i - n) * (↑(i.choose n) : R) = r ^ (i - n) * (↑(i.choose n) : R)
neg : ∀ (h : ¬n < i + 1), 0 = r ^ (i - n) * (↑(i.choose n) : R)
⊢ (if n < i + 1 then r ^ (i - n) * (↑(i.choose n) : R) else 0) = r ^ (i - n) * (↑(i.choose n) : R)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
n i : ℕ
h : n < i + 1
⊢ r ^ (i - n) * (↑(i.choose n) : R) = r ^ (i - n) * (↑(i.choose n) : R)

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ i + 1 ≤ n

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
neg : 0 = r ^ (i - n) * (↑0 : R)
neg₁ : 0 = r ^ (i - n) * 0
neg₂ neg₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 0 = r ^ (i - n) * (↑(i.choose n) : R)

Tactic:
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Nat.choose_eq_zero_of_lt, Nat.cast_zero
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
rw : eval r ((hasseDeriv 0 : (a : R[X]) → R[X]) f) = eval r f
rw₁ : eval r ((LinearMap.id : (a : R[X]) → R[X]) f) = eval r f
rw₂ rw₃ : eval r f = eval r f
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) 0 = eval r f

Tactic:
rw [taylor_coeff, hasseDeriv_zero, LinearMap.id_apply]

Premises used: LinearMap.id_apply, Polynomial.hasseDeriv_zero, Polynomial.taylor_coeff
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
rw : eval r ((hasseDeriv 1 : (a : R[X]) → R[X]) f) = eval r ((derivative : (a : R[X]) → R[X]) f)
rw₁ rw₂ : eval r ((derivative : (a : R[X]) → R[X]) f) = eval r ((derivative : (a : R[X]) → R[X]) f)
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) 1 = eval r ((derivative : (a : R[X]) → R[X]) f)

Tactic:
rw [taylor_coeff, hasseDeriv_one]

Premises used: Polynomial.taylor_coeff, Polynomial.hasseDeriv_one
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
pos : ∀ (hf : f = 0), coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff
neg : ∀ (hf : ¬f = 0), coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff

Tactic:
by_cases hf : f = 0
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
hf : f = 0
pos : Eq (α := R) (coeff ((taylor r : (a : R[X]) → R[X]) 0) (natDegree.{u_1} (R := R) 0)) (leadingCoeff 0)
pos₁ : Eq.{u_1 + 1} (α := R) (coeff 0 (natDegree.{u_1} (R := R) 0)) (leadingCoeff 0)
pos₂ pos₃ : Eq.{u_1 + 1} (α := R) (leadingCoeff 0) (leadingCoeff 0)
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff

Tactic:
rw [hf, map_zero, coeff_natDegree]

Premises used: Polynomial.coeff_natDegree, map_zero
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
hf : ¬f = 0
neg : eval r ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f) = f.leadingCoeff
neg₁ : eval r ((C : (a : R) → R[X]) f.leadingCoeff) = f.leadingCoeff
neg₂ neg₃ : f.leadingCoeff = f.leadingCoeff
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff

Tactic:
rw [taylor_coeff, hasseDeriv_natDegree_eq_C, eval_C]

Premises used: Polynomial.eval_C, Polynomial.hasseDeriv_natDegree_eq_C, Polynomial.taylor_coeff
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
⊢ natDegree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.natDegree

Tactic:
map_natDegree_eq_natDegree _ ?_

Premises used: Polynomial.map_natDegree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
refine :
  ∀ (n : ℕ) (c : R),
    c ≠ 0 → natDegree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) c)) = n
⊢ natDegree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.natDegree

Tactic:
refine map_natDegree_eq_natDegree _ ?_

Premises used: Polynomial.map_natDegree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
h : Nontrivial R
n : ℕ
c : R
c0 : c ≠ 0
⊢ natDegree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) c)) = n

Tactic:
simp [taylor_monomial, natDegree_C_mul_of_mul_ne_zero, natDegree_pow_X_add_C, c0]

Premises used: Polynomial.natDegree_C_mul_of_mul_ne_zero, Polynomial.taylor_monomial, Polynomial.natDegree_pow_X_add_C
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
rw :
  coeff ((taylor r : (a : R[X]) → R[X]) f) (natDegree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) f)) =
    f.leadingCoeff
rw₁ :
  coeff ((taylor r : (a : R[X]) → R[X]) f) (natDegree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) f)) =
    f.coeff f.natDegree
rw₂ : coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.coeff f.natDegree
rw₃ : f.leadingCoeff = f.coeff f.natDegree
rw₄ rw₅ : f.coeff f.natDegree = f.coeff f.natDegree
⊢ leadingCoeff ((taylor r : (a : R[X]) → R[X]) f) = f.leadingCoeff

Tactic:
rw [leadingCoeff, leadingCoeff, natDegree_taylor, coeff_taylor_natDegree, leadingCoeff]

Premises used: Polynomial.coeff_taylor_natDegree, Polynomial.leadingCoeff, Polynomial.natDegree_taylor
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
rw : Eq.{u_1 + 1} (α := R) (leadingCoeff ((taylor r : (a : R[X]) → R[X]) f)) 0 ↔ f = 0
rw₁ : Eq.{u_1 + 1} (α := R) (leadingCoeff ((taylor r : (a : R[X]) → R[X]) f)) 0 ↔ f.leadingCoeff = 0
rw₂ rw₃ : f.leadingCoeff = 0 ↔ f.leadingCoeff = 0
⊢ Eq (α := R[X]) ((taylor r : (a : R[X]) → R[X]) f : R[X]) (0 : R[X]) ↔ f = 0

Tactic:
rw [← leadingCoeff_eq_zero, ← leadingCoeff_eq_zero, leadingCoeff_taylor]

Premises used: Polynomial.leadingCoeff_eq_zero, Polynomial.leadingCoeff_taylor
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
pos : ∀ (hp : p = 0), degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree
neg : ∀ (hp : ¬p = 0), degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree
⊢ degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
hp : p = 0
pos : degree (R := R) ((taylor r : (a : R[X]) → R[X]) 0) = degree.{u_1} (R := R) 0
pos₁ pos₂ : degree.{u_1} (R := R) 0 = degree.{u_1} (R := R) 0
⊢ degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree

Tactic:
rw [hp, map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
hp : ¬p = 0
neg : degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = (↑p.natDegree : WithBot ℕ)
neg₁ : natDegree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.natDegree
neg₂ neg₃ : p.natDegree = p.natDegree
⊢ degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree

Tactic:
rw [degree_eq_natDegree hp, degree_eq_iff_natDegree_eq ((taylor_eq_zero r p).not.2 hp),
      natDegree_taylor]

Premises used: Iff.mpr, Polynomial.degree_eq_natDegree, Polynomial.taylor_eq_zero, Iff.not, Polynomial.natDegree_taylor, Polynomial.degree_eq_iff_natDegree_eq
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k : (a : R[X]) → R[X]) f) = 0
rw : Eq (α := R[X]) ((taylor r : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ f = 0

Tactic:
rw [← taylor_eq_zero r]

Premises used: Polynomial.taylor_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k : (a : R[X]) → R[X]) f) = 0
a : ∀ (k : ℕ), Eq.{u_1 + 1} (α := R) (coeff ((taylor r : (a : R[X]) → R[X]) f) k) (coeff 0 k)
⊢ Eq (α := R[X]) ((taylor r : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])

Tactic:
ext k
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k : (a : R[X]) → R[X]) f) = 0
k : ℕ
a : eval r ((hasseDeriv k : (a : R[X]) → R[X]) f) = coeff 0 k
a₁ : Eq.{u_1 + 1} (α := R) 0 (coeff 0 k)
a₂ a₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) (coeff ((taylor r : (a : R[X]) → R[X]) f) k) (coeff 0 k)

Tactic:
rw [taylor_coeff, h, coeff_zero]

Premises used: Polynomial.coeff_zero, Polynomial.taylor_coeff
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
p : R[X]
r : R
f : R →+* S
⊢ map f ((taylor r : (a : R[X]) → R[X]) p) =
    ((taylor ((f : (a : R) → S) r) : S[X] →ₗ[S] S[X]) : (a : S[X]) → S[X]) (map f p)

Tactic:
simp [taylor_apply, Polynomial.map_comp]

Premises used: Polynomial.taylor_apply, Polynomial.map_comp
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Ring R
r : R
⊢ Function.Injective (α := R[X]) (β := R[X]) (⇑(taylor r) : (a : R[X]) → R[X])

Tactic:
(injective_iff_map_eq_zero' _).2 (taylor_eq_zero r)

Premises used: Iff.mpr, Polynomial.taylor_eq_zero, injective_iff_map_eq_zero'
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : Ring R
r : R
p q : R[X]
⊢ Eq (α := R[X]) ((taylor r : (a : R[X]) → R[X]) p : R[X]) ((taylor r : (a : R[X]) → R[X]) q : R[X]) ↔ p = q

Tactic:
(taylor_injective r).eq_iff

Premises used: Polynomial.taylor_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
r : R
p q : R[X]
⊢ (taylor r : (a : R[X]) → R[X]) (p * q) =
    HMul.hMul (α := R[X]) (β := R[X]) ((taylor r : (a : R[X]) → R[X]) p : R[X])
      ((taylor r : (a : R[X]) → R[X]) q : R[X])

Tactic:
mul_comp ..

Premises used: Polynomial.mul_comp, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
r : R
f : R[X]
n : ℕ
⊢ (taylor r : (a : R[X]) → R[X]) (f ^ n) = HPow.hPow (α := R[X]) ((taylor r : (a : R[X]) → R[X]) f : R[X]) n

Tactic:
(taylorAlgHom r).map_pow ..

Premises used: Polynomial.taylorAlgHom, AlgHom.toRingHom, Polynomial.comp, RingHom.map_pow
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
r : R
⊢ Eq (α := R[X] →ₗ[R] R[X])
    (↑(taylorAlgHom r) :
      [inst_1 : FunLike (R[X] →ₐ[R] R[X]) R[X] R[X]] →
        [SemilinearMapClass (R[X] →ₐ[R] R[X]) (RingHom.id R) R[X] R[X]] → R[X] →ₗ[R] R[X])
    (taylor r)

Tactic:
rfl

Premises used: Polynomial.taylor, SemilinearMapClass.semilinearMap, Polynomial.comp, rfl
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
r s : R
⊢ Eq (α := R[X]) ((taylor r : (a : R[X]) → R[X]) ((taylor s : (a : R[X]) → R[X]) f) : R[X])
    ((taylor (r + s) : (a : R[X]) → R[X]) f : R[X])

Tactic:
simp only [taylor_apply, comp_assoc, map_add, add_comp, X_comp, C_comp, add_assoc]

Premises used: Polynomial.comp_assoc, Polynomial.X_comp, add_assoc, Polynomial.taylor_apply, map_add, Polynomial.add_comp, Polynomial.C_comp
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
r : R
f : R[X]
s : R
⊢ eval s ((taylor r : (a : R[X]) → R[X]) f) = eval (s + r) f

Tactic:
simp only [taylor_apply, eval_comp, eval_C, eval_X, eval_add]

Premises used: Polynomial.eval_C, Polynomial.eval_X, Polynomial.taylor_apply, Polynomial.eval_comp, Polynomial.eval_add
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
x y t : R
⊢ natDegree.{u_1} (R := R) ((taylor x : (a : R[X]) → R[X]) p) <
    natDegree.{u_1} (R := R) ((taylor x : (a : R[X]) → R[X]) p) + 2

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
x y : R
⊢ ∀ (t : R),
    eval t ((taylor x : (a : R[X]) → R[X]) p) =
      ∑ i ∈ Finset.range (natDegree.{u_1} (R := R) ((taylor x : (a : R[X]) → R[X]) p) + 2),
        coeff ((taylor x : (a : R[X]) → R[X]) p) i * t ^ i

Tactic:
have this t :
      (taylor x p).eval t =
      ∑ i ∈ Finset.range ((taylor x p).natDegree + 2), (taylor x p).coeff i * t ^ i :=
    (taylor x p).eval_eq_sum_range' (n := (taylor x p).natDegree + 2) (by lia) t
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
x y : R
this :
  ∀ (t : R),
    eval t ((taylor x : (a : R[X]) → R[X]) p) =
      ∑ i ∈ Finset.range (natDegree.{u_1} (R := R) ((taylor x : (a : R[X]) → R[X]) p) + 2),
        coeff ((taylor x : (a : R[X]) → R[X]) p) i * t ^ i
rw :
  ∃ (c : R),
    c * HPow.hPow (β := ℕ) y 2 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p =
      ∑ k ∈ Finset.range (natDegree.{u_1} (R := R) ((taylor x : (a : R[X]) → R[X]) p)),
            coeff ((taylor x : (a : R[X]) → R[X]) p) (k + 1 + 1) * y ^ (k + 1 + 1) +
          coeff ((taylor x : (a : R[X]) → R[X]) p) (HAdd.hAdd (α := ℕ) 0 1) * y ^ HAdd.hAdd (α := ℕ) 0 1 +
        coeff ((taylor x : (a : R[X]) → R[X]) p) 0 * HPow.hPow (β := ℕ) y 0
⊢ ∃ (c : R), c * HPow.hPow (β := ℕ) y 2 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p = eval (x + y) p

Tactic:
rw [add_comm, ← p.taylor_eval x y, this, Finset.sum_range_succ', Finset.sum_range_succ']

Premises used: Polynomial.taylor_eval, add_comm, Finset.sum_range_succ'
-- Module: Mathlib.Algebra.Polynomial.Taylor
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
x y : R
this :
  ∀ (t : R),
    eval t ((taylor x : (a : R[X]) → R[X]) p) =
      ∑ i ∈ Finset.range (natDegree.{u_1} (R := R) ((taylor x : (a : R[X]) → R[X]) p) + 2),
        coeff ((taylor x : (a : R[X]) → R[X]) p) i * t ^ i
h :
  (∑ i ∈ Finset.range p.natDegree, coeff ((taylor x : (a : R[X]) → R[X]) p) (i + 2) * y ^ i) * HPow.hPow (β := ℕ) y 2 +
        eval x ((derivative : (a : R[X]) → R[X]) p) * y +
      eval x p =
    ∑ k ∈ Finset.range (natDegree.{u_1} (R := R) ((taylor x : (a : R[X]) → R[X]) p)),
          coeff ((taylor x : (a : R[X]) → R[X]) p) (k + 1 + 1) * y ^ (k + 1 + 1) +
        coeff ((taylor x : (a : R[X]) → R[X]) p) (HAdd.hAdd (α := ℕ) 0 1) * y ^ HAdd.hAdd (α := ℕ) 0 1 +
      coeff ((taylor x : (a : R[X]) → R[X]) p) 0 * HPow.hPow (β := ℕ) y 0
⊢ ∃ (c : R),
    c * HPow.hPow (β := ℕ) y 2 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p =
      ∑ k ∈ Finset.range (natDegree.{u_1} (R := R) ((taylor x : (a : R[X]) → R[X]) p)),
            coeff ((taylor x : (a : R[X]) → R[X]) p) (k + 1 + 1) * y ^ (k + 1 + 1) +
          coeff ((taylor x : (a : R[X]) → R[X]) p) (HAdd.hAdd (α := ℕ) 0 1) * y ^ HAdd.hAdd (α := ℕ) 0 1 +
        coeff ((taylor x : (a : R[X]) → R[X]) p) 0 * HPow.hPow (β := ℕ) y 0

Tactic:
use ∑ i ∈ Finset.range p.natDegree, (taylor x p).coeff (i + 2) * y ^ i

Premises used: Finset.range, Polynomial.natDegree