Prob Output context Fork View Collision le collision

theorem probOutput_contextForkViewCollision_le_collision [IsUniformSpec spec]    (main : OracleComp spec α) (qb : ι → ℕ) (i : ι)    (cf : α → Option (Fin (qb i + 1))) (s : Fin (qb i + 1)) :    Pr[= (some s : Option (Fin (qb i + 1))) |        contextForkViewCollision main qb i cf s] ≤      Pr[= (some s : Option (Fin (qb i + 1))) |        contextForkCollision main qb i cf s] := by  let paths : OracleComp spec (PFunctor.FreeM.Path main) := PFunctor.FreeM.withPath main  let viewCollision : PFunctor.FreeM.Path main →      OracleComp spec (Option (Fin (qb i + 1))) := fun path =>    match PFunctor.FreeM.Cursor.locateAt? (P := spec.toPFunctor) i main path s with    | none => pure none    | some located =>        PFunctor.FreeM.bind          (PFunctor.FreeM.lift (P := spec.toPFunctor) i) fun secondAnswer =>            (fun secondSuffix =>              collideForkView main qb i cf s (some {                occurrence := located.occurrence                first := located.completion                second := ⟨secondAnswer, secondSuffix⟩ })) <$>              PFunctor.FreeM.withPath (located.occurrence.resume secondAnswer)  let answerCollision : PFunctor.FreeM.Path main →      OracleComp spec (Option (Fin (qb i + 1))) := fun path =>    match PFunctor.FreeM.Cursor.locateAt? (P := spec.toPFunctor) i main path s with    | none => pure none    | some located => do        let secondAnswer ← spec.query i        if located.completion.answer = secondAnswer ∧            cf (PFunctor.FreeM.output main path) = some s then          pure (some s)        else pure none  have hsource : contextForkViewCollision main qb i cf s =      paths >>= viewCollision := by    letI : spec.toPFunctor.DecidableEq :=      (inferInstance : spec.DecidableEq).toDecidableEq    unfold contextForkViewCollision contextForkView    rw [PFunctor.FreeM.Cursor.map_locateAndForkAt]    apply congrArg (fun k => paths >>= k)    funext path    simp only [viewCollision]    rcases PFunctor.FreeM.Cursor.locateAt?        (P := spec.toPFunctor) i main path s with _ | located    · rfl    · simp [PFunctor.FreeM.Cursor.Located.fork]  have hinner : ∀ path : PFunctor.FreeM.Path main,      Pr[= (some s : Option (Fin (qb i + 1))) | viewCollision path] ≤        Pr[= (some s : Option (Fin (qb i + 1))) | answerCollision path] := by    intro path    simp only [viewCollision, answerCollision]    rcases hlocated : PFunctor.FreeM.Cursor.locateAt?        (P := spec.toPFunctor) i main path s with _ | located    · simp    · let continuation : spec.Range i →          OracleComp spec (Option (Fin (qb i + 1))) := fun secondAnswer =>        (fun secondSuffix =>          collideForkView main qb i cf s (some {            occurrence := located.occurrence            first := located.completion            second := ⟨secondAnswer, secondSuffix⟩ })) <$>          PFunctor.FreeM.withPath (located.occurrence.resume secondAnswer)      change Pr[= (some s : Option (Fin (qb i + 1))) |          OracleComp.lift (spec.query i) >>= continuation] ≤ _      rw [probOutput_bind_eq_tsum, probOutput_bind_eq_tsum]      refine ENNReal.tsum_le_tsum fun secondAnswer => ?_      let firstAnswer : spec.Range i := located.completion.answer      by_cases heq : firstAnswer = secondAnswer      · by_cases hcf : cf (PFunctor.FreeM.output main path) = some s        · simp [continuation, firstAnswer, heq, hcf, collideForkView,            probOutput_query]        · have hfirst : cf (PFunctor.FreeM.output main located.completion.path) ≠              some s := by rw [located.path_eq]; exact hcf          simp [continuation, firstAnswer, heq, hcf, hfirst, collideForkView,            PFunctor.FreeM.Cursor.ForkView.firstPath, probOutput_query]      · simp [continuation, firstAnswer, heq, collideForkView,          PFunctor.FreeM.Cursor.ForkView.firstAnswer,          PFunctor.FreeM.Cursor.ForkView.secondAnswer, probOutput_query]  calc    Pr[= (some s : Option (Fin (qb i + 1))) |        contextForkViewCollision main qb i cf s]        = ∑' path, Pr[= path | paths] *            Pr[= (some s : Option (Fin (qb i + 1))) | viewCollision path] := by          rw [hsource, probOutput_bind_eq_tsum]    _ ≤ ∑' path, Pr[= path | paths] *          Pr[= (some s : Option (Fin (qb i + 1))) | answerCollision path] :=      ENNReal.tsum_le_tsum fun path => mul_le_mul' le_rfl (hinner path)    _ = Pr[= (some s : Option (Fin (qb i + 1))) |          contextForkCollision main qb i cf s] := by        simp only [contextForkCollision, paths, answerCollision]        rw [probOutput_bind_eq_tsum]        rfl