Oracle Reduction completeness

@[simp]theorem oracleReduction_completeness --(h : init.neverFails)    (hRel : ∀ stmtIn oStmtIn witIn,      ((stmtIn, oStmtIn), witIn) ∈ relIn →      ((mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn), mapWit stmtIn witIn) ∈ relOut) :    (oracleReduction oSpec mapStmt mapWit embedIdx hEq).perfectCompleteness init impl      relIn relOut := by  simp only [OracleReduction.perfectCompleteness, Reduction.perfectCompleteness,    Reduction.completeness, ENNReal.coe_zero, tsub_zero]  intro ⟨stmtIn, oStmtIn⟩ witIn hIn  -- Reduce the run to a deterministic `pure` of the expected output.  have hrun : (oracleReduction oSpec mapStmt mapWit embedIdx hEq).toReduction.run      ⟨stmtIn, oStmtIn⟩ witIn =      (pure ((default,          ((mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn), mapWit stmtIn witIn)),          (mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn)) :        OptionT (OracleComp _) _) := by    simp only [oracleReduction, OracleReduction.toReduction, Reduction.run, oracleProver,      oracleVerifier, OracleVerifier.toVerifier, Prover.run, Verifier.run, Prover.runToRound]    rfl  rw [hrun]  rw [ge_iff_le, one_le_probEvent_iff, 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 _ hmem    change none ∈ support      (StateT.run' (simulateQ _ (pure (some ((default,        ((mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn), mapWit stmtIn witIn)),        (mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn))) : OracleComp _ _)) s) at hmem    rw [simulateQ_pure] at hmem    change none ∈ support      (Prod.fst <$> (pure (some ((default,        ((mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn), mapWit stmtIn witIn)),        (mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn))) :          StateT σ ProbComp _).run s) at hmem    rw [StateT.run_pure] at hmem    simp [map_pure] at hmem  · 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 _ (pure (some ((default,        ((mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn), mapWit stmtIn witIn)),        (mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn))) : OracleComp _ _)) s) at hx    rw [simulateQ_pure] at hx    change some x ∈ support      (Prod.fst <$> (pure (some ((default,        ((mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn), mapWit stmtIn witIn)),        (mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn))) :          StateT σ ProbComp _).run s) at hx    rw [StateT.run_pure] at hx    simp [map_pure, support_pure] at hx    cases hx    exact ⟨hRel stmtIn oStmtIn witIn hIn, rfl⟩