Prob Event guarded Context Fork eq context Fork component

theorem probEvent_guardedContextFork_eq_contextFork_component    [IsProbabilitySpec spec]    (main : OracleComp spec α) (qb : ι → ℕ) (i : ι)    (cf : α → Option (Fin (qb i + 1))) (s : Fin (qb i + 1)) :    Pr[fun result : Option (α × α) => result.isSome |        guardedContextFork main qb i cf s] =      Pr[fun result : Option (α × α) =>          result.map (cf ∘ Prod.fst) = some (some s) |        contextFork main qb i cf] := by  letI : spec.toPFunctor.DecidableEq :=    (inferInstance : spec.DecidableEq).toDecidableEq  rw [contextFork_eq_contextForkByClassify]  unfold guardedContextFork contextForkByClassify  rw [PFunctor.FreeM.Cursor.filterMapLocateAndForkAt_eq_bind_complete,    PFunctor.FreeM.Cursor.filterMapLocateAndForkBy_eq_bind_complete,    probEvent_ofFreeM_bind_eq_tsum, probEvent_ofFreeM_bind_eq_tsum]  refine tsum_congr fun path => ?_  congr 1  rcases hcf : cf (PFunctor.FreeM.output main path) with _ | t  · rcases hloc : PFunctor.FreeM.Cursor.locateAt?        (P := spec.toPFunctor) i main path s with _ | located    · rw [probEvent_ofFreeM_pure, probEvent_ofFreeM_pure]      simp    · have hfirst :          cf (PFunctor.FreeM.output main located.completion.path) = none := by        simpa only [located.path_eq] using hcf      rw [probEvent_classifyForkView_isSome_eq_zero_of_first_ne          main qb i cf s located (by simp [hfirst]),        probEvent_ofFreeM_pure]      simp  · by_cases hts : t = s    · subst t      rcases hloc : PFunctor.FreeM.Cursor.locateAt?          (P := spec.toPFunctor) i main path s with _ | located      · simp only [hloc]        rw [probEvent_ofFreeM_pure, probEvent_ofFreeM_pure]        simp      · simp only [hloc]        rw [probEvent_ofFreeM_map, probEvent_ofFreeM_map]        congr 1        funext second        exact propext (classifyForkView_component_iff main qb i cf s {            occurrence := located.occurrence            first := located.completion            second := second }).symm    · trans (0 : ℝ≥0∞)      · rcases hlocFixed : PFunctor.FreeM.Cursor.locateAt?            (P := spec.toPFunctor) i main path s with _ | locatedFixed        · rw [probEvent_ofFreeM_pure]          simp        · dsimp only          have hfirstNe :              cf (PFunctor.FreeM.output main locatedFixed.completion.path) ≠ some s := by            simp only [locatedFixed.path_eq, hcf]            grind          rw [probEvent_classifyForkView_isSome_eq_zero_of_first_ne            main qb i cf s locatedFixed hfirstNe]      · dsimp only        rcases hlocDynamic : PFunctor.FreeM.Cursor.locateAt?            (P := spec.toPFunctor) i main path t with _ | locatedDynamic        · rw [probEvent_ofFreeM_pure]          simp        · rw [probEvent_classifyForkView_component_eq_zero_of_ne            main qb i cf t s locatedDynamic hts]