awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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,
      ∑ i ∈ T, ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
    (∑ x ∈ powersetCard (#S - k) S ×ˢ S with
      match (motive := Finset R × R → Prop) x with
      | (T, i) => i ∈ T,
      match (motive := Finset R × R → R[X]) x with
      | (T, i) => ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have h : ∀ (p : Finset R × R),
  p ∈
      {x ∈ powersetCard (#S - k) S ×ˢ S |
        match (motive := Finset R × R → Prop) x with
        | (T, i) => i ∈ T} ↔
    p.1 ∈ powersetCard (#S - k) S ∧ p.2 ∈ p.1
Tactic: rw [← sum_finset_product']
-- 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])
    (∑ x ∈ powersetCard (#S - k) S ×ˢ S with
      match (motive := Finset R × R → Prop) x with
      | (T, i) => i ∈ T,
      match (motive := Finset R × R → R[X]) x with
      | (T, i) => ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
    (∑ x ∈ powersetCard (#S - (k + 1)) S ×ˢ S with
      match (motive := Finset R × R → Prop) x with
      | (T, i) => i ∉ T,
      match (motive := Finset R × R → R[X]) x with
      | (T, i) => ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have left_neg : ∀ (a : Finset R × R)
  (ha :
    a ∈
      {x ∈ powersetCard (#S - k) S ×ˢ S |
        match (motive := Finset R × R → Prop) x with
        | (T, i) => i ∈ T}),
  (match (motive :=
      (x : Finset R × R) →
        x ∈
            {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
              match (motive := Finset R × R → Prop) x with
              | (T, i) => i ∉ T} →
          Finset R × R)
      match (motive :=
        (x : Finset R × R) →
          x ∈
              {x ∈ powersetCard (#S - k) S ×ˢ S |
                match (motive := Finset R × R → Prop) x with
                | (T, i) => i ∈ T} →
            Finset R × R)
        a, ha with
      | (T, i), x => (T.erase i, i),
      sorry with
    | (T, i), x => (insert i T, i)) =
    a
Tactic: apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
-- 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]))
left_neg :
  ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match (motive := Finset R × R → Prop) x with
          | (T, i) => i ∈ T}),
    (match (motive :=
        (x : Finset R × R) →
          x ∈
              {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
                match (motive := Finset R × R → Prop) x with
                | (T, i) => i ∉ T} →
            Finset R × R)
        match (motive :=
          (x : Finset R × R) →
            x ∈
                {x ∈ powersetCard (#S - k) S ×ˢ S |
                  match (motive := Finset R × R → Prop) x with
                  | (T, i) => i ∈ T} →
              Finset R × R)
          a, ha with
        | (T, i), x => (T.erase i, i),
        ⋯ with
      | (T, i), x => (insert i T, i)) =
      a
⊢ Eq (α := R[X])
    (∑ x ∈ powersetCard (#S - k) S ×ˢ S with
      match (motive := Finset R × R → Prop) x with
      | (T, i) => i ∈ T,
      match (motive := Finset R × R → R[X]) x with
      | (T, i) => ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
    (∑ x ∈ powersetCard (#S - (k + 1)) S ×ˢ S with
      match (motive := Finset R × R → Prop) x with
      | (T, i) => i ∉ T,
      match (motive := Finset R × R → R[X]) x with
      | (T, i) => ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have right_neg : ∀ (a : Finset R × R)
  (ha :
    a ∈
      {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
        match (motive := Finset R × R → Prop) x with
        | (T, i) => i ∉ T}),
  (match (motive :=
      (x : Finset R × R) →
        x ∈
            {x ∈ powersetCard (#S - k) S ×ˢ S |
              match (motive := Finset R × R → Prop) x with
              | (T, i) => i ∈ T} →
          Finset R × R)
      match (motive :=
        (x : Finset R × R) →
          x ∈
              {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
                match (motive := Finset R × R → Prop) x with
                | (T, i) => i ∉ T} →
            Finset R × R)
        a, ha with
      | (T, i), x => (insert i T, i),
      sorry with
    | (T, i), x => (T.erase i, i)) =
    a
Tactic: apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
-- 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]))
r : Finset R × R
hr : r ∈ {x ∈ powersetCard (#S - k) S ×ˢ S | x.2 ∈ x.1}
⊢ (insert r.2 (r.1.erase r.2), r.2) = r
have left_neg : insert r.2 (r.1.erase r.2) = r.1
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]))
r : Finset R × R
hr : r ∈ {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S | x.2 ∉ x.1}
⊢ ((insert r.2 r.1).erase r.2, r.2) = r
have right_neg : (insert r.2 r.1).erase r.2 = r.1
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])
    (∑ x ∈ powersetCard (#S - (k + 1)) S ×ˢ S with
      match (motive := Finset R × R → Prop) x with
      | (T, i) => i ∉ T,
      match (motive := Finset R × R → R[X]) x with
      | (T, i) => ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
    (∑ T ∈ powersetCard (#S - (k + 1)) S,
      ∑ i ∈ S \ T, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
have h : ∀ (p : Finset R × R),
  p ∈
      {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
        match (motive := Finset R × R → Prop) x with
        | (T, i) => i ∉ T} ↔
    p.1 ∈ powersetCard (#S - (k + 1)) S ∧ p.2 ∈ S \ p.1
Tactic: rw [← sum_finset_product']
-- 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 ∈ powersetCard (#S - (k + 1)) S,
      ∑ i ∈ S \ T, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) =
    HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 *
      ∑ 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 : Eq (α := R[X])
  (∑ T ∈ powersetCard (#S - (k + 1)) S,
    ∑ i ∈ S \ T, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
  (∑ i ∈ powersetCard (#S - (k + 1)) S,
    HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 * ∏ a ∈ i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: rw [mul_sum]
-- 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 + 1)) S,
      ∑ i ∈ S \ T, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
    (∑ i ∈ powersetCard (#S - (k + 1)) S,
      HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 *
        ∏ a ∈ 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 + 1)) S),
  ∑ i ∈ S \ T, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) =
    HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 * ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])
Tactic: congr! 1 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]))
⊢ ∑ 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]))
have T : 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]))
Tactic: calc
      ∑ T ∈ S.powersetCard (#S - k), derivative (∏ a ∈ T, (X - C a)) =
      ∑ T ∈ S.powersetCard (#S - k), ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        congr! with T hT
        simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]
      _ = ∑ (T ∈ S.powersetCard (#S - k)) (i ∈ S) with i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = ∑ (T ∈ S.powersetCard (#S - (k + 1))) (i ∈ S) with i ∉ T, ∏ a ∈ T, (X - C a) := by
        apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        all_goals grind
      _ = ∑ T ∈ S.powersetCard (#S - (k + 1)), ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = (k + 1) * ∑ T ∈ S.powersetCard (#S - (k + 1)), ∏ a ∈ T, (X - C a) := by
        rw [mul_sum]
        congr! 1 with T hT
        simp [sum_const, show #(S \ T) = k + 1 by grind]
      _ = _ := by grind
-- 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 :
  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]))
⊢ ∑ 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]))
have T₁ : Eq (α := 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]))
  (∑ x ∈ powersetCard (#S - k) S ×ˢ S with
    match (motive := Finset R × R → Prop) x with
    | (T, i) => i ∈ T,
    match (motive := Finset R × R → R[X]) x with
    | (T, i) => ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: calc
      ∑ T ∈ S.powersetCard (#S - k), derivative (∏ a ∈ T, (X - C a)) =
      ∑ T ∈ S.powersetCard (#S - k), ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        congr! with T hT
        simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]
      _ = ∑ (T ∈ S.powersetCard (#S - k)) (i ∈ S) with i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = ∑ (T ∈ S.powersetCard (#S - (k + 1))) (i ∈ S) with i ∉ T, ∏ a ∈ T, (X - C a) := by
        apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        all_goals grind
      _ = ∑ T ∈ S.powersetCard (#S - (k + 1)), ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = (k + 1) * ∑ T ∈ S.powersetCard (#S - (k + 1)), ∏ a ∈ T, (X - C a) := by
        rw [mul_sum]
        congr! 1 with T hT
        simp [sum_const, show #(S \ T) = k + 1 by grind]
      _ = _ := by grind
-- 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 :
  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]))
T₁ :
  Eq (α := 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]))
    (∑ x ∈ powersetCard (#S - k) S ×ˢ S with
      match (motive := Finset R × R → Prop) x with
      | (T, i) => i ∈ T,
      match (motive := Finset R × R → R[X]) x with
      | (T, i) => ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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])) =
    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 T₂ : Eq (α := R[X])
  (∑ x ∈ powersetCard (#S - k) S ×ˢ S with
    match (motive := Finset R × R → Prop) x with
    | (T, i) => i ∈ T,
    match (motive := Finset R × R → R[X]) x with
    | (T, i) => ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
  (∑ x ∈ powersetCard (#S - (k + 1)) S ×ˢ S with
    match (motive := Finset R × R → Prop) x with
    | (T, i) => i ∉ T,
    match (motive := Finset R × R → R[X]) x with
    | (T, i) => ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
Tactic: calc
      ∑ T ∈ S.powersetCard (#S - k), derivative (∏ a ∈ T, (X - C a)) =
      ∑ T ∈ S.powersetCard (#S - k), ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        congr! with T hT
        simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]
      _ = ∑ (T ∈ S.powersetCard (#S - k)) (i ∈ S) with i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = ∑ (T ∈ S.powersetCard (#S - (k + 1))) (i ∈ S) with i ∉ T, ∏ a ∈ T, (X - C a) := by
        apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        all_goals grind
      _ = ∑ T ∈ S.powersetCard (#S - (k + 1)), ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = (k + 1) * ∑ T ∈ S.powersetCard (#S - (k + 1)), ∏ a ∈ T, (X - C a) := by
        rw [mul_sum]
        congr! 1 with T hT
        simp [sum_const, show #(S \ T) = k + 1 by grind]
      _ = _ := by grind
-- 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: classical
  induction k
  case zero => simp
  case succ k ind =>
    specialize ind (Nat.le_of_succ_le hk)
    nth_rewrite 1 [add_comm]
    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]
    congr 1
    calc
      ∑ T ∈ S.powersetCard (#S - k), derivative (∏ a ∈ T, (X - C a)) =
      ∑ T ∈ S.powersetCard (#S - k), ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        congr! with T hT
        simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]
      _ = ∑ (T ∈ S.powersetCard (#S - k)) (i ∈ S) with i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = ∑ (T ∈ S.powersetCard (#S - (k + 1))) (i ∈ S) with i ∉ T, ∏ a ∈ T, (X - C a) := by
        apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        all_goals grind
      _ = ∑ T ∈ S.powersetCard (#S - (k + 1)), ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = (k + 1) * ∑ T ∈ S.powersetCard (#S - (k + 1)), ∏ a ∈ T, (X - C a) := by
        rw [mul_sum]
        congr! 1 with T hT
        simp [sum_const, show #(S \ T) = k + 1 by grind]
      _ = _ := by grind
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: classical
  induction k
  case zero => simp
  case succ k ind =>
    specialize ind (Nat.le_of_succ_le hk)
    nth_rewrite 1 [add_comm]
    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]
    congr 1
    calc
      ∑ T ∈ S.powersetCard (#S - k), derivative (∏ a ∈ T, (X - C a)) =
      ∑ T ∈ S.powersetCard (#S - k), ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        congr! with T hT
        simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]
      _ = ∑ (T ∈ S.powersetCard (#S - k)) (i ∈ S) with i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = ∑ (T ∈ S.powersetCard (#S - (k + 1))) (i ∈ S) with i ∉ T, ∏ a ∈ T, (X - C a) := by
        apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        all_goals grind
      _ = ∑ T ∈ S.powersetCard (#S - (k + 1)), ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = (k + 1) * ∑ T ∈ S.powersetCard (#S - (k + 1)), ∏ a ∈ T, (X - C a) := by
        rw [mul_sum]
        congr! 1 with T hT
        simp [sum_const, show #(S \ T) = k + 1 by grind]
      _ = _ := by grind
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
P : R[X]
h : P ∣ (derivative : (a : R[X]) → R[X]) P
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
have pos : ∀ (hP : P = 0), Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
Tactic: by_cases hP : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
P : R[X]
h : P ∣ (derivative : (a : R[X]) → R[X]) P
pos : ∀ (hP : P = 0), Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
have neg : ∀ (hP : ¬P = 0), Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
Tactic: by_cases hP : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
n : ℕ
chn : Ne.{u + 1} (α := R) (↑n : R) 0
a : R[X]
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (a ^ n) : R[X]) (0 : R[X]) ↔
    Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])
have inst : Nontrivial R
Tactic: nontriviality R