Pure accepting of mem

theorem pure_accepting_of_mem    {n : ℕ} {pSpec : ProtocolSpec n} [∀ i, SampleableType (pSpec.Challenge i)]    (V : Verifier oSpec Stmt₁ Stmt₂ pSpec)    (stmt : Stmt₁) (tr : pSpec.FullTranscript)    (lang : Set Stmt₂) (out : Stmt₂)    (hV : V.verify stmt tr = pure out) (hout : out ∈ lang) :      Pr[(· ∈ lang) |        OptionT.mk do (simulateQ impl (V.run stmt tr)).run' (← init)] = 1 := by  simp only [Verifier.run, hV]  rw [probEvent_eq_one_iff]  refine ⟨?_, ?_⟩  · rw [OptionT.probFailure_eq, OptionT.run_mk]    simp only [probFailure_eq_zero, zero_add]    apply probOutput_eq_zero_of_not_mem_support    simp only [support_bind, Set.mem_iUnion, not_exists]    intro s _    change none ∈ support      (StateT.run' (simulateQ (r := StateT σ ProbComp) impl        (pure (some out) : OracleComp oSpec (Option Stmt₂))) s) → False    rw [simulateQ_pure]    change none ∈ support      (Prod.fst <$> (pure (some out) : StateT σ ProbComp (Option Stmt₂)).run s) → False    rw [StateT.run_pure]    simp [map_pure]  · intro x hx    rw [OptionT.mem_support_iff] at hx    simp only [OptionT.run_mk, support_bind, Set.mem_iUnion] at hx    obtain ⟨s, _, hx⟩ := hx    change some x ∈ support      (StateT.run' (simulateQ (r := StateT σ ProbComp) impl        (pure (some out) : OracleComp oSpec (Option Stmt₂))) s) at hx    rw [simulateQ_pure] at hx    change some x ∈ support      (Prod.fst <$> (pure (some out) : StateT σ ProbComp (Option Stmt₂)).run s) at hx    rw [StateT.run_pure] at hx    simp only [map_pure, support_pure, Set.mem_singleton_iff, Option.some.injEq] at hx    subst x    exact hout