-- Module: Mathlib.Algebra.Polynomial.HasseDeriv
Goal:
R : Type u_1
inst : Semiring R
D : (k : ℕ) → R[X] →+ R[X] := fun (k : ℕ) ↦ LinearMap.toAddMonoidHom (hasseDeriv k)
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
hn : x.2 ≤ n
neg :
  Eq (α := R[X])
    ((monomial (m + (n - x.2) - x.1) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) : R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])
neg₁ :
  Eq (α := R[X])
    ((monomial (m + n - x.2 - x.1) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) : R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])
neg₂ :
  Eq (α := R[X])
    ((monomial (m + n - (x.2 + x.1)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) : R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])
neg₃ :
  Eq (α := R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) : R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])
neg₄ :
  Eq (α := R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * (r * ((↑(n.choose x.2) : R) * s))) :
      R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])
neg₅ :
  Eq (α := R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * (r * (↑(n.choose x.2) : R) * s)) : R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])
neg₆ :
  Eq (α := R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * ((↑(n.choose x.2) : R) * r * s)) : R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])
neg₇ :
  Eq (α := R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * ((↑(n.choose x.2) : R) * (r * s))) :
      R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])
neg₈ neg₉ :
  Eq (α := R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * ((↑(n.choose x.2) : R) * (r * s))) :
      R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * ((↑(n.choose x.2) : R) * (r * s))) :
      R[X])
⊢ Eq (α := R[X])
    ((monomial (m - x.1 + (n - x.2)) : (a : R) → R[X]) ((↑(m.choose x.1) : R) * r * ((↑(n.choose x.2) : R) * s)) : R[X])
    ((monomial (m + n - (x.1 + x.2)) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])

Tactic:
rw [tsub_add_eq_add_tsub hm, ← add_tsub_assoc_of_le hn, ← tsub_add_eq_tsub_tsub,
      add_comm x.2 x.1, mul_assoc, ← mul_assoc r, ← (Nat.cast_commute _ r).eq, mul_assoc, mul_assoc]

Premises used: add_tsub_assoc_of_le, mul_assoc, add_comm, Prod.fst, tsub_add_eq_add_tsub, tsub_add_eq_tsub_tsub, Prod.snd, Commute.eq, Nat.cast_commute