Canonical Momentum eq gradient kinetic Term

lemma canonicalMomentum_eq_gradient_kineticTerm {d}    {𝓕 : FreeSpace} (A : ElectromagneticPotential d)    (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) :    A.canonicalMomentum 𝓕 J = fun x =>    gradient (fun (v : Lorentz.Vector d) =>    kineticTerm 𝓕 ⟨fun x => A x + x (Sum.inl 0) • v⟩ x) 0:= by  funext x  apply ext_inner_right (𝕜 := ℝ)  intro v  rw [gradient, canonicalMomentum]  simp only [Fin.isValue, toDual_symm_apply]  rw [inner_sub_left, inner_smul_left]  simp [gradient]  conv_lhs =>    enter [2]    simp [lagrangian_add_const]  have hx : DifferentiableAt ℝ (fun v => kineticTerm 𝓕 ⟨fun x => A x + x (Sum.inl 0) • v⟩ x) 0 := by    simp only [kineticTerm_add_time_mul_const _ (hA.differentiable (by simp))]    fun_prop  conv_lhs =>    enter [1]    simp only [lagrangian, Fin.isValue, map_add, map_smul,      LinearMap.smul_apply, smul_eq_mul]    rw [fderiv_fun_sub hx (by simp [freeCurrentPotential]; fun_prop)]    simp only [Fin.isValue, freeCurrentPotential, map_add, map_smul, _root_.add_apply,      FunLike.coe_smul, Pi.smul_apply, smul_eq_mul, fderiv_const_add,      FunLike.coe_sub, Pi.sub_apply]    rw [fderiv_const_mul (by fun_prop)]  simp only [Fin.isValue, FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]  rw [fderiv_fun_sub (by fun_prop) (by fun_prop)]  simp