Canonical Momentum eq electric Field

lemma canonicalMomentum_eq_electricField {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)    (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) :    A.canonicalMomentum 𝓕 J = fun x => fun μ =>      match μ with      | Sum.inl 0 => 0      | Sum.inr i => - (1/(𝓕.μ₀ * 𝓕.c)) * A.electricField 𝓕.c (x.time 𝓕.c) x.space i := by  rw [canonicalMomentum_eq A hA J]  funext x μ  match μ with  | Sum.inl 0 => simp  | 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))]  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)