Space deriv magnetic Field Matrix eq electric Field mul propogator

lemma space_deriv_magneticFieldMatrix_eq_electricField_mul_propogator {d : ℕ}    {𝓕 : FreeSpace} {A : ElectromagneticPotential d}    {s : Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ 2 A)    (t : Time) (x : Space d) (i j k : Fin d) :    ∂[k] (A.magneticFieldMatrix 𝓕.c t · (i, j)) x =    ∂[k] (fun x => s.unit j / 𝓕.c * A.electricField 𝓕.c t x i    - s.unit i / 𝓕.c * A.electricField 𝓕.c t x j) x := by  rw [P.magneticFieldMatrix_space_deriv_eq_time_deriv hA,    P.time_deriv_magneticFieldMatrix_eq_electricField_mul_propogator hA,    Space.deriv_eq_fderiv_basis, fderiv_fun_sub, fderiv_const_mul, fderiv_const_mul]  simp [← Space.deriv_eq_fderiv_basis]  rw [Time.deriv_eq, fderiv_fun_sub, fderiv_const_mul, fderiv_const_mul]  simp [← Time.deriv_eq]  rw [P.electricField_space_deriv_eq_time_deriv hA, P.electricField_space_deriv_eq_time_deriv hA]  simp only [smul_eq_mul, neg_mul, mul_neg, sub_neg_eq_add]  field_simp  ring  any_goals apply Differentiable.differentiableAt  any_goals apply Differentiable.const_mul  any_goals exact electricField_apply_differentiable_time hA x _  any_goals exact electricField_apply_differentiable_space hA t _