∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸} {x : 𝕜},
  DifferentiableAt 𝕜 f x → ∀ (n : ℕ), deriv (fun x => f x ^ n) x = ↑n * f x ^ (n - 1) * deriv f x