diff --git a/Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml b/Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml
index d883f96788..9531440d98 100644
--- a/Physlib/ClassicalFieldTheory/GaugeTheory/API-map.yaml
+++ b/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
diff --git a/Physlib/Electromagnetism/Dynamics/Hamiltonian.lean b/Physlib/Electromagnetism/Dynamics/Hamiltonian.lean
index f3e69f1341..c42066c1fd 100644
--- a/Physlib/Electromagnetism/Dynamics/Hamiltonian.lean
+++ b/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
diff --git a/Physlib/Electromagnetism/Dynamics/IsExtrema.lean b/Physlib/Electromagnetism/Dynamics/IsExtrema.lean
index 338dc5f86f..1c82e88e39 100644
--- a/Physlib/Electromagnetism/Dynamics/IsExtrema.lean
+++ b/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]
diff --git a/Physlib/Electromagnetism/Dynamics/KineticTerm.lean b/Physlib/Electromagnetism/Dynamics/KineticTerm.lean
index 681d176df9..e63735af98 100644
--- a/Physlib/Electromagnetism/Dynamics/KineticTerm.lean
+++ b/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,22 +248,22 @@ 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]
@@ -282,8 +271,8 @@ lemma kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space {𝓕 : FreeS
   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,7 +556,7 @@ 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
@@ -574,7 +564,7 @@ lemma gradKineticTerm_eq_electric_magnetic {𝓕 : FreeSpace} (A : Electromagnet
   · 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]
diff --git a/Physlib/Electromagnetism/Dynamics/Lagrangian.lean b/Physlib/Electromagnetism/Dynamics/Lagrangian.lean
index eefd5262db..260c4e6096 100644
--- a/Physlib/Electromagnetism/Dynamics/Lagrangian.lean
+++ b/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]
diff --git a/Physlib/Electromagnetism/Kinematics/Boosts.lean b/Physlib/Electromagnetism/Kinematics/Boosts.lean
index 829b52aabc..6121138265 100644
--- a/Physlib/Electromagnetism/Kinematics/Boosts.lean
+++ b/Physlib/Electromagnetism/Kinematics/Boosts.lean
@@ -49,6 +49,9 @@ namespace Electromagnetism
 
 namespace ElectromagneticPotential
 open LorentzGroup
+open TensorSpecies Tensor
+
+attribute [-simp] Fin.succAbove_zero
 
 /-!
 
