Oracle Reduction completeness

@[simp]theorem oracleReduction_completeness :    (oracleReduction oSpec OStatement).perfectCompleteness      init impl (relIn OStatement) (relOut OStatement) := by  simp only [OracleReduction.perfectCompleteness, oracleReduction, relIn, relOut]  simp only [Reduction.perfectCompleteness_eq_prob_one]  intro ⟨stmt, oStmt⟩ wit hOStmt  have hEq : oStmt 0 = oStmt 1 := hOStmt  simp only [OracleReduction.toReduction, Reduction.run,    Prover.run_of_verifier_first, oracleProver, oracleVerifier,    OracleVerifier.toVerifier, Verifier.run]  simp_rw [show (pure : _ → OptionT (OracleComp _) _) = fun x => (pure (some x) :    OracleComp _ _) from rfl]  simp only [← OracleComp.liftComp_eq_liftM, OracleComp.liftComp_pure,    pure_bind, bind_assoc]  erw [simulateQ_bind]  erw [simulateQ_bind]  simp only [QueryImpl.addLift_def, simulateQ_pure,    QueryImpl.simulateQ_add_liftComp_right, QueryImpl.simulateQ_add_liftComp_left,    simulateQ_query,    ← OracleComp.liftComp_eq_liftM, OracleComp.liftComp_pure,    pure_bind, bind_assoc, map_pure, monadLift_pure, monadLift_bind]  erw [simulateQ_bind]  simp only [QueryImpl.addLift_def, simulateQ_pure,    QueryImpl.simulateQ_add_liftComp_right, QueryImpl.simulateQ_add_liftComp_left,    simulateQ_query,    ← OracleComp.liftComp_eq_liftM, OracleComp.liftComp_pure,    pure_bind, bind_assoc, map_pure, monadLift_pure, monadLift_bind,    OptionT.run_mk, OptionT.run_pure, OptionT.run_bind, OptionT.run,    Option.getM, Option.bind_some, Option.elimM,    FullTranscript.challenges, FullTranscript.messages, ChallengeIdx, Challenge,    hEq]  erw [simulateQ_query]  simp only [StmtOut, OStmtOut, WitOut, Fin.isValue, Fin.vcons_of_one, ChallengeIdx,    Challenge, ofPFunctor_toPFunctor, QueryImpl.liftTarget_self, MessageIdx, OStmtIn,    Message, bind_map_left, StateT.run'_eq, StateT.run_bind, map_bind, OptionT.mk_bind,    Set.mem_setOf_eq, probEvent_eq_one_iff, probFailure_bind_eq_zero_iff,    OptionT.probFailure_liftM, probFailure_eq_zero, OptionT.support_liftM,    Prod.forall, true_and, support_bind, Set.mem_iUnion, OptionT.mem_support_iff,    OptionT.run_mk, support_map, Set.mem_image, Prod.exists, exists_and_right,    exists_eq_right, exists_prop, forall_exists_index, and_imp, Prod.mk.injEq]  constructor <;> intro <;> intro <;> intro <;> intro  all_goals try erw [simulateQ_bind]  all_goals simp only [MonadLift.monadLift, liftM, monadLift, MonadLiftT.monadLift]  all_goals simp only [OracleComp.liftComp_pure, QueryImpl.simulateQ_add_liftComp_left,    simulateQ_pure, simulateQ_id', pure_bind, bind_assoc, map_pure, monadLift_pure,    OptionT.run_mk, OptionT.run_pure, OptionT.run_bind, OptionT.run,    StateT.run'_eq, probFailure_eq_zero, hEq,    support_pure, Set.mem_singleton_iff, Prod.eq_iff_fst_eq_snd_eq]  all_goals try erw [simulateQ_pure]  all_goals try simp_all only [simulateQ_pure, pure_bind, map_pure,    OptionT.run_mk, OptionT.run_pure, OptionT.run_bind, OptionT.run,    StateT.run'_eq, StateT.run_pure, probFailure_eq_zero,    support_pure, support_map, Set.mem_singleton_iff, Set.mem_image,    OptionT.probFailure_eq, probOutput_pure, hEq]  · rw [show OptionT.mk = id from rfl]    simp only [ChallengeIdx, Fin.vcons_of_one, Challenge, Fin.isValue, input_query,      cont_query, input_apply, id_eq, zero_add, probOutput_eq_zero_iff, support_map,      Set.mem_image, Prod.exists, exists_and_right, exists_eq_right, not_exists]    intro    erw [simulateQ_pure]    simp [support_pure, pure_bind]  · intro a b x hx x_1 hx1 x_2 x_3    erw [simulateQ_bind]    simp only [liftComp_eq_liftM, pure_bind, simulateQ_pure, OptionT.lift,      OptionT.run_mk, map_pure]    erw [simulateQ_pure]    simp only [pure_bind, simulateQ_pure, support_pure, StateT.run, StateT.run',      Set.mem_singleton_iff, Prod.mk.injEq]    rintro ⟨⟨rfl, rfl⟩, rfl⟩    refine ⟨?_, rfl, ?_⟩ <;> congr 1