awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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
pos :
  ∀ (hn : n < x.2),
    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])
⊢ 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])
have neg : ∀ (hn : x.2 ≤ n),
  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: by_cases! hn : n < x.2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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
⊢ 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])
have 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])
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ 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])
have 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])
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ 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])
have 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])
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ 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])
have 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])
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ 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])
have 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])
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ 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])
have 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])
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ 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])
have 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])
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
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])
⊢ 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])
have 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])
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
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
⊢ Eq (α := R[X]) ((monomial (m + n - k) : (a : R) → R[X]) ((↑((m + n).choose k) : R) * (r * s)) : R[X])
    (∑ x ∈ @antidiagonal _ instAddMonoid _ k,
        (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])
have aux : ∀ x ∈ @antidiagonal _ instAddMonoid _ k,
  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 - k) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])
Tactic: have aux :
    ∀ x : ℕ × ℕ,
      x ∈ antidiagonal k →
        monomial (m - x.1 + (n - x.2)) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
          monomial (m + n - k) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s)) := by
    intro x hx
    rw [mem_antidiagonal] at hx
    subst hx
    by_cases! hm : m < x.1
    · simp only [Nat.choose_eq_zero_of_lt hm, Nat.cast_zero, zero_mul,
                 monomial_zero_right]
    by_cases! hn : n < x.2
    · simp only [Nat.choose_eq_zero_of_lt hn, Nat.cast_zero, zero_mul,
                 mul_zero, monomial_zero_right]
    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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
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
aux :
  ∀ x ∈ @antidiagonal _ instAddMonoid _ k,
    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 - k) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
        R[X])
⊢ Eq (α := R[X]) ((monomial (m + n - k) : (a : R) → R[X]) ((↑((m + n).choose k) : R) * (r * s)) : R[X])
    (∑ x ∈ @antidiagonal _ instAddMonoid _ k,
        (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])
have e_a : Eq (α := R[X]) ((monomial (m + n - k) : (a : R) → R[X]) ((↑((m + n).choose k) : R) * (r * s)) : R[X])
  (∑ x ∈ @antidiagonal _ instAddMonoid _ k,
      (monomial (m + n - k) : (a : R) → R[X])
        (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
    R[X])
Tactic: rw [Finset.sum_congr rfl aux]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
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
aux :
  ∀ x ∈ @antidiagonal _ instAddMonoid _ k,
    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 - k) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
        R[X])
⊢ Eq (α := R[X]) ((monomial (m + n - k) : (a : R) → R[X]) ((↑((m + n).choose k) : R) * (r * s)) : R[X])
    (∑ x ∈ @antidiagonal _ instAddMonoid _ k,
        (monomial (m + n - k) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
      R[X])
have e_a : Eq (α := R[X]) ((monomial (m + n - k) : (a : R) → R[X]) ((↑((m + n).choose k) : R) * (r * s)) : R[X])
  ((monomial (m + n - k) : (a : R) → R[X])
      ((∑ i ∈ @antidiagonal _ instAddMonoid _ k, HMul.hMul (α := R) (↑(m.choose i.1) : R) (↑(n.choose i.2) : R)) *
        (r * s)) :
    R[X])
Tactic: rw [← map_sum, ← Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.HasseDeriv (goal)
Goal:
R : Type u_1
inst : Semiring R
k : ℕ
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
aux :
  ∀ x ∈ @antidiagonal _ instAddMonoid _ k,
    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 - k) : (a : R) → R[X])
          (HMul.hMul (α := R) (↑(m.choose x.1) : R) (↑(n.choose x.2) : R) * (r * s)) :
        R[X])
⊢ Eq (α := R[X]) ((monomial (m + n - k) : (a : R) → R[X]) ((↑((m + n).choose k) : R) * (r * s)) : R[X])
    ((monomial (m + n - k) : (a : R) → R[X])
        ((∑ i ∈ @antidiagonal _ instAddMonoid _ k, HMul.hMul (α := R) (↑(m.choose i.1) : R) (↑(n.choose i.2) : R)) *
          (r * s)) :
      R[X])
have e_a : Eq.{u_1 + 1} (α := R) (↑((m + n).choose k) : R)
  (∑ i ∈ @antidiagonal _ instAddMonoid _ k, HMul.hMul (α := R) (↑(m.choose i.1) : R) (↑(n.choose i.2) : R))
Tactic: congr