@@ -71,17 +74,17 @@ lemma electricField_apply_x_boost_zero {d : ℕ} {c : SpeedOfLight} (β : ℝ) (
     electricField c (Λ • A) t x 0 =
     A.electricField c t' x' 0 := by
   dsimp
-  rw [electricField_eq_fieldStrengthMatrix, fieldStrengthMatrix_equivariant _ _ hA]
-  simp [Fintype.sum_sum_type, Fin.sum_univ_succ]
-  rw [electricField_eq_fieldStrengthMatrix (hA := hA)]
+  rw [electricField_eq_toFieldStrength_eval, toFieldStrength_eval_equivariant _ _ hA]
+  simp [Fintype.sum_sum_type, Fin.sum_univ_succ, toFieldStrength_eval_diag_eq_zero]
+  rw [electricField_eq_toFieldStrength_eval (hA := hA)]
   simp only [Fin.isValue, neg_mul, neg_inj, mul_eq_mul_left_iff, SpeedOfLight.val_ne_zero, or_false]
   conv_lhs =>
     enter [2]
-    rw [fieldStrengthMatrix_antisymm]
+    rw [toFieldStrength_eval_antisymm]
   trans γ β ^ 2 * (1 - β ^ 2) *
-      (A.fieldStrengthMatrix
-      ((boost (d := d.succ) 0 β hβ)⁻¹ • (SpaceTime.toTimeAndSpace c).symm (t, x)))
-      (Sum.inl 0, Sum.inr 0)
+      toField {A.toFieldStrength
+      ((boost (d := d.succ) 0 β hβ)⁻¹ • (SpaceTime.toTimeAndSpace c).symm (t, x)) |
+      [Sum.inl 0] [Sum.inr 0]}ᵀ
   · ring
   rw [γ_sq β hβ]
   field_simp
@@ -107,11 +110,11 @@ lemma electricField_apply_x_boost_succ {d : ℕ} {c : SpeedOfLight} (β : ℝ) (
     electricField c (Λ • A) t x i.succ =
     γ β * (A.electricField c t' x' i.succ + c * β * A.magneticFieldMatrix c t' x' (0, i.succ)) := by
   dsimp
-  rw [electricField_eq_fieldStrengthMatrix,
-    fieldStrengthMatrix_equivariant _ _ hA]
+  rw [electricField_eq_toFieldStrength_eval,
+    toFieldStrength_eval_equivariant _ _ hA]
   simp [Fintype.sum_sum_type, boost_zero_inr_succ_inr_succ, Fin.sum_univ_succ]
-  rw [fieldStrengthMatrix_inl_inr_eq_electricField (c := c) (hA := hA),
-    fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix (c := c),
+  rw [toFieldStrength_eval_inl_inr_eq_electricField (c := c) (hA := hA),
+    toFieldStrength_eval_inr_inr_eq_magneticFieldMatrix (c := c),
     SpaceTime.boost_zero_apply_time_space]
   simp only [one_div, Nat.succ_eq_add_one, SpaceTime.time_toTimeAndSpace_symm,
     SpaceTime.space_toTimeAndSpace_symm, neg_mul, mul_neg]
@@ -143,10 +146,10 @@ lemma magneticFieldMatrix_apply_x_boost_zero_succ {d : ℕ} {c : SpeedOfLight} (
     magneticFieldMatrix c (Λ • A) t x (0, i.succ) =
     γ β * (A.magneticFieldMatrix c t' x' (0, i.succ) + β / c * A.electricField c t' x' i.succ) := by
   dsimp [magneticFieldMatrix_eq]
-  rw [fieldStrengthMatrix_equivariant _ _ hA]
+  rw [toFieldStrength_eval_equivariant _ _ hA]
   simp [Fintype.sum_sum_type, boost_zero_inr_succ_inr_succ, Fin.sum_univ_succ]
-  rw [fieldStrengthMatrix_inl_inr_eq_electricField (c := c) (hA := hA),
-    fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix (c := c),
+  rw [toFieldStrength_eval_inl_inr_eq_electricField (c := c) (hA := hA),
+    toFieldStrength_eval_inr_inr_eq_magneticFieldMatrix (c := c),
     SpaceTime.boost_zero_apply_time_space]
   simp only [one_div, Nat.succ_eq_add_one, SpaceTime.time_toTimeAndSpace_symm,
     SpaceTime.space_toTimeAndSpace_symm, neg_mul, mul_neg, neg_neg]
@@ -171,7 +174,7 @@ lemma magneticFieldMatrix_apply_x_boost_succ_succ {d : ℕ} {c : SpeedOfLight} (
     magneticFieldMatrix c (Λ • A) t x (i.succ, j.succ) =
     A.magneticFieldMatrix c t' x' (i.succ, j.succ) := by
   dsimp [magneticFieldMatrix_eq]
-  rw [fieldStrengthMatrix_equivariant _ _ hA]
+  rw [toFieldStrength_eval_equivariant _ _ hA]
   simp [Fintype.sum_sum_type, boost_zero_inr_succ_inr_succ, Fin.sum_univ_succ]
   rw [SpaceTime.boost_zero_apply_time_space]
   rfl
diff --git a/Physlib/Electromagnetism/Kinematics/ElectricField.lean b/Physlib/Electromagnetism/Kinematics/ElectricField.lean
index fb3696ae45..31fde14938 100644
--- a/Physlib/Electromagnetism/Kinematics/ElectricField.lean
+++ b/Physlib/Electromagnetism/Kinematics/ElectricField.lean
@@ -22,8 +22,8 @@ In this module we define the electric field, and prove lemmas about it.
 ## ii. Key results
 
 - `electricField` : The electric field from the electromagnetic potential.
-- `electricField_eq_fieldStrengthMatrix` : The electric field expressed in terms of the
-  field strength tensor.
+- `electricField_eq_toFieldStrength_eval` : The electric field expressed in terms of the
+  components of the field strength tensor.
 
 ## iii. Table of contents
 
@@ -145,12 +145,12 @@ The electric field can be expressed in terms of the field strength tensor as
 `E_i = - c * F_0^i`.
 -/
 
-lemma electricField_eq_fieldStrengthMatrix {c : SpeedOfLight}
+lemma electricField_eq_toFieldStrength_eval {c : SpeedOfLight}
     (A : ElectromagneticPotential d) (t : Time)
     (x : Space d) (i : Fin d) (hA : Differentiable ℝ A) :
-    A.electricField c t x i = -
-    c * A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x)) (Sum.inl 0, Sum.inr i) := by
-  rw [toFieldStrength_basis_repr_apply_eq_single]
+    A.electricField c t x i = - c *
+    toField {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [Sum.inl 0] [Sum.inr i]}ᵀ := by
+  rw [toFieldStrength_eval_apply_eq_single]
   simp only [Fin.isValue, inl_0_inl_0, one_mul, inr_i_inr_i, neg_mul, sub_neg_eq_add]
   rw [electricField]
   simp only [PiLp.sub_apply, PiLp.neg_apply, Fin.isValue, mul_add, neg_add_rev]
@@ -185,21 +185,21 @@ lemma electricField_eq_fieldStrengthMatrix {c : SpeedOfLight}
     · exact hA
   · exact 1
 
-lemma fieldStrengthMatrix_inl_inr_eq_electricField {c : SpeedOfLight}
+lemma toFieldStrength_eval_inl_inr_eq_electricField {c : SpeedOfLight}
     (A : ElectromagneticPotential d)
     (x : SpaceTime d) (i : Fin d) (hA : Differentiable ℝ A) :
-    A.fieldStrengthMatrix x (Sum.inl 0, Sum.inr i) =
+    toField {A.toFieldStrength x | [Sum.inl 0] [Sum.inr i]}ᵀ =
     - (1 /c) * A.electricField c (x.time c) x.space i := by
-  rw [electricField_eq_fieldStrengthMatrix A (x.time c) x.space i hA]
+  rw [electricField_eq_toFieldStrength_eval A (x.time c) x.space i hA]
   simp
 
-lemma fieldStrengthMatrix_inr_inl_eq_electricField {c : SpeedOfLight}
+lemma toFieldStrength_eval_inr_inl_eq_electricField {c : SpeedOfLight}
     (A : ElectromagneticPotential d)
     (x : SpaceTime d) (i : Fin d) (hA : Differentiable ℝ A) :
-    A.fieldStrengthMatrix x (Sum.inr i, Sum.inl 0) =
+    toField {A.toFieldStrength x | [Sum.inr i] [Sum.inl 0]}ᵀ =
     (1 /c) * A.electricField c (x.time c) x.space i := by
-  rw [fieldStrengthMatrix_antisymm A x (Sum.inr i) (Sum.inl 0),
-    fieldStrengthMatrix_inl_inr_eq_electricField A x i hA]
+  rw [toFieldStrength_eval_antisymm A x (Sum.inr i) (Sum.inl 0),
+    toFieldStrength_eval_inl_inr_eq_electricField A x i hA]
   ring
 /-!
 
@@ -214,10 +214,10 @@ lemma electricField_contDiff {n} {c : SpeedOfLight} {A : ElectromagneticPotentia
   conv =>
     enter [3, x];
     change A.electricField c x.1 x.2 i
-    rw [electricField_eq_fieldStrengthMatrix (A) x.1 x.2 i (hA.differentiable (by simp))]
+    rw [electricField_eq_toFieldStrength_eval (A) x.1 x.2 i (hA.differentiable (by simp))]
   apply ContDiff.mul
   · fun_prop
-  exact (fieldStrengthMatrix_contDiff hA).comp
+  exact (toFieldStrength_eval_contDiff hA).comp
     (ContinuousLinearEquiv.contDiff (toTimeAndSpace c).symm)
 
 lemma electricField_apply_contDiff {n} {c : SpeedOfLight} {A : ElectromagneticPotential d}
@@ -304,46 +304,47 @@ lemma time_deriv_comp_vectorPotential_eq_electricField {d} {A : ElectromagneticP
 
 open Space
 
-lemma time_deriv_electricField_eq_fieldStrengthMatrix {d} {A : ElectromagneticPotential d}
+lemma time_deriv_electricField_eq_toFieldStrength_eval {d} {A : ElectromagneticPotential d}
     {c : SpeedOfLight} (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i : Fin d) :
     ∂ₜ (fun t => A.electricField c t x) t i =
-    - c ^ 2 * ∂_ (Sum.inl 0) (fun x => (A.fieldStrengthMatrix x) (Sum.inl 0, Sum.inr i))
+    - c ^ 2 * ∂_ (Sum.inl 0) (fun x => toField {A.toFieldStrength x | [Sum.inl 0] [Sum.inr i]}ᵀ)
     ((toTimeAndSpace c).symm (t, x)) := by
   rw [SpaceTime.deriv_sum_inl c]
   simp only [one_div, ContinuousLinearEquiv.apply_symm_apply, Fin.isValue, smul_eq_mul, neg_mul]
   rw [← Time.deriv_euclid]
   conv_lhs =>
     enter [1, t]
-    rw [electricField_eq_fieldStrengthMatrix (c := c) A t x i (hA.differentiable (by simp))]
+    rw [electricField_eq_toFieldStrength_eval (c := c) A t x i (hA.differentiable (by simp))]
   rw [Time.deriv_eq, fderiv_const_mul]
   simp [← Time.deriv_eq]
   field_simp
-  · exact (fieldStrengthMatrix_differentiable_time hA x).differentiableAt
+  · exact (toFieldStrength_eval_differentiable_time hA x).differentiableAt
   · apply electricField_differentiable_time hA x
-  · apply fieldStrengthMatrix_differentiable hA
+  · apply toFieldStrength_eval_differentiable hA
 
-lemma div_electricField_eq_fieldStrengthMatrix{d} {A : ElectromagneticPotential d}
+lemma div_electricField_eq_toFieldStrength_eval {d} {A : ElectromagneticPotential d}
     {c : SpeedOfLight} (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) :
     (∇ ⬝ A.electricField c t) x = c * ∑ (μ : (Fin 1 ⊕ Fin d)),
-      (∂_ μ (A.fieldStrengthMatrix · (μ, Sum.inl 0)) ((toTimeAndSpace c).symm (t, x))) := by
+      (∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [Sum.inl 0]}ᵀ)
+        ((toTimeAndSpace c).symm (t, x))) := by
   rw [Finset.mul_sum]
   simp only [Fin.isValue, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
-    Finset.sum_singleton, fieldStrengthMatrix_diag_eq_zero, SpaceTime.deriv_zero, Pi.ofNat_apply,
+    Finset.sum_singleton, toFieldStrength_eval_diag_eq_zero, SpaceTime.deriv_zero, Pi.ofNat_apply,
     mul_zero, zero_add]
   conv_rhs =>
     enter [2, i]
-    rw [SpaceTime.deriv_sum_inr c _ (fieldStrengthMatrix_differentiable hA)]
+    rw [SpaceTime.deriv_sum_inr c _ (toFieldStrength_eval_differentiable hA)]
   rw [Space.div]
   congr
   funext i
   simp only [ContinuousLinearEquiv.apply_symm_apply, Fin.isValue]
   conv_lhs =>
     enter [2, y]
-    rw [electricField_eq_fieldStrengthMatrix (c := c) A t y i (hA.differentiable (by simp))]
-    rw [fieldStrengthMatrix_antisymm]
+    rw [electricField_eq_toFieldStrength_eval (c := c) A t y i (hA.differentiable (by simp))]
+    rw [toFieldStrength_eval_antisymm]
   rw [Space.deriv_eq_fderiv_basis, fderiv_const_mul]
   simp [← Space.deriv_eq_fderiv_basis]
-  exact (fieldStrengthMatrix_differentiable_space hA t).neg.differentiableAt
+  exact (toFieldStrength_eval_differentiable_space hA t).neg.differentiableAt
 end ElectromagneticPotential
 
 end Electromagnetism
diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
index 649bae9da2..a1dbba4a42 100644
--- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
+++ b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
@@ -16,13 +16,14 @@ public import Mathlib.Algebra.Order.Archimedean.Real.Hom
 
 In this module we define the field strength tensor in terms of the electromagnetic potential.
 
-We define a tensor version and a matrix version and prover various properties of these.
+We define the tensor and prove various properties of it. Its components are accessed
+through index evaluation, `toField {A.toFieldStrength x | [μ] [ν]}ᵀ`.
 
 ## ii. Key results
 
 - `toFieldStrength` : The field strength tensor from an electromagnetic potential.
-- `fieldStrengthMatrix` : The field strength matrix from an electromagnetic potential
-  (matrix representation of the field strength tensor in the standard basis).
+- `toFieldStrength_eval_apply_eq_single` : The components of the field strength tensor
+  in terms of derivatives of the potential, `F^{μν} = η^{μμ} ∂_μ A^ν - η^{νν} ∂_ν A^μ`.
 
 ## iii. Table of contents
 
@@ -31,13 +32,13 @@ We define a tensor version and a matrix version and prover various properties of
   - A.2. Vector equalities
   - A.3. The group action acting on the field strength tensor
   - A.4. Differentiability and smoothness of the field strength tensor
-  - A.5. Elements of the field strength tensor in terms of basis
-    - A.5.1. Index evaluation
-  - A.6. The field strength matrix
-    - A.6.1. Differentiability of the field strength matrix
-  - A.7. The antisymmetry of the field strength tensor
-  - A.8. Equivariance of the field strength matrix
-  - A.9. Linearity of the field strength tensor
+  - A.5. Components of the field strength tensor
+    - A.5.1. Components in terms of the tensor basis
+    - A.5.2. Index evaluation
+    - A.5.3. Differentiability of the components
+  - A.6. The antisymmetry of the field strength tensor
+  - A.7. Equivariance of the components of the field strength tensor
+  - A.8. Linearity of the field strength tensor
 
 ## iv. References
 
@@ -61,13 +62,6 @@ open Lorentz
 attribute [-simp] Fintype.sum_sum_type
 attribute [-simp] Nat.succ_eq_add_one
 
-TODO "Currently the API for the field strength tensor has the definition
-  of `fieldStrengthMatrix`. This is now unneeded, and should be replaced with
-  `toField {A.toFieldStrength x| [μ] [ν]}ᵀ` and suitble API around that.
-  To undertake this TODO, it is likely easier to start building the API
-  around `toField {A.toFieldStrength x| [μ] [ν]}ᵀ` and then remove `fieldStrengthMatrix`
-  once the API is in place."
-
 /-!
 
 ## A. The field strength tensor
@@ -261,7 +255,16 @@ lemma contDiff_toFieldStrength {d} {n : WithTop ℕ∞} {A : ElectromagneticPote
 
 /-!
 
-### A.5. Elements of the field strength tensor in terms of basis
+### A.5. Components of the field strength tensor
+
+The components `F^{μν}` of the field strength tensor are accessed through index evaluation,
+`toField {A.toFieldStrength x | [μ] [ν]}ᵀ`. This is the canonical way to refer to the
+components of the field strength tensor, and is what should be used downstream.
+
+The lemmas in terms of the tensor basis are used to prove the index evaluation lemmas,
+and are not expected to be used directly.
+
+#### A.5.1. Components in terms of the tensor basis
 
 -/
 
@@ -318,31 +321,9 @@ lemma toFieldStrength_tensor_basis_eq_basis {d} (A : ElectromagneticPotential d)
   rw [hb, Module.Basis.repr_reindex_apply]
   congr 1
 
-lemma toFieldStrength_basis_repr_apply {d} {μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)}
-    (A : ElectromagneticPotential d) (x : SpaceTime d) :
-    (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x) μν =
-    ∑ κ, ((η μν.1 κ * ∂_ κ A x μν.2) - η μν.2 κ * ∂_ κ A x μν.1) := by
-  match μν with
-  | (μ, ν) =>
-  trans (Tensor.basis _).repr (Tensorial.toTensor (toFieldStrength A x))
-    (fun | 0 => μ | 1 => ν); swap
-  · rw [toTensor_toFieldStrength_basis_repr]
-  rw [toFieldStrength_tensor_basis_eq_basis]
-  rfl
-
-lemma toFieldStrength_basis_repr_apply_eq_single {d} {μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)}
-    (A : ElectromagneticPotential d) (x : SpaceTime d) :
-    (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x) μν =
-    ((η μν.1 μν.1 * ∂_ μν.1 A x μν.2) - η μν.2 μν.2 * ∂_ μν.2 A x μν.1) := by
-  rw [toFieldStrength_basis_repr_apply, Finset.sum_sub_distrib,
-    Finset.sum_eq_single μν.1
-      (fun b _ hb => by simp [minkowskiMatrix.off_diag_zero hb.symm]) (by simp),
-    Finset.sum_eq_single μν.2
-      (fun b _ hb => by simp [minkowskiMatrix.off_diag_zero hb.symm]) (by simp)]
-
 /-!
 
-#### A.5.1. Index evaluation
+#### A.5.2. Index evaluation
 
 These lemmas express the components of the field strength tensor using index evaluation.
 
@@ -364,14 +345,34 @@ lemma toFieldStrength_eval_eq_basis_repr {d} (A : ElectromagneticPotential d)
     simp [Basis.tensorProduct_repr_tmul_apply, Finsupp.single_apply]
   · rfl
 
+/-- Evaluating both tensor indices of the field strength gives the coefficient in the
+tensor basis. -/
+lemma toFieldStrength_eval_eq_tensor_basis_repr {d} (A : ElectromagneticPotential d)
+    (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) :
+    toField {A.toFieldStrength x | [μ] [ν]}ᵀ =
+    (Tensor.basis _).repr (Tensorial.toTensor (toFieldStrength A x)) (fun | 0 => μ | 1 => ν) := by
+  rw [toFieldStrength_eval_eq_basis_repr, toFieldStrength_tensor_basis_eq_basis]
+  rfl
+
+/-- The coefficient of the field strength tensor in the tensor basis is given by
+index evaluation. -/
+lemma toFieldStrength_tensor_basis_repr_eq_eval {d} (A : ElectromagneticPotential d)
+    (x : SpaceTime d)
+    (b : ComponentIdx (S := realLorentzTensor d) (Fin.append ![Color.up] ![Color.up])) :
+    (Tensor.basis _).repr (Tensorial.toTensor (toFieldStrength A x)) b =
+    toField {A.toFieldStrength x | [b 0] [b 1]}ᵀ := by
+  rw [toFieldStrength_eval_eq_tensor_basis_repr]
+  congr 1
+  funext i
+  fin_cases i <;> rfl
+
 /-- The evaluated components of the field strength tensor in terms of derivatives of the
 electromagnetic potential. -/
 lemma toFieldStrength_eval_apply {d} (A : ElectromagneticPotential d)
     (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) :
     toField {A.toFieldStrength x | [μ] [ν]}ᵀ =
     ∑ κ, (η μ κ * ∂_ κ A x ν - η ν κ * ∂_ κ A x μ) := by
-  rw [toFieldStrength_eval_eq_basis_repr]
-  exact toFieldStrength_basis_repr_apply (μν := (μ, ν)) A x
+  rw [toFieldStrength_eval_eq_tensor_basis_repr, toTensor_toFieldStrength_basis_repr]
 
 /-- The evaluated components of the field strength tensor after using diagonal form of the
 Minkowski metric. -/
@@ -379,116 +380,63 @@ lemma toFieldStrength_eval_apply_eq_single {d} (A : ElectromagneticPotential d)
     (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) :
     toField {A.toFieldStrength x | [μ] [ν]}ᵀ =
     η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ := by
-  rw [toFieldStrength_eval_eq_basis_repr]
-  exact toFieldStrength_basis_repr_apply_eq_single (μν := (μ, ν)) A x
+  rw [toFieldStrength_eval_apply, Finset.sum_sub_distrib,
+    Finset.sum_eq_single μ
+      (fun b _ hb => by simp [minkowskiMatrix.off_diag_zero hb.symm]) (by simp),
+    Finset.sum_eq_single ν
+      (fun b _ hb => by simp [minkowskiMatrix.off_diag_zero hb.symm]) (by simp)]
 
 /-!
 
-### A.6. The field strength matrix
-
-We define the field strength matrix to be the matrix representation of the field strength tensor
-in the standard basis.
+#### A.5.3. Differentiability of the components
 
-This is currently not used as much as it could be.
 -/
 open ContDiff
 
-/-- The matrix corresponding to the field strength in the standard basis. -/
-noncomputable abbrev fieldStrengthMatrix {d} (A : ElectromagneticPotential d) (x : SpaceTime d) :=
-    (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)
-
-lemma fieldStrengthMatrix_eq {d} (A : ElectromagneticPotential d) (x : SpaceTime d) :
-    A.fieldStrengthMatrix x =
-    (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x) := by rfl
-
-/-- Index evaluation of the field strength tensor agrees with the corresponding component of
-the field strength matrix. -/
-lemma toFieldStrength_eval_eq_fieldStrengthMatrix {d} (A : ElectromagneticPotential d)
-    (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) :
-    toField {A.toFieldStrength x | [μ] [ν]}ᵀ = A.fieldStrengthMatrix x (μ, ν) := by
-  rw [toFieldStrength_eval_eq_basis_repr, fieldStrengthMatrix_eq]
-
-lemma fieldStrengthMatrix_eq_tensor_basis_repr {d} (A : ElectromagneticPotential d)
-    (x : SpaceTime d) (μ ν : (Fin 1 ⊕ Fin d)) :
-    A.fieldStrengthMatrix x (μ, ν) =
-    (Tensor.basis _).repr (Tensorial.toTensor (toFieldStrength A x))
-    (fun | 0 => μ | 1 => ν) := by
-  rw [toFieldStrength_tensor_basis_eq_basis]
-  rfl
-
-lemma toFieldStrength_eq_fieldStrengthMatrix {d} (A : ElectromagneticPotential d) :
-    toFieldStrength A = fun x => ∑ μ, ∑ ν,
-      A.fieldStrengthMatrix x (μ, ν) • (Lorentz.Vector.basis μ) ⊗ₜ (Lorentz.Vector.basis ν) := by
-  ext x
-  apply (Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr.injective
-  simp only [map_sum, map_smul]
-  ext κ
-  match κ with
-  | (μ', ν') =>
-  simp [Finsupp.single_apply]
-  rfl
-
-/-!
-
-#### A.6.1. Differentiability of the field strength matrix
-
--/
-
-lemma fieldStrengthMatrix_differentiable {d} {A : ElectromagneticPotential d}
-    {μν} (hA : ContDiff ℝ 2 A) :
-    Differentiable ℝ (A.fieldStrengthMatrix · μν) := by
+lemma toFieldStrength_eval_differentiable {d} {A : ElectromagneticPotential d}
+    {μ ν : Fin 1 ⊕ Fin d} (hA : ContDiff ℝ 2 A) :
+    Differentiable ℝ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) := by
   have diff_partial (μ) :
       ∀ ν, Differentiable ℝ fun x => (fderiv ℝ A x) (Lorentz.Vector.basis μ) ν := by
     rw [SpaceTime.differentiable_vector]
     exact Differentiable.clm_apply
       (((contDiff_succ_iff_fderiv (n := 1)).mp hA).2.2.differentiable (by simp)) (by fun_prop)
-  conv => enter [2, x]; rw [toFieldStrength_basis_repr_apply_eq_single,
-    SpaceTime.deriv_eq, SpaceTime.deriv_eq]
+  simp only [toFieldStrength_eval_apply_eq_single, SpaceTime.deriv_eq]
   exact ((diff_partial _ _).const_mul _).sub ((diff_partial _ _).const_mul _)
 
-lemma fieldStrengthMatrix_differentiable_space {d} {A : ElectromagneticPotential d}
-    {μν} (hA : ContDiff ℝ 2 A) (t : Time) {c : SpeedOfLight} :
-    Differentiable ℝ (fun x => A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x)) μν) := by
-  change Differentiable ℝ ((A.fieldStrengthMatrix · μν) ∘ fun x => (toTimeAndSpace c).symm (t, x))
-  exact (fieldStrengthMatrix_differentiable hA).comp (by fun_prop)
-
-lemma fieldStrengthMatrix_differentiable_time {d} {A : ElectromagneticPotential d}
-    {μν} (hA : ContDiff ℝ 2 A) (x : Space d) {c : SpeedOfLight} :
-    Differentiable ℝ (fun t => A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x)) μν) := by
-  change Differentiable ℝ ((A.fieldStrengthMatrix · μν) ∘ fun t => (toTimeAndSpace c).symm (t, x))
-  exact (fieldStrengthMatrix_differentiable hA).comp (by fun_prop)
-
-lemma fieldStrengthMatrix_contDiff {d} {n : WithTop ℕ∞} {A : ElectromagneticPotential d}
-    {μν} (hA : ContDiff ℝ (n + 1) A) :
-    ContDiff ℝ n (A.fieldStrengthMatrix · μν) := by
-  conv => enter [3, x]; rw [toFieldStrength_basis_repr_apply_eq_single,
-    SpaceTime.deriv_eq, SpaceTime.deriv_eq]
-  apply ContDiff.sub
-  apply ContDiff.mul
-  · fun_prop
-  · match μν with
-    | (μ, ν) =>
-    simp only
-    revert ν
-    rw [SpaceTime.contDiff_vector]
-    exact ContDiff.clm_apply (ContDiff.fderiv_right (m := n) hA (by rfl)) (by fun_prop)
-  apply ContDiff.mul
-  · fun_prop
-  · match μν with
-    | (μ, ν) =>
-    simp only
-    revert μ
+lemma toFieldStrength_eval_differentiable_space {d} {A : ElectromagneticPotential d}
+    {μ ν : Fin 1 ⊕ Fin d} (hA : ContDiff ℝ 2 A) (t : Time) {c : SpeedOfLight} :
+    Differentiable ℝ (fun x =>
+      toField {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [μ] [ν]}ᵀ) := by
+  change Differentiable ℝ ((fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) ∘
+    fun x => (toTimeAndSpace c).symm (t, x))
+  exact (toFieldStrength_eval_differentiable hA).comp (by fun_prop)
+
+lemma toFieldStrength_eval_differentiable_time {d} {A : ElectromagneticPotential d}
+    {μ ν : Fin 1 ⊕ Fin d} (hA : ContDiff ℝ 2 A) (x : Space d) {c : SpeedOfLight} :
+    Differentiable ℝ (fun t =>
+      toField {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [μ] [ν]}ᵀ) := by
+  change Differentiable ℝ ((fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) ∘
+    fun t => (toTimeAndSpace c).symm (t, x))
+  exact (toFieldStrength_eval_differentiable hA).comp (by fun_prop)
+
+lemma toFieldStrength_eval_contDiff {d} {n : WithTop ℕ∞} {A : ElectromagneticPotential d}
+    {μ ν : Fin 1 ⊕ Fin d} (hA : ContDiff ℝ (n + 1) A) :
+    ContDiff ℝ n (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) := by
+  have h (μ) : ∀ ν, ContDiff ℝ n fun x => (fderiv ℝ A x) (Lorentz.Vector.basis μ) ν := by
     rw [SpaceTime.contDiff_vector]
     exact ContDiff.clm_apply (ContDiff.fderiv_right (m := n) hA (by rfl)) (by fun_prop)
