awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
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)
inr :
  HAdd.hAdd (α := A) (β := A)
        (∑ x ∈ range (q - 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : A)
        ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) : A) +
      ∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    0 + (q - 1)! • eval r p' +
      HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
⊢ ∑ x ∈ range q ∪ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    0 + (q - 1)! • eval r p' +
      HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
have inr₁ : Disjoint (range q) (Ico q (p.natDegree + 1))
Tactic: rw [sum_union, this, sum_range_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
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)
⊢ HAdd.hAdd (α := A) (β := A)
        (∑ x ∈ range (q - 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : A)
        ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) : A) +
      ∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    0 + (q - 1)! • eval r p' +
      HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
have inr : Eq.{u_3 + 1} (α := A) (∑ x ∈ range (q - 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p)) 0
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
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)
inr :
  Eq.{u_3 + 1} (α := A) (∑ x ∈ range (q - 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p)) 0
⊢ HAdd.hAdd (α := A) (β := A)
        (∑ x ∈ range (q - 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : A)
        ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) : A) +
      ∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    0 + (q - 1)! • eval r p' +
      HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
have inr₁ : (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) = (q - 1)! • eval r p'
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
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)
inr :
  Eq.{u_3 + 1} (α := A) (∑ x ∈ range (q - 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p)) 0
inr₁ : (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) = (q - 1)! • eval r p'
⊢ HAdd.hAdd (α := A) (β := A)
        (∑ x ∈ range (q - 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : A)
        ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) : A) +
      ∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    0 + (q - 1)! • eval r p' +
      HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
have inr₂ : ∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
  HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
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)
⊢ Eq.{u_3 + 1} (α := A) (∑ x ∈ range (q - 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p)) 0
have inr : ∀ x ∈ range (q - 1),
  Eq.{u_3 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) : A) (0 : A)
Tactic: apply sum_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
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)
⊢ (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) = (q - 1)! • eval r p'
have inr : Eq.{u_3 + 1} (α := A) ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) : A)
  ((aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[q - 1] p) : A)
