Field Strength Matrix bare Gradient inl inr

lemma fieldStrengthMatrix_bareGradient_inl_inr {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.fieldStrengthMatrix x (Sum.inl 0, Sum.inr i) = 2 := by  intro χ B  have hχ : ContDiff ℝ 2 χ := by    show ContDiff ℝ 2 (fun y : SpaceTime d => y (Sum.inl 0) * y (Sum.inr i))    fun_prop  have hB : Differentiable ℝ B := by    rw [← SpaceTime.differentiable_vector]; intro μ    exact SpaceTime.differentiable_deriv μ χ hχ  -- fieldStrengthMatrix (μ, ν) = η μ μ * ∂_ μ B x ν − η ν ν * ∂_ ν B x μ  rw [toFieldStrength_basis_repr_apply_eq_single]  -- Expand ∂_ μ B x ν as ∂_ μ (fun y => ∂_ ν χ y) x = ∂_ μ (∂_ ν χ) x  rw [SpaceTime.deriv_apply_eq (Sum.inl 0) (Sum.inr i) B hB,      SpaceTime.deriv_apply_eq (Sum.inr i) (Sum.inl 0) B hB]  -- Now compute the mixed partials of χ = t·xⁱ using fderiv_fun_mul + deriv_coord  -- ∂_t χ = xⁱ, ∂_{xⁱ} χ = t; so ∂_{xⁱ}(∂_t χ) = 1 and ∂_t(∂_{xⁱ} χ) = 1  have hfderiv : ∀ (y : SpaceTime d),      fderiv ℝ χ y = (y (Sum.inr i)) • Lorentz.Vector.coordCLM (Sum.inl 0) +                      (y (Sum.inl 0)) • Lorentz.Vector.coordCLM (Sum.inr i) := fun y => by    have h : fderiv ℝ (fun z : SpaceTime d => z (Sum.inl 0) * z (Sum.inr i)) y =        (y (Sum.inr i)) • Lorentz.Vector.coordCLM (Sum.inl 0) +        (y (Sum.inl 0)) • Lorentz.Vector.coordCLM (Sum.inr i) := by      have hmul := fderiv_fun_mul (𝕜 := ℝ)        (hc := (Lorentz.Vector.coordCLM (Sum.inl 0)).differentiableAt)        (hd := (Lorentz.Vector.coordCLM (Sum.inr i)).differentiableAt) (x := y)      simp only [ContinuousLinearMap.fderiv, Lorentz.Vector.coordCLM_apply] at hmul      -- hmul: fderiv ... y = y (Sum.inl 0) • coordCLM (Sum.inr i)      --                         + y (Sum.inr i) • coordCLM (Sum.inl 0)      -- goal: ... = y (Sum.inr i) • coordCLM (Sum.inl 0)      --               + y (Sum.inl 0) • coordCLM (Sum.inr i)      rw [hmul, add_comm]    exact h  simp only [SpaceTime.deriv_eq, B]  simp_rw [hfderiv]  simp only [_root_.add_apply, FunLike.coe_smul,    Pi.smul_apply, Lorentz.Vector.coordCLM_apply, smul_eq_mul, Lorentz.Vector.basis_apply]  simp only [mul_ite, mul_one, mul_zero, ite_add, zero_add, if_true]  simp only [minkowskiMatrix.inl_0_inl_0, minkowskiMatrix.inr_i_inr_i]  simp only [reduceCtorEq, ↓reduceIte, add_zero]  simp only [Lorentz.Vector.fderiv_coord, Lorentz.Vector.coordCLM_apply,    Lorentz.Vector.basis_apply, ↓reduceIte]  norm_num