+  simp only [toFieldStrength_eval_apply_eq_single, SpaceTime.deriv_eq]
+  exact (contDiff_const.mul (h _ _)).sub (contDiff_const.mul (h _ _))
 
-lemma fieldStrengthMatrix_smooth {d} {A : ElectromagneticPotential d}
-    (hA : ContDiff ℝ ∞ A) (μν) :
-    ContDiff ℝ ∞ (A.fieldStrengthMatrix · μν) :=
-  fieldStrengthMatrix_contDiff (by simpa using hA)
+lemma toFieldStrength_eval_smooth {d} {A : ElectromagneticPotential d}
+    (hA : ContDiff ℝ ∞ A) (μ ν : Fin 1 ⊕ Fin d) :
+    ContDiff ℝ ∞ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) :=
+  toFieldStrength_eval_contDiff (by simpa using hA)
 
 /-!
 
-### A.7. The antisymmetry of the field strength tensor
+### A.6. The antisymmetry of the field strength tensor
 
 We show that the field strength tensor is antisymmetric.
 
@@ -505,35 +453,31 @@ lemma toFieldStrength_antisymmetric {d} (A : ElectromagneticPotential d) (x : Sp
   simp only [Fin.isValue, neg_sub]
   rfl
 
-lemma fieldStrengthMatrix_antisymm {d} (A : ElectromagneticPotential d) (x : SpaceTime d)
+lemma toFieldStrength_eval_antisymm {d} (A : ElectromagneticPotential d) (x : SpaceTime d)
     (μ ν : Fin 1 ⊕ Fin d) :
-    A.fieldStrengthMatrix x (μ, ν) = - A.fieldStrengthMatrix x (ν, μ) := by
-  rw [toFieldStrength_basis_repr_apply, toFieldStrength_basis_repr_apply,
-    ← Finset.sum_neg_distrib]
+    toField {A.toFieldStrength x | [μ] [ν]}ᵀ = - toField {A.toFieldStrength x | [ν] [μ]}ᵀ := by
+  rw [toFieldStrength_eval_apply, toFieldStrength_eval_apply, ← Finset.sum_neg_distrib]
   exact Finset.sum_congr rfl fun κ _ => by simp
 
-@[simp]
-lemma fieldStrengthMatrix_diag_eq_zero {d} (A : ElectromagneticPotential d) (x : SpaceTime d)
+lemma toFieldStrength_eval_diag_eq_zero {d} (A : ElectromagneticPotential d) (x : SpaceTime d)
     (μ : Fin 1 ⊕ Fin d) :
-    A.fieldStrengthMatrix x (μ, μ) = 0 := by
-  simp [toFieldStrength_basis_repr_apply_eq_single]
+    toField {A.toFieldStrength x | [μ] [μ]}ᵀ = 0 := by
+  rw [toFieldStrength_eval_apply_eq_single, sub_self]
 
 /-!
 
-### A.8. Equivariance of the field strength matrix
+### A.7. Equivariance of the components of the field strength tensor
 
 -/
 
 set_option backward.isDefEq.respectTransparency false in
-lemma fieldStrengthMatrix_equivariant {d} (A : ElectromagneticPotential d)
+lemma toFieldStrength_eval_equivariant {d} (A : ElectromagneticPotential d)
     (Λ : LorentzGroup d) (hf : Differentiable ℝ A) (x : SpaceTime d)
-    (μ : (Fin 1 ⊕ Fin d)) (ν : Fin 1 ⊕ Fin d) :
-    fieldStrengthMatrix (Λ • A) x (μ, ν) =
-    ∑ κ, ∑ ρ, (Λ.1 μ κ * Λ.1 ν ρ) * A.fieldStrengthMatrix (Λ⁻¹ • x) (κ, ρ) := by
-  rw [fieldStrengthMatrix, toFieldStrength_equivariant A Λ hf x]
-  conv_rhs =>
-    enter [2, κ, 2, ρ]
-    rw [fieldStrengthMatrix]
+    (μ ν : Fin 1 ⊕ Fin d) :
+    toField {(Λ • A).toFieldStrength x | [μ] [ν]}ᵀ =
+    ∑ κ, ∑ ρ, (Λ.1 μ κ * Λ.1 ν ρ) * toField {A.toFieldStrength (Λ⁻¹ • x) | [κ] [ρ]}ᵀ := by
+  simp only [toFieldStrength_eval_eq_basis_repr]
+  rw [toFieldStrength_equivariant A Λ hf x]
   generalize A.toFieldStrength (Λ⁻¹ • x) = F
   let P (F : Lorentz.Vector d ⊗[ℝ] Lorentz.Vector d) : Prop :=
     ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (Λ • F)) (μ, ν) =
