Sq prob Output map le observed Fork Pair

theorem sq_probOutput_map_le_observedForkPair [spec.DecidableEq] [IsUniformSpec spec]    (main : OracleComp spec α) (i : ι) (n : Nat) (observe : α → Option β) (value : β)    (hselect : OutputSelectsOccurrence main i n observe value) :    Pr[= value | observe <$> main] ^ 2 ≤      Pr[= (some (some value, some value) : Option (Option β × Option β)) |        observedForkPair main i n observe] := by  classical  letI : DecidableEq spec.Domain := inferInstance  letI (j : spec.Domain) : DecidableEq (spec.Range j) := inferInstance  set y : Option β := some value  let splitComp : OracleComp spec      {split : PFunctor.FreeM.Cursor.Split i main n // split.Valid} :=    Cursor.splitAtValid main i n  let finish : PFunctor.FreeM.Path main → OracleComp spec (Option β) :=    fun path => pure (observe (PFunctor.FreeM.output main path))  let kernel : {split : PFunctor.FreeM.Cursor.Split i main n // split.Valid} →      OracleComp spec (Option β) := fun certified =>    Cursor.complete certified.1 >>= finish  have hprogram : (observe <$> main : OracleComp spec (Option β)) = splitComp >>= kernel := by    simp only [splitComp, kernel]    rw [← bind_assoc, splitAtValid_bind_complete_oracleComp]    calc      observe <$> main = observe <$>          (PFunctor.FreeM.output main <$> Cursor.withPath main) := by        rw [Cursor.map_output_withPath]      _ = (observe ∘ PFunctor.FreeM.output main) <$>          Cursor.withPath main := by        simp only [Functor.map_map, Function.comp_def]      _ = Cursor.withPath main >>= finish := by        simp [finish, Function.comp_def]  rw [hprogram]  refine (sq_probOutput_bind_le_probOutput_bind_prod splitComp kernel y).trans_eq ?_  let observeView : PFunctor.FreeM.Cursor.ForkView i main n → Option β × Option β :=    fun view =>      (observe (PFunctor.FreeM.output main view.firstPath),        observe (PFunctor.FreeM.output main view.secondPath))  have hpair : observedForkPair main i n observe =      splitComp >>= fun certified => Option.map observeView <$>        Cursor.completeFork certified.1 := by    unfold observedForkPair    rw [← splitAtValid_bind_completeFork_oracleComp, map_bind]  rw [hpair, probOutput_bind_eq_tsum, probOutput_bind_eq_tsum]  refine tsum_congr fun certified => congrArg    (fun z => Pr[= certified | splitComp] * z) ?_  rcases certified with ⟨split, hvalid⟩  cases split with  | missing path => exact probOutput_pair_eq_observedForkPair_missing i n hvalid hselect  | found occurrence => exact probOutput_pair_eq_observedForkPair_found occurrence