Theorem: SciLean.odeSolve.arg_x₀.semiAdjoint_rule (SciLean/Modules/DifferentialEquations/OdeSolve.lean)

State before:
R✝ : Type ?u.20793
inst✝⁶ : RCLike R✝
X✝ : Type ?u.20799
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.20845
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.20857
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf : ∀ (t : R), HasSemiAdjoint R (f t)
hx₀ : HasSemiAdjoint R x₀
⊢ (semiAdjoint R fun w => odeSolve f t₀ t (x₀ w)) = fun x₀' =>
    let f' := fun s y => -semiAdjoint R (f s) y;
    let y := odeSolve f' t t₀ x₀';
    semiAdjoint R x₀ y
Tactic:
sorry_proof
State after:
no goals