Time deriv electric Field eq magnetic Field Matrix

lemma time_deriv_electricField_eq_magneticFieldMatrix {d : ℕ}    {𝓕 : FreeSpace} {A : ElectromagneticPotential d}    {s : Direction d} (P : IsPlaneWave 𝓕 A s) (hA : ContDiff ℝ ∞ A)    (h : IsExtrema 𝓕 A 0)    (t : Time) (x : Space d) (i : Fin d) :    ∂ₜ (A.electricField 𝓕.c · x i) t =    ∂ₜ (fun t => 𝓕.c * ∑ j, A.magneticFieldMatrix 𝓕.c t x (i, j) * s.unit j) t := by  have hBd : ∀ k, Differentiable ℝ (fun t => A.magneticFieldMatrix 𝓕.c t x (i, k)) :=    fun k => magneticFieldMatrix_differentiable_time A (hA.of_le ENat.LEInfty.out) x (i, k)  rw [Time.deriv_euclid, time_deriv_electricField_of_isExtrema hA 0 _ h t x i]  simp only [one_div, _root_.mul_inv_rev, LorentzCurrentDensity.currentDensity_zero, Pi.zero_apply,    PiLp.zero_apply, mul_zero, sub_zero]  conv_lhs =>    enter [2, 2, i];    rw [magneticFieldMatrix_space_deriv_eq_time_deriv P (hA.of_le ENat.LEInfty.out) t x i]  rw [Time.deriv_eq, fderiv_const_mul]  simp [← Time.deriv_eq]  have h1 : ∂ₜ (fun t => ∑ j, A.magneticFieldMatrix 𝓕.c t x (i, j) * s.unit j) t    = ∑ j, ∂ₜ (A.magneticFieldMatrix 𝓕.c · x (i, j)) t * s.unit j := by    rw [Time.deriv_eq, fderiv_fun_sum]    simp only [FunLike.coe_sum, Finset.sum_apply]    conv_lhs =>      enter [2, k]      rw [fderiv_mul_const (hBd _).differentiableAt]    simp only [FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]    congr    funext i    ring_nf    rfl    · intro k _      apply DifferentiableAt.mul_const      exact (hBd k).differentiableAt   rw [h1, Finset.mul_sum, Finset.mul_sum,← Finset.sum_neg_distrib]  field_simp  congr  funext k  field_simp  simp [𝓕.c_sq]  field_simp  conv_lhs =>    enter [1, 2, 1, t]    rw [magneticFieldMatrix_antisymm]  rw [Time.deriv_eq, fderiv_fun_neg]  simp [← Time.deriv_eq]  · refine DifferentiableAt.fun_sum ?_    intro k _    apply DifferentiableAt.mul_const    exact (hBd k).differentiableAt  · change ContDiff ℝ ∞ (fun _ => 0)    fun_prop  · exact electricField_differentiable_time (hA.of_le (ENat.LEInfty.out)) x