Exists agrees With Fn eval With Answer Fn eq iff mem support

theorem exists_agreesWithFn_evalWithAnswerFn_eq_iff_mem_support    [DecidableEq ι] [spec.Inhabited] [(t : spec.Domain) → SampleableType (spec.Range t)]    (oa : OracleComp spec α) (cache : spec.QueryCache) (a : α) :    (∃ f : QueryImpl spec Id, cache.AgreesWithFn f ∧ evalWithAnswerFn f oa = a)    ↔    (∃ cache' : spec.QueryCache,      (a, cache') ∈ support ((simulateQ randomOracle oa).run cache)) := by  classical  induction oa using OracleComp.inductionOn generalizing cache a with  | pure x =>    simp only [simulateQ_pure, StateT.run_pure, evalWithAnswerFn_pure, support_pure,      Set.mem_singleton_iff, Prod.mk.injEq]    refine ⟨fun ⟨_, _, h⟩ => ⟨cache, h.symm, rfl⟩, fun ⟨_, ha, _⟩ => ?_⟩    obtain ⟨f, hf⟩ := QueryCache.exists_agreesWithFn (spec := spec) cache    exact ⟨f, hf, ha.symm⟩  | query_bind t k ih =>    have h_eval : ∀ f : QueryImpl spec Id, evalWithAnswerFn f (liftM (spec.query t) >>= k)        = evalWithAnswerFn f (k (f t)) := fun f => by      rw [evalWithAnswerFn_bind,        show evalWithAnswerFn f (liftM (spec.query t)) = f t from simulateQ_spec_query f t]    simp_rw [h_eval]    rw [simulateQ_bind, simulateQ_spec_query, StateT.run_bind]    rcases hcache : cache t with _ | u    · simp only [support_randomOracle_run_bind_of_uncached t hcache, Set.mem_iUnion]      refine ⟨fun ⟨f, hf, ha⟩ => ?_, fun ⟨cache', u, hcache'⟩ => ?_⟩      · obtain ⟨cache', hcache'⟩ := (ih (f t) (cache.cacheQuery t (f t)) a).mp          ⟨f, (QueryCache.agreesWithFn_cacheQuery_iff cache t (f t) f hcache).mpr ⟨hf, rfl⟩, ha⟩        exact ⟨cache', f t, hcache'⟩      · obtain ⟨f, hagree, ha⟩ := (ih u (cache.cacheQuery t u) a).mpr ⟨cache', hcache'⟩        obtain ⟨hf, hfu⟩ := (QueryCache.agreesWithFn_cacheQuery_iff cache t u f hcache).mp hagree        exact ⟨f, hf, hfu ▸ ha⟩    · rw [QueryImpl.withCaching_run_some _ hcache, pure_bind]      refine ⟨fun ⟨f, hf, ha⟩ => (ih u cache a).mp ⟨f, hf, hf hcache ▸ ha⟩, fun hsupp => ?_⟩      obtain ⟨f, hf, ha⟩ := (ih u cache a).mpr hsupp      exact ⟨f, hf, hf hcache ▸ ha⟩