unfold explicitSymplecticEuler
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (explicitSymplecticEuler fun q p => T p + V q) = fun Δt qₙ pₙ =>
    solve q' p',
      q' = qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p ∧ p' = pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q p'
R : Type u_1
inst✝⁶ : RCLike R
X✝ : Type ?u.46671
inst✝⁵ : Vec R X✝
Y✝ : Type ?u.46685
inst✝⁴ : Vec R Y✝
Z✝ : Type ?u.46697
inst✝³ : Vec R Z✝
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.46721
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.46733
inst✝ : SemiInnerProductSpace R Z
T V : X → R
hT : HasAdjDiff R T
hV : HasAdjDiff R V
⊢ (fun Δt qₙ pₙ =>
      let p' := pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q pₙ;
      let q' := qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p;
      (q', p')) =
    fun Δt qₙ pₙ =>
    solve q' p',
      q' = qₙ + Δt • ∇ (p:=p'), (fun q p => T p + V q) qₙ p ∧ p' = pₙ - Δt • ∇ (q:=qₙ), (fun q p => T p + V q) q p'