@@ -561,7 +505,7 @@ lemma fieldStrengthMatrix_equivariant {d} (A : ElectromagneticPotential d)
 
 /-!
 
-### A.9. Linearity of the field strength tensor
+### A.8. Linearity of the field strength tensor
 
 We show that the field strength tensor is linear in the potential.
 
@@ -571,10 +515,11 @@ set_option backward.isDefEq.respectTransparency false in
 lemma toFieldStrength_add {d} (A1 A2 : ElectromagneticPotential d)
     (x : SpaceTime d) (hA1 : Differentiable ℝ A1) (hA2 : Differentiable ℝ A2) :
     toFieldStrength (A1 + A2) x = toFieldStrength A1 x + toFieldStrength A2 x := by
-  apply (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr.injective
-  ext μν
+  apply Tensorial.toTensor.injective
+  apply (Tensor.basis _).repr.injective
+  ext b
   simp only [map_add, Finsupp.coe_add, Pi.add_apply]
-  repeat rw [toFieldStrength_basis_repr_apply]
+  repeat rw [toTensor_toFieldStrength_basis_repr]
   rw [← Finset.sum_add_distrib]
   apply Finset.sum_congr rfl (fun κ _ => ?_)
   repeat rw [SpaceTime.deriv_eq]
@@ -583,21 +528,23 @@ lemma toFieldStrength_add {d} (A1 A2 : ElectromagneticPotential d)
   simp only [_root_.add_apply, Lorentz.Vector.apply_add]
   ring
 
-set_option backward.isDefEq.respectTransparency false in
-lemma fieldStrengthMatrix_add {d} (A1 A2 : ElectromagneticPotential d)
-    (x : SpaceTime d) (hA1 : Differentiable ℝ A1) (hA2 : Differentiable ℝ A2) :
-    (A1 + A2).fieldStrengthMatrix x =
-    A1.fieldStrengthMatrix x + A2.fieldStrengthMatrix x := by
-  simp [fieldStrengthMatrix, toFieldStrength_add A1 A2 x hA1 hA2]
+lemma toFieldStrength_eval_add {d} (A1 A2 : ElectromagneticPotential d)
+    (x : SpaceTime d) (hA1 : Differentiable ℝ A1) (hA2 : Differentiable ℝ A2)
+    (μ ν : Fin 1 ⊕ Fin d) :
+    toField {(A1 + A2).toFieldStrength x | [μ] [ν]}ᵀ =
+    toField {A1.toFieldStrength x | [μ] [ν]}ᵀ + toField {A2.toFieldStrength x | [μ] [ν]}ᵀ := by
+  rw [toFieldStrength_add A1 A2 x hA1 hA2]
+  simp only [map_add]
 
 set_option backward.isDefEq.respectTransparency false in
 lemma toFieldStrength_smul {d} (c : ℝ) (A : ElectromagneticPotential d)
     (x : SpaceTime d) (hA : Differentiable ℝ A) :
     toFieldStrength (c • A) x = c • toFieldStrength A x := by
-  apply (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr.injective
-  ext μν
+  apply Tensorial.toTensor.injective
+  apply (Tensor.basis _).repr.injective
+  ext b
   simp only [map_smul, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul]
-  repeat rw [toFieldStrength_basis_repr_apply]
+  repeat rw [toTensor_toFieldStrength_basis_repr]
   rw [Finset.mul_sum]
   apply Finset.sum_congr rfl (fun κ _ => ?_)
   repeat rw [SpaceTime.deriv_eq]
@@ -606,11 +553,12 @@ lemma toFieldStrength_smul {d} (c : ℝ) (A : ElectromagneticPotential d)
   simp only [FunLike.coe_smul, Pi.smul_apply, Lorentz.Vector.apply_smul]
   ring
 
-set_option backward.isDefEq.respectTransparency false in
-lemma fieldStrengthMatrix_smul {d} (c : ℝ) (A : ElectromagneticPotential d)
-    (x : SpaceTime d) (hA : Differentiable ℝ A) :
-    (c • A).fieldStrengthMatrix x = c • A.fieldStrengthMatrix x := by
-  simp [fieldStrengthMatrix, toFieldStrength_smul c A x hA]
+lemma toFieldStrength_eval_smul {d} (c : ℝ) (A : ElectromagneticPotential d)
+    (x : SpaceTime d) (hA : Differentiable ℝ A) (μ ν : Fin 1 ⊕ Fin d) :
+    toField {(c • A).toFieldStrength x | [μ] [ν]}ᵀ =
+    c * toField {A.toFieldStrength x | [μ] [ν]}ᵀ := by
+  rw [toFieldStrength_smul c A x hA]
+  simp only [map_smul, smul_eq_mul]
 
 end ElectromagneticPotential
 
diff --git a/Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean b/Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean
index c3c1cc6310..d6b9e5f576 100644
--- a/Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean
+++ b/Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean
@@ -18,7 +18,7 @@ that the field strength tensor is invariant under such transformations.
 
 The raised-index gradient `∂^μ χ := η^{μν} ∂_ν χ` is necessary because the bare covariant gradient
 `∂_μ χ` does not make `F^{μν}` invariant. The formal witness is
-`fieldStrengthMatrix_bareGradient_inl_inr` (§B.5), which computes a specific nonzero component of
+`toFieldStrength_eval_bareGradient_inl_inr` (§B.5), which computes a specific nonzero component of
 the field strength of a bare-gradient potential. The invariance theorem
 `toFieldStrength_gaugeTransform` doubles as a correctness test of `ofGradient`.
 
@@ -29,13 +29,13 @@ the field strength of a bare-gradient potential. The invariance theorem
 - `toFieldStrength_ofGradient` : A pure-gauge potential has vanishing field strength.
 - `toFieldStrength_gaugeTransform` : The field strength tensor is invariant under gauge
   transformations.
-- `fieldStrengthMatrix_gaugeTransform` : The field strength matrix is invariant under gauge
-  transformations.
+- `toFieldStrength_eval_gaugeTransform` : The components of the field strength tensor are
+  invariant under gauge transformations.
 - `gaugeTransform_gaugeTransform` : Composing two gauge shifts equals shifting by the sum;
   upgrades one-step F-invariance to invariance along any finite chain.
 - `ofGradient_equivariant` : `ofGradient` intertwines the Lorentz action with function composition.
 - `gaugeTransform_equivariant` : Gauge transformations commute with Lorentz transformations.
-- `fieldStrengthMatrix_bareGradient_inl_inr` : The `(inl 0, inr i)` field-strength component of
+- `toFieldStrength_eval_bareGradient_inl_inr` : The `(inl 0, inr i)` field-strength component of
   the bare-gradient potential `χ(x) = x⁰·xⁱ` equals `2`; in particular the bare gradient does
   not give a gauge-invariant field strength (necessity of the metric contraction in `ofGradient`).
 
@@ -76,7 +76,6 @@ open Lorentz
 
 attribute [-simp] Fintype.sum_sum_type
 attribute [-simp] Nat.succ_eq_add_one
-
 /-!
 
 ## A. The pure-gauge potential
@@ -161,27 +160,21 @@ lemma contDiff_ofGradient {n} {d} {χ : SpaceTime d → ℝ} (hχ : ContDiff ℝ
 /-- A pure-gauge potential has vanishing field strength. -/
 lemma toFieldStrength_ofGradient {d} {χ : SpaceTime d → ℝ} (hχ : ContDiff ℝ 2 χ)
     (x : SpaceTime d) : (ofGradient χ).toFieldStrength x = 0 := by
-  apply (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr.injective
-  apply Finsupp.ext
-  intro μν
-  simp only [toFieldStrength_basis_repr_apply_eq_single]
-  rw [SpaceTime.deriv_apply_eq μν.1 μν.2 (ofGradient χ) (differentiable_ofGradient hχ),
-    SpaceTime.deriv_apply_eq μν.2 μν.1 (ofGradient χ) (differentiable_ofGradient hχ)]
+  rw [congrFun (toFieldStrength_eq_sum_basis_eval (A := ofGradient χ)) x]
+  refine Finset.sum_eq_zero fun μ _ => Finset.sum_eq_zero fun ν _ => ?_
+  rw [toFieldStrength_eval_apply_eq_single]
+  rw [SpaceTime.deriv_apply_eq μ ν (ofGradient χ) (differentiable_ofGradient hχ),
+    SpaceTime.deriv_apply_eq ν μ (ofGradient χ) (differentiable_ofGradient hχ)]
   simp only [ofGradient_apply]
-  rw [fderiv_const_mul (SpaceTime.differentiable_deriv μν.1 χ hχ).differentiableAt,
-    fderiv_const_mul (SpaceTime.differentiable_deriv μν.2 χ hχ).differentiableAt]
+  rw [fderiv_const_mul (SpaceTime.differentiable_deriv μ χ hχ).differentiableAt,
+    fderiv_const_mul (SpaceTime.differentiable_deriv ν χ hχ).differentiableAt]
   simp only [FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]
-  -- simplify repr 0 to 0
-  conv_rhs => rw [show (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
-      (0 : Lorentz.Vector d ⊗[ℝ] Lorentz.Vector d) = 0 from map_zero _]
-  simp only [Finsupp.zero_apply]
   -- use Clairaut: ∂_ μ (∂_ ν χ) x = ∂_ ν (∂_ μ χ) x, so the two terms cancel
-  have heq : fderiv ℝ (∂_ μν.2 χ) x (Lorentz.Vector.basis μν.1) =
-      fderiv ℝ (∂_ μν.1 χ) x (Lorentz.Vector.basis μν.2) := by
-    change ∂_ μν.1 (∂_ μν.2 χ) x = ∂_ μν.2 (∂_ μν.1 χ) x
-    rw [← SpaceTime.deriv_commute μν.2 μν.1 χ hχ]
-  rw [heq]
-  ring
+  have heq : fderiv ℝ (∂_ ν χ) x (Lorentz.Vector.basis μ) =
+      fderiv ℝ (∂_ μ χ) x (Lorentz.Vector.basis ν) := by
+    change ∂_ μ (∂_ ν χ) x = ∂_ ν (∂_ μ χ) x
+    rw [← SpaceTime.deriv_commute ν μ χ hχ]
+  rw [heq, mul_left_comm, sub_self, zero_smul]
 
 /-!
 
@@ -270,11 +263,13 @@ lemma toFieldStrength_gaugeTransform {d} (A : ElectromagneticPotential d)
   rw [gaugeTransform, toFieldStrength_add A (ofGradient χ) x hA (differentiable_ofGradient hχ),
     toFieldStrength_ofGradient hχ, add_zero]
 
-/-- The field strength matrix is invariant under gauge transformations. -/
-lemma fieldStrengthMatrix_gaugeTransform {d} (A : ElectromagneticPotential d)
-    (χ : SpaceTime d → ℝ) (hA : Differentiable ℝ A) (hχ : ContDiff ℝ 2 χ) (x : SpaceTime d) :
-    (gaugeTransform χ A).fieldStrengthMatrix x = A.fieldStrengthMatrix x := by
-  rw [fieldStrengthMatrix, toFieldStrength_gaugeTransform A χ hA hχ]
+/-- The components of the field strength tensor are invariant under gauge transformations. -/
+lemma toFieldStrength_eval_gaugeTransform {d} (A : ElectromagneticPotential d)
+    (χ : SpaceTime d → ℝ) (hA : Differentiable ℝ A) (hχ : ContDiff ℝ 2 χ) (x : SpaceTime d)
+    (μ ν : Fin 1 ⊕ Fin d) :
+    toField {(gaugeTransform χ A).toFieldStrength x | [μ] [ν]}ᵀ =
+    toField {A.toFieldStrength x | [μ] [ν]}ᵀ := by
+  rw [toFieldStrength_gaugeTransform A χ hA hχ]
 
 /-!
 
@@ -340,15 +335,15 @@ contraction in `ofGradient` is required for gauge invariance.
 
 -/
 
-/-- The `(inl 0, inr i)` component of the field strength matrix of the bare-gradient potential
+/-- The `(inl 0, inr i)` component of the field strength tensor of the bare-gradient potential
   `B^μ := ∂_μ χ` for `χ(x) = x⁰·xⁱ` equals `2`. This witnesses that the bare covariant gradient
   does not produce a gauge-invariant field strength, so the raised-index contraction
   `η^{μν} ∂_ν χ` in `ofGradient` is necessary (see the module overview). -/
-lemma fieldStrengthMatrix_bareGradient_inl_inr {d : ℕ} (i : Fin d)
+lemma toFieldStrength_eval_bareGradient_inl_inr {d : ℕ} (i : Fin d)
     (x : SpaceTime d) :
     let χ : SpaceTime d → ℝ := fun y => y (Sum.inl 0) * y (Sum.inr i)
     let B : ElectromagneticPotential d := ⟨fun y μ => ∂_ μ χ y⟩
-    B.fieldStrengthMatrix x (Sum.inl 0, Sum.inr i) = 2 := by
+    toField {B.toFieldStrength x | [Sum.inl 0] [Sum.inr i]}ᵀ = 2 := by
   intro χ B
   have hχ : ContDiff ℝ 2 χ := by
     show ContDiff ℝ 2 (fun y : SpaceTime d => y (Sum.inl 0) * y (Sum.inr i))
@@ -356,8 +351,8 @@ lemma fieldStrengthMatrix_bareGradient_inl_inr {d : ℕ} (i : Fin d)
   have hB : Differentiable ℝ B := by
     rw [← SpaceTime.differentiable_vector]; intro μ
     exact SpaceTime.differentiable_deriv μ χ hχ
-  -- fieldStrengthMatrix (μ, ν) = η μ μ * ∂_ μ B x ν − η ν ν * ∂_ ν B x μ
-  rw [toFieldStrength_basis_repr_apply_eq_single]
+  -- F^{μν} = η μ μ * ∂_ μ B x ν − η ν ν * ∂_ ν B x μ
+  rw [toFieldStrength_eval_apply_eq_single]
   -- Expand ∂_ μ B x ν as ∂_ μ (fun y => ∂_ ν χ y) x = ∂_ μ (∂_ ν χ) x
   rw [SpaceTime.deriv_apply_eq (Sum.inl 0) (Sum.inr i) B hB,
       SpaceTime.deriv_apply_eq (Sum.inr i) (Sum.inl 0) B hB]
@@ -391,19 +386,17 @@ lemma fieldStrengthMatrix_bareGradient_inl_inr {d : ℕ} (i : Fin d)
   norm_num
 
 /-- The field strength of the bare-gradient potential `B^μ := ∂_μ χ` for
-  `χ(x) = x⁰·xⁱ` is nonzero (follows from `fieldStrengthMatrix_bareGradient_inl_inr`). -/
+  `χ(x) = x⁰·xⁱ` is nonzero (follows from `toFieldStrength_eval_bareGradient_inl_inr`). -/
 lemma toFieldStrength_bareGradient_ne_zero {d : ℕ} (i : Fin d)
     (x : SpaceTime d) :
     let χ : SpaceTime d → ℝ := fun y => y (Sum.inl 0) * y (Sum.inr i)
     let B : ElectromagneticPotential d := ⟨fun y μ => ∂_ μ χ y⟩
     B.toFieldStrength x ≠ 0 := by
   intro χ B h
-  have h2 := fieldStrengthMatrix_bareGradient_inl_inr i x
+  have h2 := toFieldStrength_eval_bareGradient_inl_inr i x
   dsimp only at h2
-  rw [fieldStrengthMatrix_eq, h] at h2
-  have h3 : ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr
-      (0 : Lorentz.CoVector d ⊗[ℝ] Lorentz.Vector d)) = 0 := map_zero _
-  erw [h3, Finsupp.zero_apply] at h2
+  rw [h] at h2
+  simp only [map_zero] at h2
   norm_num at h2
 
 end ElectromagneticPotential
diff --git a/Physlib/Electromagnetism/Kinematics/MagneticField.lean b/Physlib/Electromagnetism/Kinematics/MagneticField.lean
index 1d88db0dd1..d2162bb868 100644
--- a/Physlib/Electromagnetism/Kinematics/MagneticField.lean
+++ b/Physlib/Electromagnetism/Kinematics/MagneticField.lean
@@ -64,6 +64,7 @@ open TensorProduct
 open minkowskiMatrix
 attribute [-simp] Fintype.sum_sum_type
 attribute [-simp] Nat.succ_eq_add_one
+attribute [-simp] Fin.succAbove_zero
 
 open Space Time
 
@@ -83,16 +84,16 @@ lemma magneticField_eq {c : SpeedOfLight} (A : ElectromagneticPotential) :
 
 /-!
 
-### A.1. Relation between the magnetic field and the field strength matrix
+### A.1. Relation between the magnetic field and the field strength tensor
 
 -/
 
-lemma magneticField_coord_eq_fieldStrengthMatrix {i : Fin 3} {c : SpeedOfLight}
+lemma magneticField_coord_eq_toFieldStrength_eval {i : Fin 3} {c : SpeedOfLight}
     (A : ElectromagneticPotential) (t : Time)
     (x : Space) (hA : Differentiable ℝ A) :
-    A.magneticField c t x i =
-    - A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x)) (Sum.inr (i+1), Sum.inr (i+2)) := by
-  rw [toFieldStrength_basis_repr_apply_eq_single]
+    A.magneticField c t x i = - toField {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) |
+      [Sum.inr (i+1)] [Sum.inr (i+2)]}ᵀ := by
+  rw [toFieldStrength_eval_apply_eq_single]
   simp only [Fin.isValue, inr_i_inr_i, neg_mul, one_mul, sub_neg_eq_add, neg_add_rev, neg_neg]
   rw [magneticField]
   simp only [curl, Fin.isValue]
@@ -160,13 +161,13 @@ lemma ofElectromagneticField_magneticField {c : SpeedOfLight}
 
 /-!
 
-## B. The field strength matrix in terms of the electric and magnetic fields
+## B. The components of the field strength tensor in terms of the electric and magnetic fields
 
 -/
 
-lemma fieldStrengthMatrix_eq_electric_magnetic {c} (A : ElectromagneticPotential) (t : Time)
+lemma toFieldStrength_eval_eq_electric_magnetic {c} (A : ElectromagneticPotential) (t : Time)
     (x : Space) (hA : Differentiable ℝ A) (μ ν : Fin 1 ⊕ Fin 3) :
-    A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x)) (μ, ν) =
+    toField {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [μ] [ν]}ᵀ =
     match μ, ν with
     | Sum.inl 0, Sum.inl 0 => 0
     | Sum.inl 0, Sum.inr i => - A.electricField c t x i / c
