simp
case h
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
w : W
⊢ (odeSolve f t₀ t (x₀ w),
      semiAdjoint R fun dw =>
        (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
            (∂> (w:=w;dw), x₀ w)).2) =
    (odeSolve f t₀ t (x₀ w), fun dx =>
      semiAdjoint R (∂ x₀ w)
        (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx))
case h
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
w : W
⊢ (semiAdjoint R fun dw =>
      (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
          (∂> (w:=w;dw), x₀ w)).2) =
    fun dx =>
    semiAdjoint R (∂ x₀ w) (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx)