awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Derivative
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]))
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]))
⊢ (⇑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:
induction k
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
S : Finset R
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:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
S : Finset R
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:
case zero => simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
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] (∏ 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)

Premises used: Nat.le_of_succ_le
-- 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]))
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]))
⊢ (⇑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]))

Tactic:
nth_rewrite 1 [add_comm]

Premises used: add_comm
-- 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]))
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]))
⊢ (⇑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:
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]

Premises used: Polynomial.derivative_sum, Polynomial.derivative_smul, Function.iterate_add_apply, Nat.factorial_succ, mul_assoc, Nat.cast_mul, Function.iterate_one, HAdd.hAdd, mul_comm, nsmul_eq_mul, OfNat.ofNat
-- 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]))
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]))
⊢ 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:
congr 1
-- 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]))
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]))
⊢ 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:
congr! with T hT
-- 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 : 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]))
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]))
⊢ 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:
simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]

Premises used: Polynomial.derivative_prod_finset, mul_one, Polynomial.derivative_X_sub_C
-- 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]))
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
⊢ 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:
rw [← sum_finset_product']

Premises used: Finset.sum_finset_product'
-- 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]))
⊢ ∀ (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:
grind
-- 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]))
r : Finset R × R
hr :
  r ∈
    {x ∈ powersetCard (#S - k) S ×ˢ S |
      match (motive := Finset R × R → Prop) x with
      | (T, i) => i ∈ T}
left_neg : (insert r.2 (r.1.erase r.2), r.2) = 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)
      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)
        r, hr with
      | (T, i), x => (T.erase i, i),
      ⋯ with
    | (T, i), x => (insert i T, i)) =
    r

Tactic:
dsimp at hr ⊢
-- 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]))
r : Finset R × R
hr : r ∈ {x ∈ powersetCard (#S - k) S ×ˢ S | x.2 ∈ x.1}
left_neg : insert r.2 (r.1.erase r.2) = r.1
⊢ (insert r.2 (r.1.erase r.2), r.2) = r

Tactic:
congr 1
-- 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]))
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.1

Tactic:
grind
-- 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]))
r : Finset R × R
hr :
  r ∈
    {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
      match (motive := Finset R × R → Prop) x with
      | (T, i) => i ∉ T}
right_neg : ((insert r.2 r.1).erase r.2, r.2) = 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)
      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)
        r, hr with
      | (T, i), x => (insert i T, i),
      ⋯ with
    | (T, i), x => (T.erase i, i)) =
    r

Tactic:
dsimp at hr ⊢
-- 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]))
r : Finset R × R
hr : r ∈ {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S | x.2 ∉ x.1}
right_neg : (insert r.2 r.1).erase r.2 = r.1
⊢ ((insert r.2 r.1).erase r.2, r.2) = r

Tactic:
congr 1
-- 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]))
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.1

Tactic:
grind
-- 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]))
⊢ ∀ (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])

Tactic:
grind
-- 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]))
⊢ ∀ (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)

Tactic:
grind
-- 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]))
⊢ ∀ (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)

Tactic:
grind
-- 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]))
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
⊢ 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]))

Tactic:
rw [← sum_finset_product']

Premises used: Finset.sum_finset_product'
-- 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]))
⊢ ∀ (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:
grind
-- 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]))
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]))
⊢ ∑ 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])

Tactic:
rw [mul_sum]

Premises used: Finset.mul_sum
-- 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]))
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])
⊢ 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:
congr! 1 with T hT
-- 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 : Finset R
hT : T ∈ powersetCard (#S - (k + 1)) S
⊢ #(S \ T) = k + 1

Tactic:
grind
-- 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 : 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:
simp [sum_const, show #(S \ T) = k + 1 by grind]

Premises used: Finset.sum_const