@@ -183,22 +184,22 @@ lemma fieldStrengthMatrix_eq_electric_magnetic {c} (A : ElectromagneticPotential
     | 2, 1 => A.magneticField c t x 0
     | 2, 2 => 0 := by
   match μ, ν with
-  | Sum.inl 0, Sum.inl 0 => simp
-  | Sum.inl 0, Sum.inr i => simp [electricField_eq_fieldStrengthMatrix A t x i hA]
+  | Sum.inl 0, Sum.inl 0 => simp [toFieldStrength_eval_diag_eq_zero]
+  | Sum.inl 0, Sum.inr i => simp [electricField_eq_toFieldStrength_eval A t x i hA]
   | Sum.inr i, Sum.inl 0 =>
-    simp [electricField_eq_fieldStrengthMatrix A t x i hA]
+    simp [electricField_eq_toFieldStrength_eval A t x i hA]
     field_simp
-    rw [fieldStrengthMatrix_antisymm]
+    rw [toFieldStrength_eval_antisymm]
   | Sum.inr i, Sum.inr j =>
     fin_cases i <;> fin_cases j <;>
-    simp [magneticField_coord_eq_fieldStrengthMatrix A t x hA]
-    repeat rw [fieldStrengthMatrix_antisymm]
+    simp [magneticField_coord_eq_toFieldStrength_eval A t x hA, toFieldStrength_eval_diag_eq_zero]
+    repeat rw [toFieldStrength_eval_antisymm]
 
-lemma fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime (c : SpeedOfLight)
+lemma toFieldStrength_eval_eq_electric_magnetic_of_spaceTime (c : SpeedOfLight)
     (A : ElectromagneticPotential)
     (x : SpaceTime) (hA : Differentiable ℝ A) (μ ν : Fin 1 ⊕ Fin 3) :
     let tx := SpaceTime.toTimeAndSpace c x
-    A.fieldStrengthMatrix x (μ, ν) =
+    toField {A.toFieldStrength x | [μ] [ν]}ᵀ =
     match μ, ν with
     | Sum.inl 0, Sum.inl 0 => 0
     | Sum.inl 0, Sum.inr i => - A.electricField c tx.1 tx.2 i / c
@@ -215,7 +216,7 @@ lemma fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime (c : SpeedOfLight)
     | 2, 1 => A.magneticField c tx.1 tx.2 0
     | 2, 2 => 0 := by
   dsimp
-  rw [← fieldStrengthMatrix_eq_electric_magnetic A]
+  rw [← toFieldStrength_eval_eq_electric_magnetic A]
   simp only [Prod.mk.eta, ContinuousLinearEquiv.symm_apply_apply]
   exact hA
 
@@ -229,16 +230,17 @@ lemma fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime (c : SpeedOfLight)
   In `3` space-dimensions this reduces to a vector. -/
 noncomputable def magneticFieldMatrix (c : SpeedOfLight := 1) (A : ElectromagneticPotential d) :
     Time → Space d → (Fin d × Fin d) → ℝ := timeSlice c <| fun x ij =>
-    A.fieldStrengthMatrix x (Sum.inr ij.1, Sum.inr ij.2)
+    toField {A.toFieldStrength x | [Sum.inr ij.1] [Sum.inr ij.2]}ᵀ
 
 lemma magneticFieldMatrix_eq {c : SpeedOfLight} (A : ElectromagneticPotential d) :
     A.magneticFieldMatrix c = fun t x ij =>
-      A.fieldStrengthMatrix ((toTimeAndSpace c).symm (t, x)) (Sum.inr ij.1, Sum.inr ij.2) := rfl
+      toField {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) |
+        [Sum.inr ij.1] [Sum.inr ij.2]}ᵀ := rfl
 
