Is Extrema iff vector Potential

lemma isExtrema_iff_vectorPotential {𝓕 : FreeSpace}    (A : DistElectromagneticPotential d)    (J : DistLorentzCurrentDensity d) :    IsExtrema 𝓕 A J ↔      (∀ ε, distSpaceDiv (A.electricField 𝓕.c) ε = (1/𝓕.ε₀) * (J.chargeDensity 𝓕.c) ε) ∧      (∀ ε i, 𝓕.μ₀ * 𝓕.ε₀ * distTimeDeriv (A.electricField 𝓕.c) ε i -      (∑ x, -(distSpaceDeriv x (distSpaceDeriv x (A.vectorPotential 𝓕.c)) ε i        - distSpaceDeriv x (distSpaceDeriv i (A.vectorPotential 𝓕.c)) ε x)) +      𝓕.μ₀ * J.currentDensity 𝓕.c ε i = 0) := by  rw [isExtrema_iff_space_time]  refine and_congr (by rfl) ?_  suffices ∀ ε i, ∑ x, -(distSpaceDeriv x (distSpaceDeriv x (A.vectorPotential 𝓕.c)) ε i        - distSpaceDeriv x (distSpaceDeriv i (A.vectorPotential 𝓕.c)) ε x) =        ∑ j, ((PiLp.basisFun 2 ℝ (Fin d)).tensorProduct (PiLp.basisFun 2 ℝ (Fin d))).repr          ((Space.distSpaceDeriv j (A.magneticFieldMatrix 𝓕.c)) ε) (j, i) by    conv_lhs => enter [2, 2]; rw [← this]  intro ε i  congr  funext j  rw [magneticFieldMatrix_distSpaceDeriv_basis_repr_eq_vector_potential]  ring