R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (sum f fun n r => ↑(monomial (n - k)) (choose n k • r)) = sum f fun i r => ↑(monomial (i - k)) (↑(choose i k) * r)
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ ↑(hasseDeriv k) f = sum f fun i r => ↑(monomial (i - k)) (↑(choose i k) * r)
dsimp [hasseDeriv]
case e_f
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (fun n r => ↑(monomial (n - k)) (choose n k • r)) = fun i r => ↑(monomial (i - k)) (↑(choose i k) * r)
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (sum f fun n r => ↑(monomial (n - k)) (choose n k • r)) = sum f fun i r => ↑(monomial (i - k)) (↑(choose i k) * r)
congr
case e_f.h.h.a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
x✝¹ : ℕ
x✝ : R
n✝ : ℕ
⊢ coeff (↑(monomial (x✝¹ - k)) (choose x✝¹ k • x✝)) n✝ = coeff (↑(monomial (x✝¹ - k)) (↑(choose x✝¹ k) * x✝)) n✝
case e_f
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (fun n r => ↑(monomial (n - k)) (choose n k • r)) = fun i r => ↑(monomial (i - k)) (↑(choose i k) * r)
ext
case e_f.h.h.a.e_a.h.e_6.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
x✝¹ : ℕ
x✝ : R
n✝ : ℕ
⊢ choose x✝¹ k • x✝ = ↑(choose x✝¹ k) * x✝
case e_f.h.h.a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
x✝¹ : ℕ
x✝ : R
n✝ : ℕ
⊢ coeff (↑(monomial (x✝¹ - k)) (choose x✝¹ k • x✝)) n✝ = coeff (↑(monomial (x✝¹ - k)) (↑(choose x✝¹ k) * x✝)) n✝
congr
no goals
case e_f.h.h.a.e_a.h.e_6.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
x✝¹ : ℕ
x✝ : R
n✝ : ℕ
⊢ choose x✝¹ k • x✝ = ↑(choose x✝¹ k) * x✝
apply nsmul_eq_mul