To Field Strength bare Gradient ne zero

lemma toFieldStrength_bareGradient_ne_zero {d : ℕ} (i : Fin d)    (x : SpaceTime d) :    let χ : SpaceTime d → ℝ := fun y => y (Sum.inl 0) * y (Sum.inr i)    let B : ElectromagneticPotential d := ⟨fun y μ => ∂_ μ χ y⟩    B.toFieldStrength x ≠ 0 := by  intro χ B h  have h2 := fieldStrengthMatrix_bareGradient_inl_inr i x  dsimp only at h2  rw [fieldStrengthMatrix_eq, h] at h2  have h3 : ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr      (0 : Lorentz.CoVector d ⊗[ℝ] Lorentz.Vector d)) = 0 := map_zero _  erw [h3, Finsupp.zero_apply] at h2  norm_num at h2