Magnetic Field Matrix eq propogator cross electric Field

lemma magneticFieldMatrix_eq_propogator_cross_electricField {d : ℕ}    {𝓕 : FreeSpace} {A : ElectromagneticPotential d}    {s : Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A) (i j : Fin d) :    ∃ C, ∀ t x, A.magneticFieldMatrix 𝓕.c t x (i, j) =    1/ 𝓕.c * (s.unit j * A.electricField 𝓕.c t x i -      s.unit i * A.electricField 𝓕.c t x j) + C := by  apply Space.equal_up_to_const_of_deriv_eq  · exact magneticFieldMatrix_differentiable A hA (i, j)  · exact (((electricField_apply_differentiable hA).const_mul _).sub      ((electricField_apply_differentiable hA).const_mul _)).const_mul _  · intro t x    rw [P.time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator hA t x i j]    congr    funext t    field_simp  · intro t x k    rw [P.space_deriv_magneticFieldMatrix_eq_electricField_mul_propogator hA t x i j]    congr    funext x    field_simp