Space deriv electric Field eq magnetic Field Matrix

lemma space_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 k : Fin d) :    ∂[k] (A.electricField 𝓕.c t · i) x =    ∂[k] (fun x => 𝓕.c * ∑ j, A.magneticFieldMatrix 𝓕.c t x (i, j) * s.unit j) x := by  have hA2 : ContDiff ℝ 2 A := hA.of_le ENat.LEInfty.out  rw [P.electricField_space_deriv_eq_time_deriv hA2 t x i k,    P.time_deriv_electricField_eq_magneticFieldMatrix hA h t x i, Time.deriv_eq, fderiv_const_mul,    fderiv_fun_sum]  simp [Finset.mul_sum, - Finset.sum_neg_distrib]  rw [Space.deriv_eq_fderiv_basis, fderiv_fun_sum]  simp [- Finset.sum_neg_distrib]  congr  funext j  rw [fderiv_mul_const, fderiv_const_mul, fderiv_mul_const]  simp only [FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]  rw [← Space.deriv_eq_fderiv_basis, P.magneticFieldMatrix_space_deriv_eq_time_deriv hA2 t x i j k]  simp [← Time.deriv_eq]  field_simp  any_goals apply Differentiable.differentiableAt  · exact fieldStrengthMatrix_differentiable_space hA2 t  · apply Differentiable.mul_const    exact fieldStrengthMatrix_differentiable_space hA2 t  · exact fieldStrengthMatrix_differentiable_time hA2 x  · intro i _    apply Differentiable.differentiableAt    apply Differentiable.const_mul    apply Differentiable.mul_const    exact fieldStrengthMatrix_differentiable_space hA2 t  · intro i _    apply Differentiable.differentiableAt    apply Differentiable.mul_const    exact fieldStrengthMatrix_differentiable_time hA2 x  · apply Differentiable.fun_sum    intro i _    apply Differentiable.mul_const    exact fieldStrengthMatrix_differentiable_time hA2 x