awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
hf : ¬f = 0
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff
have neg : eval r ((hasseDeriv f.natDegree : (a : R[X]) → R[X]) f) = f.leadingCoeff
Tactic: rw [taylor_coeff, hasseDeriv_natDegree_eq_C, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff
have neg₁ : eval r ((C : (a : R) → R[X]) f.leadingCoeff) = f.leadingCoeff
Tactic: rw [taylor_coeff, hasseDeriv_natDegree_eq_C, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff
have neg₂ : f.leadingCoeff = f.leadingCoeff
Tactic: rw [taylor_coeff, hasseDeriv_natDegree_eq_C, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
have 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
Tactic: refine map_natDegree_eq_natDegree _ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
⊢ ∀ (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
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
⊢ leadingCoeff ((taylor r : (a : R[X]) → R[X]) f) = f.leadingCoeff
have 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
Tactic: rw [leadingCoeff, leadingCoeff, natDegree_taylor, coeff_taylor_natDegree, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ leadingCoeff ((taylor r : (a : R[X]) → R[X]) f) = f.leadingCoeff
have 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
Tactic: rw [leadingCoeff, leadingCoeff, natDegree_taylor, coeff_taylor_natDegree, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ leadingCoeff ((taylor r : (a : R[X]) → R[X]) f) = f.leadingCoeff
have rw₂ : coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.coeff f.natDegree
Tactic: rw [leadingCoeff, leadingCoeff, natDegree_taylor, coeff_taylor_natDegree, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ leadingCoeff ((taylor r : (a : R[X]) → R[X]) f) = f.leadingCoeff
have rw₃ : f.leadingCoeff = f.coeff f.natDegree
Tactic: rw [leadingCoeff, leadingCoeff, natDegree_taylor, coeff_taylor_natDegree, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ leadingCoeff ((taylor r : (a : R[X]) → R[X]) f) = f.leadingCoeff
have rw₄ : f.coeff f.natDegree = f.coeff f.natDegree
Tactic: rw [leadingCoeff, leadingCoeff, natDegree_taylor, coeff_taylor_natDegree, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
⊢ Eq (α := R[X]) ((taylor r : (a : R[X]) → R[X]) f : R[X]) (0 : R[X]) ↔ f = 0
have rw : Eq.{u_1 + 1} (α := R) (leadingCoeff ((taylor r : (a : R[X]) → R[X]) f)) 0 ↔ f = 0
Tactic: rw [← leadingCoeff_eq_zero, ← leadingCoeff_eq_zero, leadingCoeff_taylor]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ Eq (α := R[X]) ((taylor r : (a : R[X]) → R[X]) f : R[X]) (0 : R[X]) ↔ f = 0
have rw₁ : Eq.{u_1 + 1} (α := R) (leadingCoeff ((taylor r : (a : R[X]) → R[X]) f)) 0 ↔ f.leadingCoeff = 0
Tactic: rw [← leadingCoeff_eq_zero, ← leadingCoeff_eq_zero, leadingCoeff_taylor]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ Eq (α := R[X]) ((taylor r : (a : R[X]) → R[X]) f : R[X]) (0 : R[X]) ↔ f = 0
have rw₂ : f.leadingCoeff = 0 ↔ f.leadingCoeff = 0
Tactic: rw [← leadingCoeff_eq_zero, ← leadingCoeff_eq_zero, leadingCoeff_taylor]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
⊢ degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree
have pos : ∀ (hp : p = 0), degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree
have neg : ∀ (hp : ¬p = 0), degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
hp : p = 0
⊢ degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree
have pos : degree (R := R) ((taylor r : (a : R[X]) → R[X]) 0) = degree.{u_1} (R := R) 0
Tactic: rw [hp, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree
have pos₁ : degree.{u_1} (R := R) 0 = degree.{u_1} (R := R) 0
Tactic: rw [hp, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
r : R
hp : ¬p = 0
⊢ degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree
have neg : degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = (↑p.natDegree : WithBot ℕ)
Tactic: rw [degree_eq_natDegree hp, degree_eq_iff_natDegree_eq ((taylor_eq_zero r p).not.2 hp),
      natDegree_taylor]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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 ℕ)
⊢ degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree
have neg₁ : natDegree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.natDegree
Tactic: rw [degree_eq_natDegree hp, degree_eq_iff_natDegree_eq ((taylor_eq_zero r p).not.2 hp),
      natDegree_taylor]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ degree.{u_1} (R := R) ((taylor r : (a : R[X]) → R[X]) p) = p.degree
have neg₂ : p.natDegree = p.natDegree
Tactic: rw [degree_eq_natDegree hp, degree_eq_iff_natDegree_eq ((taylor_eq_zero r p).not.2 hp),
      natDegree_taylor]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ f = 0
have rw : Eq (α := R[X]) ((taylor r : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
Tactic: rw [← taylor_eq_zero r]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ Eq (α := R[X]) ((taylor r : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
have a : ∀ (k : ℕ), Eq.{u_1 + 1} (α := R) (coeff ((taylor r : (a : R[X]) → R[X]) f) k) (coeff 0 k)
Tactic: ext k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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 : ℕ
⊢ Eq.{u_1 + 1} (α := R) (coeff ((taylor r : (a : R[X]) → R[X]) f) k) (coeff 0 k)
have a : eval r ((hasseDeriv k : (a : R[X]) → R[X]) f) = coeff 0 k
Tactic: rw [taylor_coeff, h, coeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (coeff ((taylor r : (a : R[X]) → R[X]) f) k) (coeff 0 k)
have a₁ : Eq.{u_1 + 1} (α := R) 0 (coeff 0 k)
Tactic: rw [taylor_coeff, h, coeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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)
⊢ Eq.{u_1 + 1} (α := R) (coeff ((taylor r : (a : R[X]) → R[X]) f) k) (coeff 0 k)
have a₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [taylor_coeff, h, coeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
x y : R
⊢ ∃ (c : R), c * HPow.hPow (β := ℕ) y 2 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p = eval (x + y) p
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ ∃ (c : R), c * HPow.hPow (β := ℕ) y 2 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p = eval (x + y) p
have 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
Tactic: rw [add_comm, ← p.taylor_eval x y, this, Finset.sum_range_succ', Finset.sum_range_succ']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ ∃ (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
have 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
Tactic: use ∑ i ∈ Finset.range p.natDegree, (taylor x p).coeff (i + 2) * y ^ i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
x y : R
hy : HPow.hPow (β := ℕ) y 2 = 0
⊢ eval (x + y) p = eval x p + eval x ((derivative : (a : R[X]) → R[X]) p) * y
have rcases : ∀ (c : R)
  (h : c * HPow.hPow (β := ℕ) y 2 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p = eval (x + y) p),
  eval (x + y) p = eval x p + eval x ((derivative : (a : R[X]) → R[X]) p) * y
Tactic: rcases exists_mul_sq_add_linear_part_eq_eval_add p x y with ⟨c, h⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
x y : R
hy : HPow.hPow (β := ℕ) y 2 = 0
c : R
h : c * HPow.hPow (β := ℕ) y 2 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p = eval (x + y) p
⊢ eval (x + y) p = eval x p + eval x ((derivative : (a : R[X]) → R[X]) p) * y
have rw : c * 0 + eval x ((derivative : (a : R[X]) → R[X]) p) * y + eval x p =
  eval x p + eval x ((derivative : (a : R[X]) → R[X]) p) * y
Tactic: rw [← h, hy]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
f : R[X]
s : R
⊢ eval (s - r) ((taylor r : (a : R[X]) → R[X]) f) = eval s f
have rw : eval (s - r + r) f = eval s f
Tactic: rw [taylor_eval, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
f : R[X]
s : R
rw : eval (s - r + r) f = eval s f
⊢ eval (s - r) ((taylor r : (a : R[X]) → R[X]) f) = eval s f
have rw₁ : eval s f = eval s f
Tactic: rw [taylor_eval, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
r : R
⊢ (sum ((taylor r : (a : R[X]) → R[X]) f) fun (i : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i)) =
    f
have rw : comp ((taylor r : (a : R[X]) → R[X]) f) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = f
Tactic: rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_cancel,
    taylor_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
r : R
rw : comp ((taylor r : (a : R[X]) → R[X]) f) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = f
⊢ (sum ((taylor r : (a : R[X]) → R[X]) f) fun (i : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i)) =
    f
have rw₁ : comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) r : R[X])) = f
Tactic: rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_cancel,
    taylor_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
r : R
rw : comp ((taylor r : (a : R[X]) → R[X]) f) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = f
rw₁ : comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) r : R[X])) = f
⊢ (sum ((taylor r : (a : R[X]) → R[X]) f) fun (i : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i)) =
    f
have rw₂ : comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-r) : R[X])) = f
Tactic: rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_cancel,
    taylor_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
r : R
rw : comp ((taylor r : (a : R[X]) → R[X]) f) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = f
rw₁ : comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) r : R[X])) = f
rw₂ :
  comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-r) : R[X])) = f
⊢ (sum ((taylor r : (a : R[X]) → R[X]) f) fun (i : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i)) =
    f
have rw₃ : (taylor (-r) : (a : R[X]) → R[X]) ((taylor r : (a : R[X]) → R[X]) f) = f
Tactic: rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_cancel,
    taylor_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
r : R
rw : comp ((taylor r : (a : R[X]) → R[X]) f) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = f
rw₁ : comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) r : R[X])) = f
rw₂ :
  comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-r) : R[X])) = f
