refactor(Electromagnetism): replace fieldStrengthMatrix with index-evaluation components

Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml

@@ -48,11 +48,11 @@ Requirements:
 
   - description: "Gauge invariance of the field strength under abelian U(1) gauge transformations"
     done: true
-    location: Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean (toFieldStrength_gaugeTransform, fieldStrengthMatrix_gaugeTransform)
+    location: Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean (toFieldStrength_gaugeTransform, toFieldStrength_eval_gaugeTransform)
 
   - description: "Pure-gauge (flat) configurations have vanishing curvature, and the bare gradient does not (necessity of the metric contraction)"
     done: true
-    location: Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean (toFieldStrength_ofGradient, fieldStrengthMatrix_bareGradient_inl_inr, toFieldStrength_bareGradient_ne_zero)
+    location: Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean (toFieldStrength_ofGradient, toFieldStrength_eval_bareGradient_inl_inr, toFieldStrength_bareGradient_ne_zero)
 
   - description: "Group structure of gauge transformations: identity shift and composition of successive shifts"
     done: true

Physlib/Electromagnetism/Dynamics/Hamiltonian.lean

@@ -58,6 +58,8 @@ open TensorProduct
 open minkowskiMatrix
 open InnerProductSpace
 open Lorentz.Vector
+
+attribute [-simp] Fin.succAbove_zero
 attribute [-simp] Fintype.sum_sum_type
 attribute [-simp] Nat.succ_eq_add_one
 
