Grad Lagrangian eq sum field Strength Matrix

lemma gradLagrangian_eq_sum_fieldStrengthMatrix {𝓕 : FreeSpace} (A : ElectromagneticPotential d)    (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ ∞ J) :    A.gradLagrangian 𝓕 J = fun x => ∑ ν,      (η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x - J x ν)      • Lorentz.Vector.basis ν) := by  rw [gradLagrangian_eq_kineticTerm_sub A hA J hJ]  funext x  simp only [Pi.sub_apply]  rw [gradKineticTerm_eq_fieldStrength, gradFreeCurrentPotential_eq_sum_basis A hA J hJ]  simp only [one_div, Finset.sum_apply]  rw [← Finset.sum_sub_distrib]  refine Finset.sum_congr rfl (fun ν _ => ?_)  module  exact hA