-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_mul (f g : R[X]) :
    hasseDeriv k (f * g) = ∑ ij ∈ antidiagonal k, hasseDeriv ij.1 f * hasseDeriv ij.2 g

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hx : x.1 + x.2 = 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))

Tactic:
subst hx

Result:
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ (hasseDeriv k) (f * g) = ∑ ij ∈ antidiagonal k, (hasseDeriv ij.1) f * (hasseDeriv ij.2) g

Tactic:
show
  (compHom (D k)).comp Φ f g =
    ∑ ij ∈ antidiagonal k, ((compHom.comp ((compHom Φ) (D ij.1))).flip (D ij.2) f) g

Result:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ (((compHom (D k)).comp Φ) f) g = ∑ ij ∈ antidiagonal k, (((compHom.comp ((compHom Φ) (D ij.1))).flip (D ij.2)) f) g

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
⊢ (hasseDeriv k) (f * g) = ∑ ij ∈ antidiagonal k, (hasseDeriv ij.1) f * (hasseDeriv ij.2) g

Tactic:
let Φ := @AddMonoidHom.mul R[X] _

Result:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ (hasseDeriv k) (f * g) = ∑ ij ∈ antidiagonal k, (hasseDeriv ij.1) f * (hasseDeriv ij.2) g

Proof state:
case e_a.e_a
R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ (compHom (D k)).comp Φ = ∑ x ∈ antidiagonal k, (compHom.comp ((compHom Φ) (D x.1))).flip (D x.2)

Tactic:
ext m r n s : 4

Result:
case e_a.e_a.h.h.h.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ (((((compHom (D k)).comp Φ).comp (monomial m).toAddMonoidHom) r).comp (monomial n).toAddMonoidHom) s =
    ((((∑ x ∈ antidiagonal k, (compHom.comp ((compHom Φ) (D x.1))).flip (D x.2)).comp (monomial m).toAddMonoidHom)
            r).comp
        (monomial n).toAddMonoidHom)
      s

Proof state:
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
by_cases hm : m < x.1

Result:
case pos
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : m < x.1
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : ¬m < x.1
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : ¬m < x.1
hn : ¬n < x.2
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
push_neg at hm hn

Result:
case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : x.1 ≤ m
hn : x.2 ≤ n
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ (((compHom (D k)).comp Φ) f) g = ((∑ x ∈ antidiagonal k, (compHom.comp ((compHom Φ) (D x.1))).flip (D x.2)) f) g

Tactic:
congr 2

Result:
case e_a.e_a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
⊢ (compHom (D k)).comp Φ = ∑ x ∈ antidiagonal k, (compHom.comp ((compHom Φ) (D x.1))).flip (D x.2)

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : ¬m < x.1
hn : n < x.2
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
simp only [Nat.choose_eq_zero_of_lt hn, Nat.cast_zero, zero_mul,
           mul_zero, monomial_zero_right]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : ¬m < x.1
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
by_cases hn : n < x.2

Result:
case pos
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : ¬m < x.1
hn : n < x.2
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

case neg
R : Type u_1
inst✝ : Semiring R
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hm : ¬m < x.1
hn : ¬n < x.2
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - (x.1 + x.2))) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
⊢ (hasseDeriv k) (f * g) = ∑ ij ∈ antidiagonal k, (hasseDeriv ij.1) f * (hasseDeriv ij.2) g

Tactic:
let D k := (@hasseDeriv R _ k).toAddMonoidHom

Result:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f g : R[X]
D : ℕ → R[X] →+ R[X] := fun k => (hasseDeriv k).toAddMonoidHom
⊢ (hasseDeriv k) (f * g) = ∑ ij ∈ antidiagonal k, (hasseDeriv ij.1) f * (hasseDeriv ij.2) g