𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
⊢ (∏ x in Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
⊢ (deriv^[k]) (fun x => x ^ n) x = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ (n - k)
simp only [← zpow_ofNat, iter_deriv_zpow, Int.cast_ofNat]
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
hkn : k ≤ n
⊢ (∏ x in Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)

case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
hnk : n < k
⊢ (∏ x in Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
⊢ (∏ x in Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
cases' le_or_lt k n with hkn hnk
no goals
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
hkn : k ≤ n
⊢ (∏ x in Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
rw [Int.ofNat_sub hkn]
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
hnk : n < k
this : ∏ i in Finset.range k, (↑n - ↑i) = 0
⊢ (∏ x in Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
hnk : n < k
⊢ (∏ x in Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
have : (∏ i in Finset.range k, (n - i : 𝕜)) = 0 :=
  Finset.prod_eq_zero (Finset.mem_range.2 hnk) (sub_self _)
no goals
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x✝ : 𝕜
s : Set 𝕜
m : ℤ
n : ℕ
x : 𝕜
k : ℕ
hnk : n < k
this : ∏ i in Finset.range k, (↑n - ↑i) = 0
⊢ (∏ x in Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ i in Finset.range k, (↑n - ↑i)) * x ^ ↑(n - k)
simp only [this, MulZeroClass.zero_mul]