Mem of pure accepting

theorem mem_of_pure_accepting    (V : Verifier oSpec StmtIn StmtOut pSpec)    (stmt : StmtIn) (tr : pSpec.FullTranscript)    (lang : Set StmtOut) (out : StmtOut)    (hV : V.verify stmt tr = pure out)    (hAcc : Pr[ (· ∈ lang) |      OptionT.mk do (simulateQ impl (V.run stmt tr)).run' (← init)] = 1) :      out ∈ lang := by  rw [probEvent_eq_one_iff] at hAcc  obtain ⟨hFail, hmem⟩ := hAcc  -- The underlying probabilistic computation is `init >>= fun _ => pure (some out)`.  have hrun : (do (simulateQ impl (V.run stmt tr)).run' (← init) :      ProbComp (Option StmtOut)) = (init >>= fun _ => pure (some out)) := by    simp only [Verifier.run, hV]    congr 1  refine hmem out ?_  -- `init` has nonempty support, else the whole computation would fail with probability one.  have hne : (support init).Nonempty := by    by_contra hempty    rw [Set.not_nonempty_iff_eq_empty] at hempty    have hcfail : Pr[⊥ |        (init >>= fun _ => pure (some out) : ProbComp (Option StmtOut))] = 0 := by      have h2 := hFail      rw [OptionT.probFailure_eq, OptionT.run_mk, hrun] at h2      exact (add_eq_zero.mp h2).1    have hcsupp :        support (init >>= fun _ => pure (some out) : ProbComp (Option StmtOut)) = ∅ := by      rw [support_bind_const, support_pure]; simp [hempty]    rw [probFailure_eq_one hcsupp] at hcfail    exact one_ne_zero hcfail  rw [OptionT.mem_support_iff, OptionT.run_mk, hrun, support_bind_const, support_pure]  exact ⟨Set.mem_singleton _, hne⟩