-lemma fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix {c : SpeedOfLight}
+lemma toFieldStrength_eval_inr_inr_eq_magneticFieldMatrix {c : SpeedOfLight}
     (A : ElectromagneticPotential d)
     (x : SpaceTime d) (i j : Fin d) :
-    A.fieldStrengthMatrix x (Sum.inr i, Sum.inr j) =
+    toField {A.toFieldStrength x | [Sum.inr i] [Sum.inr j]}ᵀ =
     A.magneticFieldMatrix c (x.time c) x.space (i, j) := by
   simp [magneticFieldMatrix_eq]
 
@@ -252,14 +254,14 @@ lemma magneticFieldMatrix_antisymm {c : SpeedOfLight}
     (A : ElectromagneticPotential d) (t : Time)
     (x : Space d) (i j : Fin d) :
     A.magneticFieldMatrix c t x (i, j) = - A.magneticFieldMatrix c t x (j, i) :=
-  fieldStrengthMatrix_antisymm A ((toTimeAndSpace c).symm (t, x)) (Sum.inr i) (Sum.inr j)
+  toFieldStrength_eval_antisymm A ((toTimeAndSpace c).symm (t, x)) (Sum.inr i) (Sum.inr j)
 
 @[simp]
 lemma magneticFieldMatrix_diag_eq_zero {c : SpeedOfLight}
     (A : ElectromagneticPotential d) (t : Time)
     (x : Space d) (i : Fin d) :
     A.magneticFieldMatrix c t x (i, i) = 0 :=
