Euler lagrange var Gradient

theorem euler_lagrange_varGradient    (L : Time → X → X → ℝ) (q : Time → X)    (hq : ContDiff ℝ ∞ q) (hL : ContDiff ℝ ∞ ↿L) :    (δ (q':=q), ∫ t, L t (q' t) (fderiv ℝ q' t 1)) = eulerLagrangeOp L q := by  simp only [eulerLagrangeOp_eq, Time.deriv_eq]  apply HasVarGradientAt.varGradient  apply HasVarGradientAt.intro _  · apply HasVarAdjDerivAt.comp      (F := fun (φ : Time → X × X) t => L t (φ t).fst (φ t).snd)      (G := fun (φ : Time → X) t => (φ t, fderiv ℝ φ t 1))    · apply HasVarAdjDerivAt.fmap (f := fun t => ↿(L t))      · fun_prop      · fun_prop      intro x u      apply DifferentiableAt.hasAdjFDerivAt      apply ContDiff.differentiable (n := ∞) (by fun_prop) (by simp)    · apply HasVarAdjDerivAt.prod (F:=fun φ => φ)      · apply HasVarAdjDerivAt.id _ hq      · apply HasVarAdjDerivAt.fderiv (hu := hq)  case hgrad =>    funext t    simp (disch := fun_prop) [sub_eq_add_neg]    congr    all_goals      try funext t      rw [gradient_eq_adjFDeriv, adjFDeriv_uncurry] <;>        apply ContDiff.differentiable (n := ∞) (by fun_prop) (by simp)