-- Module: Mathlib.Algebra.Polynomial.Derivative
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]))
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]))
T₃ :
  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]))
T₄ :
  ∑ 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])
T₅ :
  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]) =
    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]))
⊢ ∑ 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:
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

Premises used: HSub.hSub, HAdd.hAdd, Finset.powersetCard, Finset.card, OfNat.ofNat