Reduction support run pure verifier

lemma Reduction.support_run_pure_verifier    {StmtIn WitIn StmtOut WitOut : Type}    {n : ℕ} {pSpec : ProtocolSpec n}    (reduction : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec)    (f : StmtIn → FullTranscript pSpec → StmtOut)    (hf : ∀ stmt td,      reduction.verifier.verify stmt td =        (pure (f stmt td) : OptionT (OracleComp oSpec) StmtOut))    (stmt : StmtIn) (wit : WitIn)    {y : Option ((FullTranscript pSpec × StmtOut × WitOut) × StmtOut)}    (hy : y ∈ support (reduction.run stmt wit).run)    {td : FullTranscript pSpec} {prv : StmtOut × WitOut} {vOut : StmtOut}    (heq : y = some ((td, prv), vOut)) : vOut = f stmt td := by  rw [heq] at hy  unfold Reduction.run at hy  simp only [OptionT.run_bind, Option.elimM] at hy  rw [mem_support_bind_iff] at hy  obtain ⟨proverResultOpt, _hprover, hy⟩ := hy  cases proverResultOpt with  | none =>      exfalso      simp at hy  | some proverResult =>      simp only [Option.elim_some] at hy      rw [mem_support_bind_iff] at hy      obtain ⟨stmtOutOpt, hstmtOutOpt, hy⟩ := hy      simp only [ChallengeIdx, Challenge, Verifier.run, hf, OptionT.run_pure, liftM_pure,        support_pure, Set.mem_singleton_iff] at hstmtOutOpt      subst stmtOutOpt      simp only [Option.elim_some, Option.getM_some, OptionT.run_pure] at hy      injection hy with hpair      have htd : td = proverResult.1 := congrArg Prod.fst (congrArg Prod.fst hpair)      have hvOut : vOut = f stmt proverResult.1 := congrArg Prod.snd hpair      rw [htd]      exact hvOut