Kinetic Term eq electric Matrix magnetic Field Matrix time space

lemma kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space {𝓕 : FreeSpace}    (A : ElectromagneticPotential d) (t : Time)    (x : Space d) (hA : Differentiable ℝ A) :    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]  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  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    rw [EuclideanSpace.norm_sq_eq]    conv_lhs =>      enter [2, i]      rw [electricField_eq_fieldStrengthMatrix 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]  field_simp  ring