-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_comp (k l : ℕ) :
    (@hasseDeriv R _ k).comp (hasseDeriv l) = (k + l).choose k • hasseDeriv (k + l)

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
hil : l ≤ i
⊢ (i - l).choose k * i.choose l = 0

Tactic:
rw [← tsub_lt_iff_right hil] at hikl

Result:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
⊢ (i - l).choose k * i.choose l = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
⊢ (i - l).choose k * i.choose l = 0

Tactic:
rw [choose_eq_zero_of_lt hikl, zero_mul]

Result:
no goals

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
⊢ ↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))

Tactic:
have h2 : k ≤ i - l := le_tsub_of_add_le_right hikl

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
⊢ ↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : ¬i < k + l
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Tactic:
push_neg at hikl

Result:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Proof state:
R : Type u_1
inst✝ : Semiring R
k l : ℕ
⊢ hasseDeriv k ∘ₗ hasseDeriv l = (k + l).choose k • hasseDeriv (k + l)

Tactic:
ext i : 2

Result:
case h.h
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ ((hasseDeriv k ∘ₗ hasseDeriv l) ∘ₗ monomial i) 1 = (((k + l).choose k • hasseDeriv (k + l)) ∘ₗ monomial i) 1

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
hil : i < l
⊢ (i - l).choose k * i.choose l = 0

Tactic:
rw [choose_eq_zero_of_lt hil, mul_zero]

Result:
no goals

Proof state:
case h.h
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (monomial (i - (k + l))) ↑((i - l).choose k * i.choose l) =
    (monomial (i - (k + l))) (↑((k + l).choose k) * ↑(i.choose (k + l)))

Tactic:
rw [← Nat.cast_mul]

Result:
case h.h
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (monomial (i - (k + l))) ↑((i - l).choose k * i.choose l) =
    (monomial (i - (k + l))) ↑((k + l).choose k * i.choose (k + l))

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Tactic:
rw [choose_eq_zero_of_lt hikl, mul_zero]

Result:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = 0

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
⊢ ↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))

Tactic:
have h3 : k ≤ k + l := le_self_add

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑((i - l).choose k) * ↑(i.choose l) = ↑((k + l).choose k) * ↑(i.choose (k + l))

Tactic:
rw [cast_choose ℚ h1, cast_choose ℚ h2, cast_choose ℚ h3, cast_choose ℚ hikl]

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑(k + l - k)!) * (↑i ! / (↑(k + l)! * ↑(i - (k + l))!))

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑(k + l - k)!) * (↑i ! / (↑(k + l)! * ↑(i - (k + l))!))

Tactic:
rw [show i - (k + l) = i - l - k by rw [add_comm]; apply tsub_add_eq_tsub_tsub]

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑(k + l - k)!) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! * ↑i ! * (↑k ! * ↑l ! * (↑(k + l)! * ↑(i - l - k)!)) =
    ↑(k + l)! * ↑i ! * (↑k ! * ↑(i - l - k)! * (↑l ! * ↑(i - l)!))

Tactic:
ring

Result:
no goals

Proof state:
case h.h.h.e_6.h.e_a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Tactic:
by_cases hikl : i < k + l

Result:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : ¬i < k + l
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Proof state:
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (k + l) = i - l - k

Tactic:
rw [add_comm]

Result:
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (l + k) = i - l - k

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = 0

Tactic:
by_cases hil : i < l

Result:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
hil : i < l
⊢ (i - l).choose k * i.choose l = 0

case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
hil : ¬i < l
⊢ (i - l).choose k * i.choose l = 0

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑(k + l - k)!) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))

Tactic:
simp only [add_tsub_cancel_left]

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑l !) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Tactic:
apply @cast_injective ℚ

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ ↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ ↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))

Tactic:
have h1 : l ≤ i := le_of_add_le_right hikl

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
⊢ ↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))

Proof state:
case h.h
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ ((hasseDeriv k ∘ₗ hasseDeriv l) ∘ₗ monomial i) 1 = (((k + l).choose k • hasseDeriv (k + l)) ∘ₗ monomial i) 1

Tactic:
simp only [LinearMap.smul_apply, comp_apply, LinearMap.coe_comp, smul_monomial, hasseDeriv_apply,
  mul_one, monomial_eq_zero_iff, sum_monomial_index, mul_zero, ←
  tsub_add_eq_tsub_tsub, add_comm l k]

Result:
case h.h
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (monomial (i - (k + l))) (↑((i - l).choose k) * ↑(i.choose l)) =
    (monomial (i - (k + l))) ((k + l).choose k • ↑(i.choose (k + l)))

Proof state:
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (l + k) = i - l - k

Tactic:
apply tsub_add_eq_tsub_tsub

Result:
no goals