To Field Strength of Gradient

lemma toFieldStrength_ofGradient {d} {χ : SpaceTime d → ℝ} (hχ : ContDiff ℝ 2 χ)    (x : SpaceTime d) : (ofGradient χ).toFieldStrength x = 0 := by  apply (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr.injective  apply Finsupp.ext  intro μν  simp only [toFieldStrength_basis_repr_apply_eq_single]  rw [SpaceTime.deriv_apply_eq μν.1 μν.2 (ofGradient χ) (differentiable_ofGradient hχ),    SpaceTime.deriv_apply_eq μν.2 μν.1 (ofGradient χ) (differentiable_ofGradient hχ)]  simp only [ofGradient_apply]  rw [fderiv_const_mul (SpaceTime.differentiable_deriv μν.1 χ hχ).differentiableAt,    fderiv_const_mul (SpaceTime.differentiable_deriv μν.2 χ hχ).differentiableAt]  simp only [FunLike.coe_smul, Pi.smul_apply, smul_eq_mul]  -- simplify repr 0 to 0  conv_rhs => rw [show (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr      (0 : Lorentz.Vector d ⊗[ℝ] Lorentz.Vector d) = 0 from map_zero _]  simp only [Finsupp.zero_apply]  -- use Clairaut: ∂_ μ (∂_ ν χ) x = ∂_ ν (∂_ μ χ) x, so the two terms cancel  have heq : fderiv ℝ (∂_ μν.2 χ) x (Lorentz.Vector.basis μν.1) =      fderiv ℝ (∂_ μν.1 χ) x (Lorentz.Vector.basis μν.2) := by    change ∂_ μν.1 (∂_ μν.2 χ) x = ∂_ μν.2 (∂_ μν.1 χ) x    rw [← SpaceTime.deriv_commute μν.2 μν.1 χ hχ]  rw [heq]  ring