Field Strength Matrix eq electric magnetic

lemma fieldStrengthMatrix_eq_electric_magnetic {c} (A : ElectromagneticPotential) (t : Time)    (x : Space) (hA : Differentiable ℝ A) (μ ν : Fin 1 ⊕ Fin 3) :    A.fieldStrengthMatrix ((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    | Sum.inr i, Sum.inl 0 => A.electricField c t x i / c    | Sum.inr i, Sum.inr j =>    match i, j with    | 0, 0 => 0    | 0, 1 => - A.magneticField c t x 2    | 0, 2 => A.magneticField c t x 1    | 1, 0 => A.magneticField c t x 2    | 1, 1 => 0    | 1, 2 => - A.magneticField c t x 0    | 2, 0 => - A.magneticField c t x 1    | 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.inr i, Sum.inl 0 =>    simp [electricField_eq_fieldStrengthMatrix A t x i hA]    field_simp    rw [fieldStrengthMatrix_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]