Time deriv magnetic Field Matrix

lemma time_deriv_magneticFieldMatrix {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d)    (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i j : Fin d) :    ∂ₜ (A.magneticFieldMatrix c · x (i, j)) t =    ∂[i] (A.electricField c t · j) x - ∂[j] (A.electricField c t · i) x := by  calc _    _ = ∂ₜ (fun t => ∂[j] (fun x => A.vectorPotential c t x i) x) t        - ∂ₜ (fun t => ∂[i] (fun x => A.vectorPotential c t x j) x) t := by      conv_lhs =>        enter [1, t]        rw [magneticFieldMatrix_eq_vectorPotential _ (hA.differentiable (by simp))]      rw [Time.deriv, fderiv_fun_sub]      rfl      all_goals      · apply Differentiable.differentiableAt        apply Space.space_deriv_differentiable_time        apply vectorPotential_comp_contDiff _ hA    _ = ∂[j] (fun x => ∂ₜ (fun t => A.vectorPotential c t x i) t) x        - ∂[i] (fun x => ∂ₜ (fun t => A.vectorPotential c t x j) t) x := by      rw [Space.time_deriv_comm_space_deriv _, Space.time_deriv_comm_space_deriv _]      all_goals      · apply vectorPotential_comp_contDiff _ hA    _ = ∂[i] (A.electricField c t · j) x - ∂[j] (A.electricField c t · i) x := by      have hφ := scalarPotential_contDiff_space c A hA t      have hd1 : ∀ k : Fin d, DifferentiableAt ℝ (fun x => -(A.electricField c t x).ofLp k) x :=        fun k => (electricField_apply_differentiable_space hA t k).neg.differentiableAt      have hd2 : ∀ k : Fin d, DifferentiableAt ℝ (Space.deriv k (scalarPotential c A t)) x :=        fun k => (Space.deriv_differentiable hφ k).differentiableAt      conv_lhs =>        enter [1, 2, x]        rw [time_deriv_comp_vectorPotential_eq_electricField (hA.differentiable (by simp))]      conv_lhs =>        enter [2, 2, x]        rw [time_deriv_comp_vectorPotential_eq_electricField (hA.differentiable (by simp))]      rw [Space.deriv_eq_fderiv_basis, fderiv_fun_sub (hd1 i) (hd2 i), fderiv_fun_neg]      conv_lhs =>        enter [2]        rw [Space.deriv_eq_fderiv_basis, fderiv_fun_sub (hd1 j) (hd2 j), fderiv_fun_neg]      simp only [FunLike.coe_sub, Pi.sub_apply, _root_.neg_apply, ← Space.deriv_eq_fderiv_basis]      rw [Space.deriv_commute _ hφ]      ring