conv =>
  rhs
  solve_for p' from 1 := sorry_proof
  solve_as_inv
  solve_as_inv
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'
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ₙ =>
    let p'' := fun q' => Function.invFun (fun x => x - (pₙ - Δt • ∇ (q:=qₙ), (T x + V q))) 0;
    let q' := Function.invFun (fun x => x - (qₙ + Δt • ∇ (p:=p'' x), (T p + V qₙ))) 0;
    let p' := p'' q';
    (q', p')