@@ -124,16 +126,17 @@ lemma canonicalMomentum_eq_gradient_kineticTerm {d}
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
 lemma canonicalMomentum_eq {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
     (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) :
     A.canonicalMomentum 𝓕 J = fun x => fun μ =>
-      (1/𝓕.μ₀) * η μ μ • A.fieldStrengthMatrix x (μ, Sum.inl 0) := by
+      (1/𝓕.μ₀) * η μ μ • toField {A.toFieldStrength x | [μ] [Sum.inl 0]}ᵀ := by
   rw [canonicalMomentum_eq_gradient_kineticTerm A hA J]
   funext x
   apply ext_inner_right (𝕜 := ℝ)
   intro v
   simp [gradient]
+  conv_rhs => rw [Lorentz.Vector.inner_eq_sum]
+  simp only [toFieldStrength_eval_apply_eq_single]
   conv_lhs =>
     enter [1, 2, v]
     rw [kineticTerm_add_time_mul_const _ (hA.differentiable (by simp))]
@@ -144,11 +147,8 @@ lemma canonicalMomentum_eq {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential
   rw [← Finset.sum_sub_distrib, Finset.mul_sum]
   congr
   ext μ
-  simp only [Fin.isValue, RCLike.inner_apply, conj_trivial, equivEuclid_apply]
-  rw [fieldStrengthMatrix, toFieldStrength_basis_repr_apply_eq_single]
-  simp only [Fin.isValue, inl_0_inl_0, one_mul]
-  ring_nf
-  simp
+  linear_combination (-(v μ * 𝓕.μ₀⁻¹ * ∂_ μ A x (Sum.inl 0))) *
+    minkowskiMatrix.η_apply_mul_η_apply_diag μ
 
 /-!
 
@@ -165,14 +165,14 @@ lemma canonicalMomentum_eq_electricField {d} {𝓕 : FreeSpace} (A : Electromagn
   rw [canonicalMomentum_eq A hA J]
   funext x μ
   match μ with
-  | Sum.inl 0 => simp
+  | Sum.inl 0 => simp [toFieldStrength_eval_diag_eq_zero]
   | Sum.inr i =>
   simp only [one_div, inr_i_inr_i, Fin.isValue, smul_eq_mul, neg_mul, one_mul, mul_neg, mul_inv_rev,
     neg_inj]
-  rw [electricField_eq_fieldStrengthMatrix (hA := hA.differentiable (by simp))]
+  rw [electricField_eq_toFieldStrength_eval (hA := hA.differentiable (by simp))]
   simp only [Fin.isValue, toTimeAndSpace_symm_apply_time_space, neg_mul, mul_neg]
   field_simp
-  exact fieldStrengthMatrix_antisymm A x (Sum.inr i) (Sum.inl 0)
+  exact toFieldStrength_eval_antisymm A x (Sum.inr i) (Sum.inl 0)
 /-!
 
 ## B. The Hamiltonian

Physlib/Electromagnetism/Dynamics/IsExtrema.lean

@@ -81,16 +81,18 @@ lemma isExtrema_iff_gradLagrangian {𝓕 : FreeSpace} (A : ElectromagneticPotent
 
 /-!
 
-### A.1. Extrema condition in terms of the field strength matrix
+### A.1. Extrema condition in terms of the field strength tensor
 
 -/
 
-lemma isExtrema_iff_fieldStrengthMatrix {𝓕 : FreeSpace}
+lemma isExtrema_iff_toFieldStrength_eval {𝓕 : FreeSpace}
     (A : ElectromagneticPotential d)
     (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ ∞ J) :
     IsExtrema 𝓕 A J ↔
-    ∀ x, ∀ ν, ∑ μ, ∂_ μ (A.fieldStrengthMatrix · (μ, ν)) x = 𝓕.μ₀ * J x ν := by
-  rw [isExtrema_iff_gradLagrangian, gradLagrangian_eq_sum_fieldStrengthMatrix A hA J hJ, funext_iff]
+    ∀ x, ∀ ν, ∑ μ, ∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) x =
+      𝓕.μ₀ * J x ν := by
+  rw [isExtrema_iff_gradLagrangian, gradLagrangian_eq_sum_toFieldStrength_eval A hA J hJ,
+    funext_iff]
   conv_lhs =>
     enter [x, 1, 2, ν]
     rw [smul_smul]

Physlib/Electromagnetism/Dynamics/KineticTerm.lean

@@ -45,7 +45,7 @@ In this implementation we have set `μ₀ = 1`. It is a TODO to introduce this c
 - B. Variational gradient of the kinetic term
   - B.1. Variational gradient in terms of fderiv
   - B.2. Writing the variational gradient as a sums over double derivatives of the potential
-  - B.3. Variational gradient as a sums over fieldStrengthMatrix
+  - B.3. Variational gradient as sums over the components of the field strength tensor
   - B.4. Variational gradient in terms of the Gauss's and Ampère laws
   - B.5. Linearity properties of the variational gradient
   - B.6. HasVarGradientAt for the variational gradient
@@ -73,6 +73,7 @@ open TensorProduct
 open minkowskiMatrix
 attribute [-simp] Fintype.sum_sum_type
 attribute [-simp] Nat.succ_eq_add_one
+attribute [-simp] Fin.succAbove_zero
 
 /-!
 
@@ -116,9 +117,7 @@ lemma kineticTerm_equivariant {d} {𝓕 : FreeSpace} (A : ElectromagneticPotenti
 lemma kineticTerm_eq_sum {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) :
     A.kineticTerm 𝓕 x =
     - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, ∑ μ', ∑ ν', η μ μ' * η ν ν' *
-      (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x) (μ, ν)
-      * (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
-        (A.toFieldStrength x) (μ', ν') := by
+      toField {A.toFieldStrength x | [μ] [ν]}ᵀ * toField {A.toFieldStrength x | [μ'] [ν']}ᵀ := by
   rw [kineticTerm]
   rw [toField_eq_repr]
   rw [contrT_basis_repr_apply_eq_fin]
@@ -144,14 +143,10 @@ lemma kineticTerm_eq_sum {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
     change η (ν') (ν)
   conv_lhs =>
     enter [2, 2, μ, 2, ν, 1, 2, μ', 2, ν', 2]
-    rw [toFieldStrength_tensor_basis_eq_basis]
-    change ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x))
-      (μ', ν')
+    rw [toFieldStrength_tensor_basis_repr_eq_eval]
   conv_lhs =>
     enter [2, 2, μ, 2, ν, 2]
-    rw [toFieldStrength_tensor_basis_eq_basis]
-    change ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x))
-      (μ, ν)
+    rw [toFieldStrength_tensor_basis_repr_eq_eval]
   conv_lhs =>
     enter [2, 2, μ]
     enter [2, ν]
@@ -165,16 +160,10 @@ lemma kineticTerm_eq_sum {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
   conv_lhs => enter [2, 2, μ']; rw [Finset.sum_comm]
   rfl
 
-lemma kineticTerm_eq_sum_fieldStrengthMatrix {d} {𝓕 : FreeSpace}
+lemma kineticTerm_eq_sum_sq {d} {𝓕 : FreeSpace}
     (A : ElectromagneticPotential d) (x : SpaceTime d) : A.kineticTerm 𝓕 x =
-    - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, ∑ μ', ∑ ν', η μ μ' * η ν ν' *
-      A.fieldStrengthMatrix x (μ, ν) * A.fieldStrengthMatrix x (μ', ν') := by
+    - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, η μ μ * η ν ν * ‖toField {A.toFieldStrength x | [μ] [ν]}ᵀ‖ ^ 2 := by
   rw [kineticTerm_eq_sum]
-
-lemma kineticTerm_eq_sum_fieldStrengthMatrix_sq {d} {𝓕 : FreeSpace}
-    (A : ElectromagneticPotential d) (x : SpaceTime d) : A.kineticTerm 𝓕 x =
-    - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, η μ μ * η ν ν * ‖A.fieldStrengthMatrix x (μ, ν)‖ ^ 2 := by
-  rw [kineticTerm_eq_sum_fieldStrengthMatrix]
   congr 1
   refine Finset.sum_congr rfl fun μ _ => Finset.sum_congr rfl fun ν _ => ?_
   rw [Finset.sum_eq_single μ (fun b _ hb => by simp [minkowskiMatrix.off_diag_zero hb.symm])
@@ -198,7 +187,7 @@ lemma kineticTerm_eq_sum_potential {d} {𝓕 : FreeSpace}
           (by simp),
         Finset.sum_eq_single ν (fun b _ hb => by simp [minkowskiMatrix.off_diag_zero hb.symm])
           (by simp),
-        toFieldStrength_basis_repr_apply_eq_single]
+        toFieldStrength_eval_apply_eq_single]
     _ = - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν,
         ((η μ μ * η ν ν * (∂_ μ A x ν) ^ 2 - ∂_ μ A x ν * ∂_ ν A x μ) +
         (η ν ν * η μ μ * (∂_ ν A x μ) ^ 2 - ∂_ ν A x μ * ∂_ μ A x ν)) := by
@@ -232,8 +221,8 @@ lemma kineticTerm_eq_electric_magnetic {𝓕 : FreeSpace} (A : ElectromagneticPo
   simp only [one_div]
   conv_lhs =>
     enter [2, 2, μ, 2, ν, 2, μ', 2, ν']
-    rw [fieldStrengthMatrix_eq_electric_magnetic A t x hA,
-      fieldStrengthMatrix_eq_electric_magnetic A t x hA]
+    rw [toFieldStrength_eval_eq_electric_magnetic A t x hA,
+      toFieldStrength_eval_eq_electric_magnetic A t x hA]
   simp [Fintype.sum_sum_type, Fin.sum_univ_three, EuclideanSpace.norm_sq_eq]
   field_simp
   rw [FreeSpace.c_sq]
@@ -259,31 +248,31 @@ lemma kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space {𝓕 : FreeS
     A.kineticTerm 𝓕 ((toTimeAndSpace 𝓕.c).symm (t, x)) =
     1/2 * (𝓕.ε₀ * ‖A.electricField 𝓕.c t x‖ ^ 2 -
     (1 / (2 * 𝓕.μ₀)) * ∑ i, ∑ j, ‖A.magneticFieldMatrix 𝓕.c t x (i, j)‖ ^ 2) := by
-  rw [kineticTerm_eq_sum_fieldStrengthMatrix_sq]
+  rw [kineticTerm_eq_sum_sq]
   simp [Fintype.sum_sum_type]
   rw [Finset.sum_add_distrib]
   simp only [Fin.isValue, Finset.sum_neg_distrib]
   have h1 : ∑ i, ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) ^ 2
-      = ∑ i, ∑ j, (A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x)))
-        (Sum.inr i, Sum.inr j) ^ 2 := by rfl
+      = ∑ i, ∑ j, toField {A.toFieldStrength ((toTimeAndSpace 𝓕.c).symm (t, x)) |
+        [Sum.inr i] [Sum.inr j]}ᵀ ^ 2 := by rfl
   rw [h1]
   ring_nf
   have h2 : ‖electricField 𝓕.c A t x‖ ^ 2 = 𝓕.c.val ^ 2 *
-      ∑ i, |(A.fieldStrengthMatrix ((toTimeAndSpace 𝓕.c).symm (t, x)))
-      (Sum.inl 0, Sum.inr i)| ^ 2 := by
+      ∑ i, |toField {A.toFieldStrength ((toTimeAndSpace 𝓕.c).symm (t, x)) |
+      [Sum.inl 0] [Sum.inr i]}ᵀ| ^ 2 := by
     rw [EuclideanSpace.norm_sq_eq]
     conv_lhs =>
       enter [2, i]
-      rw [electricField_eq_fieldStrengthMatrix A t x i hA]
+      rw [electricField_eq_toFieldStrength_eval A t x i hA]
       simp only [Fin.isValue, neg_mul, norm_neg, norm_mul, Real.norm_eq_abs, FreeSpace.c_abs]
       rw [mul_pow]
     rw [← Finset.mul_sum]
   rw [h2]
   simp only [Fin.isValue, one_div, sq_abs]
   conv_lhs =>
     enter [1, 2, 1, 2, 2, i]
-    rw [fieldStrengthMatrix_antisymm]
-  simp [FreeSpace.c_sq]
+    rw [toFieldStrength_eval_antisymm]
+  simp [FreeSpace.c_sq, toFieldStrength_eval_diag_eq_zero]
   field_simp
   ring
 
@@ -322,8 +311,9 @@ lemma kineticTerm_add_const {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential
 lemma kineticTerm_contDiff {d} {n : WithTop ℕ∞} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
     (hA : ContDiff ℝ (n + 1) A) :
     ContDiff ℝ n (A.kineticTerm 𝓕) := by
-  rw [funext fun x => kineticTerm_eq_sum_fieldStrengthMatrix (𝓕 := 𝓕) A x]
-  have h (μν) : ContDiff ℝ n (A.fieldStrengthMatrix · μν) := fieldStrengthMatrix_contDiff hA
+  rw [funext fun x => kineticTerm_eq_sum (𝓕 := 𝓕) A x]
+  have h (μ ν) : ContDiff ℝ n (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) :=
+    toFieldStrength_eval_contDiff hA
   fun_prop
 
 /-!
@@ -503,17 +493,17 @@ lemma gradKineticTerm_eq_sum_sum {d} {𝓕 : FreeSpace}
 
 /-!
 
-### B.3. Variational gradient as a sums over fieldStrengthMatrix
+### B.3. Variational gradient as sums over the components of the field strength tensor
 
 We rewrite the variational gradient as a simple double sum over the
-fieldStrengthMatrix.
+components of the field strength tensor.
 
 -/
 
 lemma gradKineticTerm_eq_fieldStrength {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
     (x : SpaceTime d) (ha : ContDiff ℝ ∞ A) :
     A.gradKineticTerm 𝓕 x = ∑ (ν : (Fin 1 ⊕ Fin d)), (1/𝓕.μ₀ * η ν ν) •
-    (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (A.fieldStrengthMatrix · (μ, ν)) x))
+    (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) x))
     • Lorentz.Vector.basis ν := by
   calc _
     _ = ∑ (ν : (Fin 1 ⊕ Fin d)), ∑ (μ : (Fin 1 ⊕ Fin d)),
@@ -529,17 +519,17 @@ lemma gradKineticTerm_eq_fieldStrength {d} {𝓕 : FreeSpace} (A : Electromagnet
         ring_nf
         simp
     _ = ∑ (ν : (Fin 1 ⊕ Fin d)), ∑ (μ : (Fin 1 ⊕ Fin d)),
-      ((1/𝓕.μ₀ * η ν ν) * (∂_ μ (A.fieldStrengthMatrix · (μ, ν)) x)) •
+      ((1/𝓕.μ₀ * η ν ν) * (∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) x)) •
           Lorentz.Vector.basis ν := by
         refine Finset.sum_congr rfl fun ν _ => Finset.sum_congr rfl fun μ _ => ?_
         congr 2
         conv_rhs =>
-          simp only [toFieldStrength_basis_repr_apply_eq_single]
+          simp only [toFieldStrength_eval_apply_eq_single]
           rw [SpaceTime.deriv_eq, fderiv_fun_sub (by fun_prop) (by fun_prop),
             fderiv_const_mul (by fun_prop), fderiv_const_mul (by fun_prop)]
         simp [SpaceTime.deriv_eq]
     _ = ∑ (ν : (Fin 1 ⊕ Fin d)), (1/𝓕.μ₀ * η ν ν) •
-        (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (A.fieldStrengthMatrix · (μ, ν)) x))
+        (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) x))
         • Lorentz.Vector.basis ν := by
         apply Finset.sum_congr rfl (fun ν _ => ?_)
         rw [← Finset.sum_smul, ← Finset.mul_sum, ← smul_smul]
@@ -566,15 +556,15 @@ lemma gradKineticTerm_eq_electric_magnetic {𝓕 : FreeSpace} (A : Electromagnet
   congr 1
   · rw [smul_smul]
     congr 1
-    rw [div_electricField_eq_fieldStrengthMatrix]
+    rw [div_electricField_eq_toFieldStrength_eval]
     simp only [one_div, Fin.isValue, inl_0_inl_0, mul_one, mul_inv_rev,
       toTimeAndSpace_symm_apply_time_space]
     field_simp
     apply ha.of_le (ENat.LEInfty.out)
   · congr
     funext j
     simp only [one_div, inr_i_inr_i, mul_neg, mul_one, neg_smul]
-    rw [curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix, smul_smul, ← neg_smul]
+    rw [curl_magneticFieldMatrix_eq_electricField_toFieldStrength_eval, smul_smul, ← neg_smul]
     congr
     simp only [one_div, toTimeAndSpace_symm_apply_time_space, sub_add_cancel_left, mul_neg]
     apply ha.of_le (ENat.LEInfty.out)
@@ -610,12 +600,11 @@ lemma gradKineticTerm_add {d} {𝓕 : FreeSpace} (A1 A2 : ElectromagneticPotenti
   rw [SpaceTime.deriv_eq, SpaceTime.deriv_eq, SpaceTime.deriv_eq]
   conv_lhs =>
     enter [1, 2, x]
-    rw [fieldStrengthMatrix_add _ _ _ (hA1.differentiable (by simp))
+    rw [toFieldStrength_eval_add _ _ _ (hA1.differentiable (by simp))
       (hA2.differentiable (by simp))]
-    simp [Finsupp.coe_add, Pi.add_apply]
   rw [fderiv_fun_add
-    (fieldStrengthMatrix_differentiable (hA1.of_le ENat.LEInfty.out)).differentiableAt
-    (fieldStrengthMatrix_differentiable (hA2.of_le ENat.LEInfty.out)).differentiableAt]
+    (toFieldStrength_eval_differentiable (hA1.of_le ENat.LEInfty.out)).differentiableAt
+    (toFieldStrength_eval_differentiable (hA2.of_le ENat.LEInfty.out)).differentiableAt]
   rfl
 
 lemma gradKineticTerm_smul {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
@@ -634,13 +623,14 @@ lemma gradKineticTerm_smul {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential
   apply Finset.sum_congr rfl (fun μ _ => ?_)
   conv_rhs =>
     rw [SpaceTime.deriv_eq]
-    change (c • fderiv ℝ (fun x => (A.fieldStrengthMatrix x) (μ, ν)) x) (Lorentz.Vector.basis μ)
+    change (c • fderiv ℝ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) x)
+      (Lorentz.Vector.basis μ)
     rw [← fderiv_const_smul
-      (fieldStrengthMatrix_differentiable <| hA.of_le (ENat.LEInfty.out)).differentiableAt,
+      (toFieldStrength_eval_differentiable <| hA.of_le (ENat.LEInfty.out)).differentiableAt,
       ← SpaceTime.deriv_eq]
   congr
   funext x
-  rw [fieldStrengthMatrix_smul _ _ _ (hA.differentiable (by simp))]
+  rw [toFieldStrength_eval_smul _ _ _ (hA.differentiable (by simp))]
   rfl
 
 /-!
@@ -704,8 +694,7 @@ lemma gradKineticTerm_eq_tensorDeriv {d} {𝓕 : FreeSpace}
     enter [2, 2, 2, μ]
     rw [tensorDeriv_toTensor_basis_repr (by fun_prop)]
     enter [2, x]
-    rw [toFieldStrength_tensor_basis_eq_basis]
-    change fieldStrengthMatrix A x _
+    rw [toFieldStrength_tensor_basis_repr_eq_eval]
   conv_lhs =>
     rw [gradKineticTerm_eq_fieldStrength A x hA]
     simp [Lorentz.Vector.apply_sum]

Physlib/Electromagnetism/Dynamics/Lagrangian.lean

@@ -306,11 +306,11 @@ lemma lagrangian_hasVarGradientAt_gradLagrangian {𝓕 : FreeSpace}
 
 -/
 
-lemma gradLagrangian_eq_sum_fieldStrengthMatrix {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
+lemma gradLagrangian_eq_sum_toFieldStrength_eval {𝓕 : 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
+      (η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) x
+      - J x ν) • Lorentz.Vector.basis ν) := by
   rw [gradLagrangian_eq_kineticTerm_sub A hA J hJ]
   funext x
   simp only [Pi.sub_apply]