-  fieldStrengthMatrix_diag_eq_zero A ((toTimeAndSpace c).symm (t, x)) (Sum.inr i)
+  toFieldStrength_eval_diag_eq_zero A ((toTimeAndSpace c).symm (t, x)) (Sum.inr i)
 
 /-!
 
@@ -272,7 +274,7 @@ lemma magneticField_eq_magneticFieldMatrix {c : SpeedOfLight} (A : Electromagnet
     A.magneticField c = fun t x => WithLp.toLp 2 fun i =>
       - A.magneticFieldMatrix c t x ((i+1), (i+2)) := by
   ext t x
-  simp [magneticFieldMatrix_eq, magneticField_coord_eq_fieldStrengthMatrix A t x hA]
+  simp [magneticFieldMatrix_eq, magneticField_coord_eq_toFieldStrength_eval A t x hA]
 
 lemma magneticField_curl_eq_magneticFieldMatrix{c : SpeedOfLight} (A : ElectromagneticPotential)
     (hA : ContDiff ℝ 2 A) (t : Time) :
@@ -300,7 +302,7 @@ lemma magneticFieldMatrix_eq_vectorPotential {c : SpeedOfLight} (A : Electromagn
     A.magneticFieldMatrix c t x (i, j) = Space.deriv j (A.vectorPotential c t · i) x -
     Space.deriv i (A.vectorPotential c t · j) x := by
   simp only [magneticFieldMatrix_eq]
-  rw [toFieldStrength_basis_repr_apply_eq_single]
+  rw [toFieldStrength_eval_apply_eq_single]
   simp only [inr_i_inr_i, neg_mul, one_mul, sub_neg_eq_add]
   rw [SpaceTime.deriv_sum_inr c _ hA, SpaceTime.deriv_sum_inr c _ hA]
   simp [vectorPotential]
@@ -320,7 +322,7 @@ lemma magneticFieldMatrix_eq_vectorPotential {c : SpeedOfLight} (A : Electromagn
 lemma magneticFieldMatrix_contDiff {n} {c : SpeedOfLight} (A : ElectromagneticPotential d)
     (hA : ContDiff ℝ (n + 1) A) (ij) :
     ContDiff ℝ n ↿(fun t x => A.magneticFieldMatrix c t x ij) := by
-  exact (fieldStrengthMatrix_contDiff hA).comp (toTimeAndSpace c).symm.contDiff
+  exact (toFieldStrength_eval_contDiff hA).comp (toTimeAndSpace c).symm.contDiff
 
 lemma magneticFieldMatrix_space_contDiff {n} {c : SpeedOfLight} (A : ElectromagneticPotential d)
     (hA : ContDiff ℝ (n + 1) A) (t : Time) (ij) :
@@ -340,7 +342,7 @@ lemma magneticFieldMatrix_time_contDiff {n} {c : SpeedOfLight} (A : Electromagne
 
 lemma magneticFieldMatrix_differentiable {c : SpeedOfLight} (A : ElectromagneticPotential d)
     (hA : ContDiff ℝ 2 A) (ij) : Differentiable ℝ ↿(fun t x => A.magneticFieldMatrix c t x ij) := by
-  exact (fieldStrengthMatrix_differentiable hA).comp (toTimeAndSpace c).symm.differentiable
+  exact (toFieldStrength_eval_differentiable hA).comp (toTimeAndSpace c).symm.differentiable
 
 lemma magneticFieldMatrix_differentiable_space {c : SpeedOfLight} (A : ElectromagneticPotential d)
     (hA : ContDiff ℝ 2 A) (t : Time) (ij) :
@@ -456,12 +458,12 @@ lemma time_deriv_time_deriv_magneticFieldMatrix {d : ℕ} {c : SpeedOfLight}
 
 -/
 
-lemma curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix {d : ℕ} {c : SpeedOfLight}
+lemma curl_magneticFieldMatrix_eq_electricField_toFieldStrength_eval {d : ℕ} {c : SpeedOfLight}
     (A : ElectromagneticPotential d)
     (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i : Fin d) :
     ∑ j, Space.deriv j (A.magneticFieldMatrix c t · (j, i)) x =
     (1/c^2) * ∂ₜ (fun t => A.electricField c t x) t i +
-    (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (A.fieldStrengthMatrix · (μ, Sum.inr i))
+    (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [Sum.inr i]}ᵀ)
     ((toTimeAndSpace c).symm (t, x)))) := by
   trans (1/c^2) * ∂ₜ (fun t => A.electricField c t x) t i +
     (- (1/c^2) * ∂ₜ (fun t => A.electricField c t x) t i +
@@ -471,13 +473,13 @@ lemma curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix {d : ℕ} {c
   rw [Fintype.sum_sum_type]
   congr
   · simp
-    rw [time_deriv_electricField_eq_fieldStrengthMatrix hA t x i]
+    rw [time_deriv_electricField_eq_toFieldStrength_eval hA t x i]
     field_simp
   · funext j
     rw [SpaceTime.deriv_sum_inr c]
     simp
     rfl
-    · apply fieldStrengthMatrix_differentiable hA
+    · apply toFieldStrength_eval_differentiable hA
 
 end ElectromagneticPotential
 
diff --git a/Physlib/Electromagnetism/Vacuum/IsPlaneWave.lean b/Physlib/Electromagnetism/Vacuum/IsPlaneWave.lean
index aceb3a626a..e9e75951e1 100644
--- a/Physlib/Electromagnetism/Vacuum/IsPlaneWave.lean
+++ b/Physlib/Electromagnetism/Vacuum/IsPlaneWave.lean
@@ -481,23 +481,23 @@ lemma space_deriv_electricField_eq_magneticFieldMatrix {d : ℕ}
   simp [← Time.deriv_eq]
   field_simp
   any_goals apply Differentiable.differentiableAt
-  · exact fieldStrengthMatrix_differentiable_space hA2 t
+  · exact toFieldStrength_eval_differentiable_space hA2 t
   · apply Differentiable.mul_const
-    exact fieldStrengthMatrix_differentiable_space hA2 t
-  · exact fieldStrengthMatrix_differentiable_time hA2 x
+    exact toFieldStrength_eval_differentiable_space hA2 t
+  · exact toFieldStrength_eval_differentiable_time hA2 x
   · intro i _
     apply Differentiable.differentiableAt
     apply Differentiable.const_mul
     apply Differentiable.mul_const
-    exact fieldStrengthMatrix_differentiable_space hA2 t
+    exact toFieldStrength_eval_differentiable_space hA2 t
   · intro i _
     apply Differentiable.differentiableAt
     apply Differentiable.mul_const
-    exact fieldStrengthMatrix_differentiable_time hA2 x
+    exact toFieldStrength_eval_differentiable_time hA2 x
   · apply Differentiable.fun_sum
     intro i _
     apply Differentiable.mul_const
-    exact fieldStrengthMatrix_differentiable_time hA2 x
+    exact toFieldStrength_eval_differentiable_time hA2 x
 
 /-!
 
diff --git a/Physlib/Relativity/Tensors/Elab.lean b/Physlib/Relativity/Tensors/Elab.lean
index f64ec30e46..65573c3b68 100644
--- a/Physlib/Relativity/Tensors/Elab.lean
+++ b/Physlib/Relativity/Tensors/Elab.lean
@@ -74,8 +74,10 @@ syntax ident : indexExpr
 syntax num : indexExpr
 
 
-/-- Notation to describe the evaluation of a tensor index. -/
-syntax "[" ident "]" : indexExpr
+/-- Notation to describe the evaluation of a tensor index. The term inside the brackets is
+  the value of the index, which can be an identifier `[μ]` or an arbitrary term such as
+  `[Sum.inl 0]`. -/
+syntax "[" term "]" : indexExpr
 
 /-- Notation to describe the jiggle of a tensor index. -/
 syntax "τ(" ident ")" : indexExpr
@@ -120,10 +122,16 @@ def indexToIdent (stx : Syntax) : TermElabM Ident :=
   match stx with
   | `(indexExpr|$a:ident) => return a
   | `(indexExpr| τ($a:ident)) => return a
-  | `(indexExpr| [$a:ident]) => return a
   | _ =>
     throwError "Unsupported expression syntax in indexToIdent: {stx}"
 
+/-- For an evaluated bracket index `[t]`, the term `t` giving the value of the index. -/
+def indexToBracketTerm (stx : Syntax) : TermElabM Term :=
+  match stx with
+  | `(indexExpr| [$a:term]) => return a
+  | _ =>
+    throwError "Unsupported expression syntax in indexToBracketTerm: {stx}"
+
 /-- Takes a pair ``a b : ℕ × TSyntax `indexExpr``. If `a.1 < b.1` and `a.2 = b.2` then
   outputs `some (a.1, b.1)`, otherwise `none`. -/
 def indexPosEq (a b : TSyntax `indexExpr × ℕ) : TermElabM (Option (ℕ × ℕ)) := do
@@ -198,7 +206,7 @@ def getEvalPos (ind : List (TSyntax `indexExpr)) : TermElabM (List (ℕ × ℕ))
 def getEvalBracketPos (ind : List (TSyntax `indexExpr)) : TermElabM (List (ℕ × Term)) := do
   let indEnum := ind.zipIdx
   let evals := indEnum.filter (fun x => indexExprIsBracketEval x.1)
-  let evals2 ← (evals.mapM (fun x => indexToIdent x.1))
+  let evals2 ← (evals.mapM (fun x => indexToBracketTerm x.1))
   let pos := evalAdjustPos (evals.map (fun x => x.2))
   return List.zip pos evals2
 
diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean
index 258bbaf955..6f75ee9259 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean
@@ -143,7 +143,6 @@ lemma minkowskiProduct_toCoord_minkowskiMatrix {d : ℕ} (p q : Vector d) :
     neg_mul, Finset.sum_neg_distrib]
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma minkowskiProduct_invariant {d : ℕ} (p q : Vector d) (Λ : LorentzGroup d) :
     ⟪Λ • p, Λ • q⟫ₘ = ⟪p, q⟫ₘ := by
@@ -226,7 +225,6 @@ def adjoint {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) : Vector d →ₗ[ℝ]
   minkowskiMatrix.dual <|
   LinearMap.toMatrix Vector.basis Vector.basis f
 
-set_option backward.isDefEq.respectTransparency false in
 lemma map_minkowskiProduct_eq_adjoint {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) (p q : Vector d) :
     ⟪f p, q⟫ₘ = ⟪p, adjoint f q⟫ₘ := by
   rw [minkowskiProduct_toCoord_minkowskiMatrix, minkowskiProduct_toCoord_minkowskiMatrix]