Total Time Derivative var Gradient equivalenvce

lemma totalTimeDerivative_varGradient_equivalenvce [CompleteSpace X] (L L' : Time → X → X → ℝ)    (htot : IsTotalTimeDerivative (L' - L))    (q : Time → X) (hq : ContDiff ℝ ∞ q):    (δ (q':=q), ∫ t, L' t (q' t) (fderiv ℝ q' t 1)) =       (δ (q':=q), ∫ t, L t (q' t) (fderiv ℝ q' t 1)) := by  let δL := (fun t q v => L' t q v - L t q v)  by_cases hL : ∃ grad, HasVarGradientAt (fun q' t => L t (q' t) (fderiv ℝ q' t 1)) grad q  · apply HasVarGradientAt.varGradient    have h_triv : L' = L + (L' - L) := by module    rw [h_triv]    apply totalTimeDerivative_hasVarGradientAt_equivalence    · exact htot    · exact hq    · rcases hL with ⟨grad, hgrad⟩      rw [ HasVarGradientAt.varGradient (fun q' t => L t (q' t) (fderiv ℝ  q' t 1)) grad q hgrad]      exact hgrad  · by_cases hL' : ∃ grad, HasVarGradientAt (fun q' t => L' t (q' t) (fderiv ℝ q' t 1)) grad q    · apply Eq.symm      apply HasVarGradientAt.varGradient      have h_triv : L = L' +(-(L' - L)) := by module      rw [h_triv]      apply totalTimeDerivative_hasVarGradientAt_equivalence      · apply isTotalTimeDerivative_neg        exact htot      · exact hq      · rcases hL' with ⟨grad, hgrad⟩        rw [HasVarGradientAt.varGradient (fun q' t => L' t (q' t) (fderiv ℝ  q' t 1)) grad q hgrad]        exact hgrad    · unfold varGradient      simp only [hL, hL', ↓reduceDIte]