Kinetic Term add time mul const

lemma kineticTerm_add_time_mul_const {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)    (ha : Differentiable ℝ A)    (c : Lorentz.Vector d) (x : SpaceTime d) :    kineticTerm 𝓕 ⟨fun x => A x + x (Sum.inl 0) • c⟩ x = A.kineticTerm 𝓕 x +        (-1 / (2 * 𝓕.μ₀) * ∑ ν, ((2 * c ν * η ν ν * ∂_ (Sum.inl 0) A x ν + η ν ν * c ν ^ 2 -        2 * c ν * (∂_ ν A x (Sum.inl 0)))) + 1/(2 * 𝓕.μ₀) * c (Sum.inl 0) ^2) := by  have diff_a : ∂_ (Sum.inl 0) (fun x => A x + x (Sum.inl 0) • c) =      ∂_ (Sum.inl 0) A + (fun x => c) := by    funext x ν    rw [SpaceTime.deriv_eq, fderiv_fun_add ha.differentiableAt (by fun_prop),      fderiv_smul_const (by fun_prop)]    simp [Lorentz.Vector.coordCLM, SpaceTime.deriv_eq]  have diff_b (i : Fin d) : ∂_ (Sum.inr i) (fun x => A x + x (Sum.inl 0) • c) =      ∂_ (Sum.inr i) A := by    funext x ν    rw [SpaceTime.deriv_eq, fderiv_fun_add ha.differentiableAt (by fun_prop),      fderiv_smul_const (by fun_prop)]    simp [Lorentz.Vector.coordCLM, SpaceTime.deriv_eq]  have hdiff (μ ν : Fin 1 ⊕ Fin d) :      ∂_ μ (fun x => A x + x (Sum.inl 0) • c) x ν =      ∂_ μ A x ν + if μ = Sum.inl 0 then c ν else 0 := by    match μ with    | Sum.inl 0 => simp [diff_a]    | Sum.inr i => simp [diff_b i]  rw [kineticTerm_eq_sum_potential, kineticTerm_eq_sum_potential]  simp only [hdiff]  have key (μ ν : Fin 1 ⊕ Fin d) :      η μ μ * η ν ν * (∂_ μ A x ν + if μ = Sum.inl 0 then c ν else 0) ^ 2 -        (∂_ μ A x ν + if μ = Sum.inl 0 then c ν else 0) *          (∂_ ν A x μ + if ν = Sum.inl 0 then c μ else 0) =      (η μ μ * η ν ν * ∂_ μ A x ν ^ 2 - ∂_ μ A x ν * ∂_ ν A x μ) +        ((if μ = Sum.inl 0 then 2 * (c ν * η μ μ * η ν ν * ∂_ μ A x ν) +            η μ μ * η ν ν * c ν ^ 2 - c ν * ∂_ ν A x μ else 0) -          (if ν = Sum.inl 0 then c μ * ∂_ μ A x ν else 0) -          (if μ = Sum.inl 0 then c ν else 0) * (if ν = Sum.inl 0 then c μ else 0)) := by    split_ifs <;> ring  simp only [key]  simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib, Finset.sum_ite_irrel,    Finset.sum_const_zero, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, mul_ite, ite_mul,    mul_zero, zero_mul, inl_0_inl_0, one_mul, mul_one, two_mul, add_mul, mul_add]  ring