Deriv eq mfderiv manifold Structure

lemma deriv_eq_mfderiv_manifoldStructure {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]    (μ : Fin d) (f : Space d → M) (x : Space d) :    deriv μ f x = mfderiv (𝓡 d) 𝓘(ℝ, M) f x (EuclideanSpace.single μ 1) := by  by_cases hf : DifferentiableAt ℝ f x  · rw [deriv_eq_mfderiv]    change _ = mfderiv (𝓡 d) 𝓘(ℝ, M)      (f ∘ modelDiffeo) x (EuclideanSpace.single μ 1)    rw [mfderiv_comp (I' := 𝓘(ℝ, Space d)) _ hf.mdifferentiableAt      (modelDiffeo.mdifferentiable WithTop.top_ne_zero).mdifferentiableAt]    simp only [Function.comp_apply, modelDiffeo_apply, mfderiv_eq_fderiv,      ContinuousLinearMap.coe_comp]    rw [basis_eq_mfderiv_modelDiffeo_single]    rfl  · rw [deriv_eq, fderiv_zero_of_not_differentiableAt hf,      mfderiv_zero_of_not_mdifferentiableAt <|      mdifferentiable_manifoldStructure_iff_differentiable.mp.mt hf]    simp