awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
c : R
rw :
  HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]))
      ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
    (C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
rw₁ :
  (C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) * 1 =
    (C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
⊢ (derivative : (a : R[X]) → R[X])
      (HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) 2) =
    (C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
have rw₂ : (C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) =
  (C : (a : R) → R[X]) 2 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
Tactic: rw [derivative_sq, derivative_X_sub_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
n k : ℕ
c : R
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    n.descFactorial k • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - k)
have rw : (⇑derivative : (a : R[X]) → R[X])^[k] (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) c : R[X]) ^ n) =
  n.descFactorial k • HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) c : R[X]) ^ (n - k)
Tactic: rw [sub_eq_add_neg, ← C_neg, iterate_derivative_X_add_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
n k : ℕ
c : R
rw :
  (⇑derivative : (a : R[X]) → R[X])^[k] (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) c : R[X]) ^ n) =
    n.descFactorial k • HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) c : R[X]) ^ (n - k)
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    n.descFactorial k • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - k)
have rw₁ : (⇑derivative : (a : R[X]) → R[X])^[k] (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-c) : R[X]) ^ n) =
  n.descFactorial k • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-c) : R[X]) ^ (n - k)
Tactic: rw [sub_eq_add_neg, ← C_neg, iterate_derivative_X_add_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
n k : ℕ
c : R
rw :
  (⇑derivative : (a : R[X]) → R[X])^[k] (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) c : R[X]) ^ n) =
    n.descFactorial k • HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) c : R[X]) ^ (n - k)
rw₁ :
  (⇑derivative : (a : R[X]) → R[X])^[k] (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-c) : R[X]) ^ n) =
    n.descFactorial k • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-c) : R[X]) ^ (n - k)
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    n.descFactorial k • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - k)
have rw₂ : n.descFactorial k • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-c) : R[X]) ^ (n - k) =
  n.descFactorial k • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-c) : R[X]) ^ (n - k)
Tactic: rw [sub_eq_add_neg, ← C_neg, iterate_derivative_X_add_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
c : R
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    (↑n ! : R[X])
have rw : n.descFactorial n • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - n) = (↑n ! : R[X])
Tactic: rw [iterate_derivative_X_sub_pow, n.sub_self, pow_zero, nsmul_one, n.descFactorial_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
c : R
rw : n.descFactorial n • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - n) = (↑n ! : R[X])
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    (↑n ! : R[X])
have rw₁ : n.descFactorial n • HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) 0 =
  (↑n ! : R[X])
Tactic: rw [iterate_derivative_X_sub_pow, n.sub_self, pow_zero, nsmul_one, n.descFactorial_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
c : R
rw : n.descFactorial n • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - n) = (↑n ! : R[X])
rw₁ :
  n.descFactorial n • HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) 0 =
    (↑n ! : R[X])
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    (↑n ! : R[X])
have rw₂ : HSMul.hSMul (β := R[X]) (n.descFactorial n) 1 = (↑n ! : R[X])
Tactic: rw [iterate_derivative_X_sub_pow, n.sub_self, pow_zero, nsmul_one, n.descFactorial_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
c : R
rw : n.descFactorial n • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - n) = (↑n ! : R[X])
rw₁ :
  n.descFactorial n • HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) 0 =
    (↑n ! : R[X])
rw₂ : HSMul.hSMul (β := R[X]) (n.descFactorial n) 1 = (↑n ! : R[X])
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    (↑n ! : R[X])
have rw₃ : Eq.{u + 1} (α := R[X]) (↑(n.descFactorial n) : R[X]) (↑n ! : R[X])
Tactic: rw [iterate_derivative_X_sub_pow, n.sub_self, pow_zero, nsmul_one, n.descFactorial_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
c : R
rw : n.descFactorial n • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - n) = (↑n ! : R[X])
rw₁ :
  n.descFactorial n • HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) 0 =
    (↑n ! : R[X])
