Field Strength Matrix differentiable

lemma fieldStrengthMatrix_differentiable {d} {A : ElectromagneticPotential d}    {μν} (hA : ContDiff ℝ 2 A) :    Differentiable ℝ (A.fieldStrengthMatrix · μν) := by  have diff_partial (μ) :      ∀ ν, Differentiable ℝ fun x => (fderiv ℝ A x) (Lorentz.Vector.basis μ) ν := by    rw [SpaceTime.differentiable_vector]    exact Differentiable.clm_apply      (((contDiff_succ_iff_fderiv (n := 1)).mp hA).2.2.differentiable (by simp)) (by fun_prop)  conv => enter [2, x]; rw [toFieldStrength_basis_repr_apply_eq_single,    SpaceTime.deriv_eq, SpaceTime.deriv_eq]  exact ((diff_partial _ _).const_mul _).sub ((diff_partial _ _).const_mul _)