case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(LinearMap.comp (LinearMap.comp (hasseDeriv k) (hasseDeriv l)) (monomial i)) 1 =
    ↑(LinearMap.comp (choose (k + l) k • hasseDeriv (k + l)) (monomial i)) 1
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l : ℕ
⊢ LinearMap.comp (hasseDeriv k) (hasseDeriv l) = choose (k + l) k • hasseDeriv (k + l)
ext i : 2
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(monomial (i - (k + l))) (↑(choose (i - l) k) * ↑(choose i l)) =
    ↑(monomial (i - (k + l))) (choose (k + l) k • ↑(choose i (k + l)))
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(LinearMap.comp (LinearMap.comp (hasseDeriv k) (hasseDeriv l)) (monomial i)) 1 =
    ↑(LinearMap.comp (choose (k + l) k • hasseDeriv (k + l)) (monomial i)) 1
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]
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(monomial (i - (k + l))) ↑(choose (i - l) k * choose i l) =
    ↑(monomial (i - (k + l))) (↑(choose (k + l) k) * ↑(choose i (k + l)))
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(monomial (i - (k + l))) (↑(choose (i - l) k) * ↑(choose i l)) =
    ↑(monomial (i - (k + l))) (choose (k + l) k • ↑(choose i (k + l)))
rw_mod_cast [nsmul_eq_mul]
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(monomial (i - (k + l))) ↑(choose (i - l) k * choose i l) =
    ↑(monomial (i - (k + l))) ↑(choose (k + l) k * choose i (k + l))
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(monomial (i - (k + l))) ↑(choose (i - l) k * choose i l) =
    ↑(monomial (i - (k + l))) (↑(choose (k + l) k) * ↑(choose i (k + l)))
rw [←Nat.cast_mul]
case h.h.h.e_6.h.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
case h.h
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ ↑(monomial (i - (k + l))) ↑(choose (i - l) k * choose i l) =
    ↑(monomial (i - (k + l))) ↑(choose (k + l) k * choose i (k + l))
congr 2
case pos
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)

case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : ¬i < k + l
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
case h.h.h.e_6.h.e_a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
by_cases hikl : i < k + l
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : ¬i < k + l
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
push_neg at hikl
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
apply @cast_injective ℚ
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
have h1 : l ≤ i := le_of_add_le_right hikl
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
have h2 : k ≤ i - l := le_tsub_of_add_le_right hikl
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
have h3 : k ≤ k + l := le_self_add
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(choose (i - l) k) * ↑(choose i l) = ↑(choose (k + l) k) * ↑(choose i (k + l))
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(choose (i - l) k * choose i l) = ↑(choose (k + l) k * choose i (k + l))
push_cast
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
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))!))
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(choose (i - l) k) * ↑(choose i l) = ↑(choose (k + l) k) * ↑(choose i (k + l))
rw [cast_choose ℚ h1, cast_choose ℚ h2, cast_choose ℚ h3, cast_choose ℚ hikl]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
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)!))
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
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))!))
rw [show i - (k + l) = i - l - k by rw [add_comm]; apply tsub_add_eq_tsub_tsub]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
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)!))
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
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)!))
simp only [add_tsub_cancel_left]
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
H : ∀ (n : ℕ), ↑n ! ≠ 0
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑l !) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
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)!))
have H : ∀ n : ℕ, (n ! : ℚ) ≠ 0 := by exact_mod_cast factorial_ne_zero
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
H : ∀ (n : ℕ), ↑n ! ≠ 0
⊢ ↑(i - l)! * ↑i ! * (↑k ! * ↑l ! * (↑(k + l)! * ↑(i - l - k)!)) =
    ↑(k + l)! * ↑i ! * (↑k ! * ↑(i - l - k)! * (↑l ! * ↑(i - l)!))
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
H : ∀ (n : ℕ), ↑n ! ≠ 0
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑l !) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))
field_simp [H]
no goals
case neg.a
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
H : ∀ (n : ℕ), ↑n ! ≠ 0
⊢ ↑(i - l)! * ↑i ! * (↑k ! * ↑l ! * (↑(k + l)! * ↑(i - l - k)!)) =
    ↑(k + l)! * ↑i ! * (↑k ! * ↑(i - l - k)! * (↑l ! * ↑(i - l)!))
ring
case pos
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
⊢ choose (i - l) k * choose i l = 0
case pos
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
⊢ choose (i - l) k * choose i l = choose (k + l) k * choose i (k + l)
rw [choose_eq_zero_of_lt hikl, mul_zero]
case pos
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
hil : i < l
⊢ choose (i - l) k * choose i l = 0

case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
hil : ¬i < l
⊢ choose (i - l) k * choose i l = 0
case pos
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
⊢ choose (i - l) k * choose i l = 0
by_cases hil : i < l
no goals
case pos
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
hil : i < l
⊢ choose (i - l) k * choose i l = 0
rw [choose_eq_zero_of_lt hil, mul_zero]
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
hil : l ≤ i
⊢ choose (i - l) k * choose i l = 0
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
hil : ¬i < l
⊢ choose (i - l) k * choose i l = 0
push_neg at hil
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
⊢ choose (i - l) k * choose i l = 0
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i < k + l
hil : l ≤ i
⊢ choose (i - l) k * choose i l = 0
rw [← tsub_lt_iff_right hil] at hikl
no goals
case neg
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : i - l < k
hil : l ≤ i
⊢ choose (i - l) k * choose i l = 0
rw [choose_eq_zero_of_lt hikl, zero_mul]
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (l + k) = i - l - k
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (k + l) = i - l - k
rw [add_comm]
no goals
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ i - (l + k) = i - l - k
apply tsub_add_eq_tsub_tsub
no goals
R : Type u_1
inst✝ : Semiring R
k✝ : ℕ
f : R[X]
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ∀ (n : ℕ), ↑n ! ≠ 0
exact_mod_cast factorial_ne_zero