Free Current Potential has Var Gradient At

lemma freeCurrentPotential_hasVarGradientAt (A : ElectromagneticPotential d)    (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d)    (hJ : ContDiff ℝ ∞ J) :    HasVarGradientAt (fun A => freeCurrentPotential ⟨A⟩ J)    (((∑ μ, fun x => (η μ μ * J x μ) • Lorentz.Vector.basis μ))) A := by  conv =>    enter [1, q', x]    rw [freeCurrentPotential, minkowskiProduct_toCoord_minkowskiMatrix]  apply HasVarGradientAt.sum _ hA  intro μ  have h1 := hasVarAdjDerivAt_component μ A hA  have h2' : ContDiff ℝ ∞ fun x => η μ μ * J x μ :=    ContDiff.mul (by fun_prop) ((Lorentz.Vector.contDiff_apply _).mpr hJ μ)  have h2 := HasVarAdjDerivAt.fun_mul h2' _ _ A h1  have h3' : (fun (φ : SpaceTime d → Lorentz.Vector d) x => η μ μ * J x μ * φ x μ) =    (fun (φ : SpaceTime d → Lorentz.Vector d) x => η μ μ * φ x μ * J x μ) := by    funext φ x    ring  rw [h3'] at h2  apply HasVarGradientAt.intro _ h2  simp