Tactic: rw [← aeval_iterate_derivative_self _ _ _ hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
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 ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    HSMul.hSMul (β := A) q ! (∑ x ∈ Ico q (p.natDegree + 1), (aeval r : (a : R[X]) → A) (c x))
have inr : ∀ x ∈ Ico q (p.natDegree + 1),
  (aeval r : (a : R[X]) → A) ((⇑derivative : (a : R[X]) → R[X])^[x] p) =
    HSMul.hSMul (β := A) q ! ((aeval r : (a : R[X]) → A) (c x) : A)
Tactic: rw [smul_sum, sum_congr rfl]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (goal)
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)
⊢ Disjoint (range q) (Ico q (p.natDegree + 1))
have inr : ∀ (x : ℕ), x ∉ Ico 0 q ∩ Ico q (p.natDegree + 1)
Tactic: rw [range_eq_Ico, disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SumIteratedDerivative (hypothesis)
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 : x ∈ Ico 0 q ∩ Ico q (p.natDegree + 1)
⊢ False
have hx₁ : (0 ≤ x ∧ x < q) ∧ q ≤ x ∧ x < p.natDegree + 1
Tactic: rw [mem_inter, mem_Ico, mem_Ico] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ (taylor 0 : (a : R[X]) → R[X]) f = f
have rw : f.comp (HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 0)) = f
Tactic: rw [taylor_apply, C_0, add_zero, comp_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ (taylor 0 : (a : R[X]) → R[X]) f = f
have rw₁ : f.comp (HAdd.hAdd (α := R[X]) X 0) = f
Tactic: rw [taylor_apply, C_0, add_zero, comp_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ (taylor 0 : (a : R[X]) → R[X]) f = f
have rw₂ : f.comp X = f
Tactic: rw [taylor_apply, C_0, add_zero, comp_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ (taylor 0 : (a : R[X]) → R[X]) f = f
have rw₃ : f = f
Tactic: rw [taylor_apply, C_0, add_zero, comp_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
n : ℕ
⊢ Eq (α := R) ((lcoeff R n ∘ₗ taylor r : (a : R[X]) → R) f : R) ((leval r ∘ₗ hasseDeriv n : (a : R[X]) → R) f : R)
have e_a : lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
⊢ lcoeff R n ∘ₗ taylor r = leval r ∘ₗ hasseDeriv n
have 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)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
n 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
n i : ℕ
⊢ ∑ 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)
have e_a : (if n < i + 1 then r ^ (i - n) * (↑(i.choose n) : R) else 0) = r ^ (i - n) * (↑(i.choose n) : R)
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
n i : ℕ
⊢ (if n < i + 1 then r ^ (i - n) * (↑(i.choose n) : R) else 0) = r ^ (i - n) * (↑(i.choose n) : R)
have pos : ∀ (h : n < i + 1), r ^ (i - n) * (↑(i.choose n) : R) = r ^ (i - n) * (↑(i.choose n) : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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)
⊢ (if n < i + 1 then r ^ (i - n) * (↑(i.choose n) : R) else 0) = r ^ (i - n) * (↑(i.choose n) : R)
have neg : ∀ (h : ¬n < i + 1), 0 = r ^ (i - n) * (↑(i.choose n) : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
r : R
n i : ℕ
h : ¬n < i + 1
⊢ 0 = r ^ (i - n) * (↑(i.choose n) : R)
have h₁ : i + 1 ≤ n
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
⊢ 0 = r ^ (i - n) * (↑(i.choose n) : R)
have neg : 0 = r ^ (i - n) * (↑0 : R)
Tactic: rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
n i : ℕ
h : i + 1 ≤ n
neg : 0 = r ^ (i - n) * (↑0 : R)
⊢ 0 = r ^ (i - n) * (↑(i.choose n) : R)
have neg₁ : 0 = r ^ (i - n) * 0
Tactic: rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ 0 = r ^ (i - n) * (↑(i.choose n) : R)
have neg₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) 0 = eval r f
have rw : eval r ((hasseDeriv 0 : (a : R[X]) → R[X]) f) = eval r f
Tactic: rw [taylor_coeff, hasseDeriv_zero, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) 0 = eval r f
have rw₁ : eval r ((LinearMap.id : (a : R[X]) → R[X]) f) = eval r f
Tactic: rw [taylor_coeff, hasseDeriv_zero, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) 0 = eval r f
have rw₂ : eval r f = eval r f
Tactic: rw [taylor_coeff, hasseDeriv_zero, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) 1 = eval r ((derivative : (a : R[X]) → R[X]) f)
have rw : eval r ((hasseDeriv 1 : (a : R[X]) → R[X]) f) = eval r ((derivative : (a : R[X]) → R[X]) f)
Tactic: rw [taylor_coeff, hasseDeriv_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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)
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) 1 = eval r ((derivative : (a : R[X]) → R[X]) f)
have rw₁ : eval r ((derivative : (a : R[X]) → R[X]) f) = eval r ((derivative : (a : R[X]) → R[X]) f)
Tactic: rw [taylor_coeff, hasseDeriv_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff
have pos : ∀ (hf : f = 0), coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Taylor (goal)
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
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff
have neg : ∀ (hf : ¬f = 0), coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff
Tactic: by_cases hf : f = 0
-- 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 pos : Eq (α := R) (coeff ((taylor r : (a : R[X]) → R[X]) 0) (natDegree.{u_1} (R := R) 0)) (leadingCoeff 0)
Tactic: rw [hf, map_zero, coeff_natDegree]
-- 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
pos : Eq (α := R) (coeff ((taylor r : (a : R[X]) → R[X]) 0) (natDegree.{u_1} (R := R) 0)) (leadingCoeff 0)
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff
have pos₁ : Eq.{u_1 + 1} (α := R) (coeff 0 (natDegree.{u_1} (R := R) 0)) (leadingCoeff 0)
Tactic: rw [hf, map_zero, coeff_natDegree]
-- 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
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)
⊢ coeff ((taylor r : (a : R[X]) → R[X]) f) f.natDegree = f.leadingCoeff
have pos₂ : Eq.{u_1 + 1} (α := R) (leadingCoeff 0) (leadingCoeff 0)
Tactic: rw [hf, map_zero, coeff_natDegree]