-- 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]))
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
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),
        ⋯ with
      | (T, i), x => (T.erase i, i)) =
      a
h :
  ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match (motive := Finset R × R → Prop) x with
          | (T, i) => i ∈ T}),
    Eq (α := R[X])
      (match (motive := Finset R × R → R[X]) a with
        | (T, i) => ∏ a ∈ T.erase i, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) :
        R[X])
      (match (motive := Finset R × R → R[X])
          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) => ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) :
        R[X])
hi :
  ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match (motive := Finset R × R → Prop) x with
          | (T, i) => i ∈ T}),
    Membership.mem (α := Finset R × R)
      ({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)
          a, ha with
        | (T, i), x => (T.erase i, i) :
        Finset R × R)
hj :
  ∀ (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}),
    Membership.mem (α := Finset R × R)
      ({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)
          a, ha with
        | (T, i), x => (insert i T, i) :
        Finset R × R)
⊢ 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:
apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)

Premises used: Finset.sum_bij'