Total Time Derivative euler Lagrange equivalenvce

lemma totalTimeDerivative_eulerLagrange_equivalenvce [CompleteSpace X] (L L' : Time → X → X → ℝ)    (htot : IsTotalTimeDerivative (L' - L)) (hContDiff : (ContDiff ℝ ∞ ↿L) ∨ (ContDiff ℝ ∞ ↿L'))    (q : Time → X) (hq : ContDiff ℝ ∞ q) : eulerLagrangeOp L q = eulerLagrangeOp L' q := by  rcases (isTotalTimeDerivative_explicit.mp htot) with ⟨F, hFContDiff, hEq⟩  have hContDiff_both :  (ContDiff ℝ ∞ ↿L) ∧ (ContDiff ℝ ∞ ↿L') := by    cases hContDiff with      | inl hL =>        constructor        · exact hL        · have h_triv : ↿L' =  ↿L + ↿(L' - L) := by            funext tqv            rcases tqv with ⟨t, q', v⟩            rw [Pi.add_apply]            change L' t q' v = L t q' v + (L' - L) t q' v            simp          have h_δL_contDiff := totalTimeDerivative_contDiff htot          rw [h_triv]          exact hL.add h_δL_contDiff      | inr hL' =>        constructor        · have h_triv : ↿L =  ↿L' + ↿(-(L' - L)) := by            funext tqv            rcases tqv with ⟨t, q', v⟩            rw [Pi.add_apply]            change L t q' v = L' t q' v + (- (L' - L)) t q' v            simp          have h_δL_contDiff := totalTimeDerivative_contDiff (isTotalTimeDerivative_neg htot)          rw [h_triv]          exact hL'.add h_δL_contDiff        · exact hL'  rw [← euler_lagrange_varGradient L q hq hContDiff_both.left]  rw [← euler_lagrange_varGradient L' q hq hContDiff_both.right]  apply Eq.symm  apply totalTimeDerivative_varGradient_equivalenvce  · exact htot  · exact hq