case zero
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
m✝ m : ℤ
⊢ ((deriv^[Nat.zero]) fun x => x ^ m) = fun x => (∏ i in Finset.range Nat.zero, (↑m - ↑i)) * x ^ (m - ↑Nat.zero)

case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
m✝ m : ℤ
k : ℕ
ihk : ((deriv^[k]) fun x => x ^ m) = fun x => (∏ i in Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
⊢ ((deriv^[Nat.succ k]) fun x => x ^ m) = fun x =>
    (∏ i in Finset.range (Nat.succ k), (↑m - ↑i)) * x ^ (m - ↑(Nat.succ k))
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
m✝ m : ℤ
k : ℕ
⊢ ((deriv^[k]) fun x => x ^ m) = fun x => (∏ i in Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
induction' k with k ihk
no goals
case zero
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
m✝ m : ℤ
⊢ ((deriv^[Nat.zero]) fun x => x ^ m) = fun x => (∏ i in Finset.range Nat.zero, (↑m - ↑i)) * x ^ (m - ↑Nat.zero)
simp only [Nat.zero_eq, one_mul, Int.ofNat_zero, id, sub_zero, Finset.prod_range_zero,
  Function.iterate_zero]
no goals
case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
m✝ m : ℤ
k : ℕ
ihk : ((deriv^[k]) fun x => x ^ m) = fun x => (∏ i in Finset.range k, (↑m - ↑i)) * x ^ (m - ↑k)
⊢ ((deriv^[Nat.succ k]) fun x => x ^ m) = fun x =>
    (∏ i in Finset.range (Nat.succ k), (↑m - ↑i)) * x ^ (m - ↑(Nat.succ k))
simp only [Function.iterate_succ_apply', ihk, deriv_const_mul_field', deriv_zpow',
  Finset.prod_range_succ, Int.ofNat_succ, ← sub_sub, Int.cast_sub, Int.cast_ofNat, mul_assoc]