Electric Field eq field Strength Matrix

lemma electricField_eq_fieldStrengthMatrix {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]  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]  congr  · simp only [grad_apply, Fin.isValue]    trans c * ∂_ (Sum.inr i) (fun x => A x (Sum.inl 0)) ((toTimeAndSpace c).symm (t, x)); swap    · rw [SpaceTime.deriv_eq, SpaceTime.deriv_eq]      rw [Lorentz.Vector.fderiv_apply]      exact hA    · rw [SpaceTime.deriv_sum_inr c]      simp [scalarPotential]      change Space.deriv i (fun y => c * A ((toTimeAndSpace c).symm (t, y)) (Sum.inl 0)) x = _      rw [Space.deriv_eq_fderiv_basis, fderiv_const_mul]      simp [← Space.deriv_eq_fderiv_basis]      · fun_prop      · exact differentiable_component A hA _  · exact 2  · rw [SpaceTime.deriv_sum_inl c]    simp only [ContinuousLinearEquiv.apply_symm_apply]    rw [Time.deriv_eq, Time.deriv_eq]    rw [vectorPotential]    simp [timeSlice]    rw [Lorentz.Vector.fderiv_apply]    change ((fderiv ℝ (fun t => WithLp.toLp 2 fun i =>        A ((toTimeAndSpace c).symm (t, x)) (Sum.inr i)) t) 1).ofLp i = _    rw [← Time.fderiv_euclid]    · apply Time.differentiable_euclid      intro i      simp only      fun_prop    · fun_prop    · exact hA  · exact 1