rw₂ : HSMul.hSMul (β := R[X]) (n.descFactorial n) 1 = (↑n ! : R[X])
rw₃ : Eq.{u + 1} (α := R[X]) (↑(n.descFactorial n) : R[X]) (↑n ! : R[X])
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    (↑n ! : R[X])
have rw₄ : Eq.{u + 1} (α := R[X]) (↑n ! : R[X]) (↑n ! : R[X])
Tactic: rw [iterate_derivative_X_sub_pow, n.sub_self, pow_zero, nsmul_one, n.descFactorial_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
k : ℕ
P : R[X]
h : P.degree < (↑k : WithBot ℕ)
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
have induction : ∀ {P : R[X]} (h : P.degree < (↑0 : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[0] P = 0
Tactic: induction k generalizing P
Cleared hypotheses: k, P, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
k : ℕ
P : R[X]
h : P.degree < (↑k : WithBot ℕ)
induction : ∀ {P : R[X]} (h : P.degree < (↑0 : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[0] P = 0
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
have succ : ∀ (n : ℕ),
  (∀ {P : R[X]} (h : P.degree < (↑n : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[n] P = 0) →
    ∀ {P : R[X]} (h : P.degree < (↑(n + 1) : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[n + 1] P = 0
Tactic: induction k generalizing P
Cleared hypotheses: k, P, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1] P = 0
have pos : P = 0 → (⇑derivative : (a : R[X]) → R[X])^[k + 1] P = 0
Tactic: by_cases P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
pos : P = 0 → (⇑derivative : (a : R[X]) → R[X])^[k + 1] P = 0
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1] P = 0
have neg : ¬P = 0 → (⇑derivative : (a : R[X]) → R[X])^[k + 1] P = 0
Tactic: by_cases P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1] P = 0
have rw : Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])
Tactic: rw [Function.iterate_add_apply, Function.iterate_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])
have pos : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X]) →
  Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])
Tactic: by_cases derivative P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
pos :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X]) →
    Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])
have neg : ¬Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X]) →
  Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])
Tactic: by_cases derivative P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
hP' : ¬Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
⊢ P.natDegree ≠ 0
have contrapose : ∀ (hP' : P.natDegree = 0), Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
Tactic: contrapose hP'
Cleared hypotheses: hP'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
hP' : ¬Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])
have hP'' : P.natDegree ≠ 0
Tactic: have hP'' : P.natDegree ≠ 0 := by
          contrapose hP'
          exact derivative_of_natDegree_zero hP'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
hP' : ¬Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
hP'' : P.natDegree ≠ 0
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])
have refine : natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) P) < k
Tactic: refine ind <| (natDegree_lt_iff_degree_lt hP').mp ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
hP' : ¬Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
hP'' : P.natDegree ≠ 0
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) P) < k
have linarith : k ≤ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) P) →
  -1 + HSub.hSub (α := ℤ) (↑k : ℤ) (↑(natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) P)) : ℤ) +
        (HAdd.hAdd (α := ℤ) (↑P.natDegree : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) +
      (HAdd.hAdd (α := ℤ) (↑(natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) P)) : ℤ) 1 - (↑P.natDegree : ℤ)) =
    0
