Constant EB vector Potential space deriv

lemma constantEB_vectorPotential_space_deriv {c : SpeedOfLight}    {E₀ : EuclideanSpace ℝ (Fin d)} {B₀ : Fin d × Fin d → ℝ}    {B₀_antisymm : ∀ i j, B₀ (i, j) = - B₀ (j, i)} (t : Time) (x : Space d) (i j : Fin d) :    Space.deriv i ((constantEB c E₀ B₀ B₀_antisymm).vectorPotential c t · j) x =    (1 / 2) * B₀ (j, i) := by  rw [constantEB_vectorPotential]  rw [Space.deriv_eq]  rw [fderiv_const_mul (by fun_prop)]  rw [fderiv_fun_sum (by fun_prop)]  simp only [one_div, FunLike.coe_smul, FunLike.coe_sum, Pi.smul_apply,    Finset.sum_apply, smul_eq_mul, mul_eq_mul_left_iff, inv_eq_zero, OfNat.ofNat_ne_zero, or_false]  rw [Finset.sum_eq_single i]  · rw [fderiv_const_mul (by fun_prop)]    simp [← Space.deriv_eq]  · intro k _ hk    rw [fderiv_const_mul (by fun_prop)]    simp [← Space.deriv_eq]    rw [Space.deriv_component_diff]    simp only [or_true]    exact id (Ne.symm hk)  · simp