Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case right_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
          match x with
          | (T, i) => i ∉ T}),
    (match
        match a, ha with
        | (T, i), x => (insert i T, i),
        ⋯ with
      | (T, i), x => (T.erase i, i)) =
      a

pp: case h
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match a with
      | (T, i) => ∏ a ∈ T.erase i, (X - C a)) =
      match
        match a, ha with
        | (T, i), x => (T.erase i, i) with
      | (T, i) => ∏ a ∈ T, (X - C a)

pp: case hi
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match a, ha with
      | (T, i), x => (T.erase i, i)) ∈
      {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
        match x with
        | (T, i) => i ∉ T}

pp: case hj
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
          match x with
          | (T, i) => i ∉ T}),
    (match a, ha with
      | (T, i), x => (insert i T, i)) ∈
      {x ∈ powersetCard (#S - k) S ×ˢ S |
        match x with
        | (T, i) => i ∈ T}

Tactic:
· intro r hr; dsimp at hr ⊢; congr 1; grind

Goal state after:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match a with
      | (T, i) => ∏ a ∈ T.erase i, (X - C a)) =
      match
        match a, ha with
        | (T, i), x => (T.erase i, i) with
      | (T, i) => ∏ a ∈ T, (X - C a)

case hi
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match a, ha with
      | (T, i), x => (T.erase i, i)) ∈
      {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
        match x with
        | (T, i) => i ∉ T}

case hj
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
          match x with
          | (T, i) => i ∉ T}),
    (match a, ha with
      | (T, i), x => (insert i T, i)) ∈
      {x ∈ powersetCard (#S - k) S ×ˢ S |
        match x with
        | (T, i) => i ∈ T}