Gradient dist norm Power Series zpow

lemma gradient_dist_normPowerSeries_zpow {d : ℕ} {n : ℕ} (m : ℤ) :    ∇ᵈ (distOfFunction (fun x : Space d => (normPowerSeries n x) ^ m) (by fun_prop)) =    distOfFunction (fun x : Space d => (m * (normPowerSeries n x) ^ (m - 2)) • basis.repr x)    (by fun_prop) := by  ext1 η  refine ext_inner_right ℝ fun y => ?_  simp [distGrad_inner_eq]  rw [Distribution.fderivD_apply, distOfFunction_apply, distOfFunction_inner]  calc _    _ = - ∫ (x : Space d), fderiv ℝ η x (basis.repr.symm y) * normPowerSeries n x ^ m := by      rfl    _ = ∫ (x : Space d), η x * fderiv ℝ (normPowerSeries n · ^ m) x (basis.repr.symm y) := by      rw [integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable]      · fun_prop      · refine IsDistBounded.integrable_space_mul ?_ η        simp only [fderiv_normPowerSeries_zpow, mul_assoc]        fun_prop      · fun_prop      · fun_prop      · exact fun _ _ => (differentiable_normPowerSeries_zpow m).differentiableAt    _ = ∫ (x : Space d), η x *        (m * ⟪(basis.repr.symm y), x⟫_ℝ * (normPowerSeries n x) ^ (m - 2)) := by      simp only [fderiv_normPowerSeries_zpow]  congr  funext x  simp [inner_smul_left_eq_smul]  left  rw [real_inner_comm, basis_repr_inner_eq]  ring