rw₃ : (taylor (-r) : (a : R[X]) → R[X]) ((taylor r : (a : R[X]) → R[X]) f) = f
⊢ (sum ((taylor r : (a : R[X]) → R[X]) f) fun (i : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i)) =
    f
have rw₄ : (taylor (-r + r) : (a : R[X]) → R[X]) f = f
Tactic: rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_cancel,
    taylor_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
r : R
rw : comp ((taylor r : (a : R[X]) → R[X]) f) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = f
rw₁ : comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) r : R[X])) = f
rw₂ :
  comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-r) : R[X])) = f
rw₃ : (taylor (-r) : (a : R[X]) → R[X]) ((taylor r : (a : R[X]) → R[X]) f) = f
rw₄ : (taylor (-r + r) : (a : R[X]) → R[X]) f = f
⊢ (sum ((taylor r : (a : R[X]) → R[X]) f) fun (i : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i)) =
    f
have rw₅ : (taylor 0 : (a : R[X]) → R[X]) f = f
Tactic: rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_cancel,
    taylor_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
r : R
rw : comp ((taylor r : (a : R[X]) → R[X]) f) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = f
rw₁ : comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) r : R[X])) = f
rw₂ :
  comp ((taylor r : (a : R[X]) → R[X]) f) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-r) : R[X])) = f
rw₃ : (taylor (-r) : (a : R[X]) → R[X]) ((taylor r : (a : R[X]) → R[X]) f) = f
rw₄ : (taylor (-r + r) : (a : R[X]) → R[X]) f = f
rw₅ : (taylor 0 : (a : R[X]) → R[X]) f = f
⊢ (sum ((taylor r : (a : R[X]) → R[X]) f) fun (i : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i)) =
    f
have rw₆ : f = f
Tactic: rw [← comp_eq_sum_left, sub_eq_add_neg, ← C_neg, ← taylor_apply, taylor_taylor, neg_add_cancel,
    taylor_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ coeff (trinomial k m n u v w) n = w
have rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
    n =
  w
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.UnitTrinomial (goal)
Goal:
R : Type u_1
inst : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
      n =
    w
⊢ coeff (trinomial k m n u v w) n = w
have rw₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
      n +
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) w : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n =
  w
Tactic: rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]