Tactic: linarith [(natDegree_lt_iff_degree_lt hP).mpr h, natDegree_derivative_lt hP'']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
k : ℕ
S : Finset R
hk : k ≤ #S
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑k ! : R[X])
      (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have induction : ∀ (hk : 0 ≤ #S),
  (⇑derivative : (a : R[X]) → R[X])^[0] (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑0! : R[X])
      (∑ T ∈ powersetCard (#S - 0) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: induction k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
k : ℕ
S : Finset R
hk : k ≤ #S
induction :
  ∀ (hk : 0 ≤ #S),
    (⇑derivative : (a : R[X]) → R[X])^[0]
        (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
      HMul.hMul (α := R[X]) (↑0! : R[X])
        (∑ T ∈ powersetCard (#S - 0) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑k ! : R[X])
      (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have succ : ∀ (n : ℕ),
  (∀ (hk : n ≤ #S),
      (⇑derivative : (a : R[X]) → R[X])^[n]
          (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
        HMul.hMul (α := R[X]) (↑n ! : R[X])
          (∑ T ∈ powersetCard (#S - n) S,
            ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))) →
    ∀ (hk : n + 1 ≤ #S),
      (⇑derivative : (a : R[X]) → R[X])^[n + 1]
          (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
        HMul.hMul (α := R[X]) (↑(n + 1)! : R[X])
          (∑ T ∈ powersetCard (#S - (n + 1)) S,
            ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: induction k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Finset R
k : ℕ
ind :
  ∀ (hk : k ≤ #S),
    (⇑derivative : (a : R[X]) → R[X])^[k]
        (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
      HMul.hMul (α := R[X]) (↑k ! : R[X])
        (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
hk : k + 1 ≤ #S
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1]
      (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑(k + 1)! : R[X])
      (∑ T ∈ powersetCard (#S - (k + 1)) S,
        ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have ind₁ : (⇑derivative : (a : R[X]) → R[X])^[k] (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
  HMul.hMul (α := R[X]) (↑k ! : R[X])
    (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: specialize ind (Nat.le_of_succ_le hk)
Cleared hypotheses: ind
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
S : Finset R
k : ℕ
hk : k + 1 ≤ #S
ind :
  (⇑derivative : (a : R[X]) → R[X])^[k] (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑k ! : R[X])
      (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1]
      (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑(k + 1)! : R[X])
      (∑ T ∈ powersetCard (#S - (k + 1)) S,
        ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have nth_rewrite : (⇑derivative : (a : R[X]) → R[X])^[1 + k]
    (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
  HMul.hMul (α := R[X]) (↑(k + 1)! : R[X])
    (∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: nth_rewrite 1 [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
S : Finset R
k : ℕ
hk : k + 1 ≤ #S
ind :
  (⇑derivative : (a : R[X]) → R[X])^[k] (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑k ! : R[X])
      (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
⊢ (⇑derivative : (a : R[X]) → R[X])^[1 + k]
      (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑(k + 1)! : R[X])
      (∑ T ∈ powersetCard (#S - (k + 1)) S,
        ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have rw : HMul.hMul (α := R[X]) (↑k ! : R[X])
    (∑ b ∈ powersetCard (#S - k) S,
      (derivative : (a : R[X]) → R[X]) (∏ a ∈ b, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))) =
  (↑k ! : R[X]) *
    HMul.hMul (α := R[X]) (↑(k + 1) : R[X])
      (∑ T ∈ powersetCard (#S - (k + 1)) S,
        ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: rw [Function.iterate_add_apply, Function.iterate_one, ind, ← nsmul_eq_mul, derivative_smul,
      nsmul_eq_mul, derivative_sum, Nat.factorial_succ, mul_comm (k + 1), Nat.cast_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
S : Finset R
k : ℕ
hk : k + 1 ≤ #S
ind :
  (⇑derivative : (a : R[X]) → R[X])^[k] (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑k ! : R[X])
      (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
⊢ HMul.hMul (α := R[X]) (↑k ! : R[X])
      (∑ b ∈ powersetCard (#S - k) S,
        (derivative : (a : R[X]) → R[X])
          (∏ a ∈ b, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))) =
    (↑k ! : R[X]) *
      HMul.hMul (α := R[X]) (↑(k + 1) : R[X])
        (∑ T ∈ powersetCard (#S - (k + 1)) S,
          ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have e_a : ∑ b ∈ powersetCard (#S - k) S,
    (derivative : (a : R[X]) → R[X]) (∏ a ∈ b, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
  HMul.hMul (α := R[X]) (↑(k + 1) : R[X])
    (∑ T ∈ powersetCard (#S - (k + 1)) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
S : Finset R
k : ℕ
hk : k + 1 ≤ #S
ind :
  (⇑derivative : (a : R[X]) → R[X])^[k] (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑k ! : R[X])
      (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
⊢ Eq (α := R[X])
    (∑ T ∈ powersetCard (#S - k) S,
      (derivative : (a : R[X]) → R[X]) (∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])))
    (∑ T ∈ powersetCard (#S - k) S,
      ∑ i ∈ T, ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have a : ∀ (T : Finset R) (hT : T ∈ powersetCard (#S - k) S),
  Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X]) (∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])))
    (∑ i ∈ T, ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: congr! with T hT
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
S : Finset R
k : ℕ
hk : k + 1 ≤ #S
ind :
  (⇑derivative : (a : R[X]) → R[X])^[k] (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑k ! : R[X])
      (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
T : Finset R
hT : T ∈ powersetCard (#S - k) S
⊢ Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X]) (∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])))
    (∑ i ∈ T, ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have a : Eq (α := R[X])
  (∑ a ∈ T,
    HMul.hMul (α := R[X]) (β := R[X])
      (∏ a ∈ T.erase a, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) : R[X])
      ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X]))
  (∑ i ∈ T, ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommRing R
S : Finset R
k : ℕ
hk : k + 1 ≤ #S
ind :
  (⇑derivative : (a : R[X]) → R[X])^[k] (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑k ! : R[X])
      (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
T : Finset R
hT : T ∈ powersetCard (#S - k) S
a :
  Eq (α := R[X])
    (∑ a ∈ T,
      HMul.hMul (α := R[X]) (β := R[X])
        (∏ a ∈ T.erase a, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) : R[X])
        ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X]))
    (∑ i ∈ T, ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
⊢ Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X]) (∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])))
    (∑ i ∈ T, ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have a₁ : Eq (α := R[X])
  (∑ x ∈ T,
    HMul.hMul (α := R[X]) (∏ a ∈ T.erase x, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 1)
  (∑ i ∈ T, ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]