Eager Random Oracle eval Dist generate Seed bind

theorem eagerRandomOracle_evalDist_generateSeed_bind {ι₀ : Type} [DecidableEq ι₀]    {spec₀ : OracleSpec.{0, 0} ι₀}    [∀ t : spec₀.Domain, SampleableType (spec₀.Range t)]    [IsUniformSpec spec₀]    {α : Type} (oa : OracleComp spec₀ α) (qc : ι₀ → ℕ) (js : List ι₀) :    𝒟[do      let seed ← generateSeed spec₀ qc js      (simulateQ (eagerRandomOracle (spec := spec₀)) oa).run' seed] = 𝒟[oa] := by  classical  revert qc js  induction oa using OracleComp.inductionOn with  | pure a => intro qc js; apply evalDist_ext; intro; simp  | query_bind t f ih =>    intro qc js; apply evalDist_ext; intro x    have hsimQ : ∀ seed : QuerySeed spec₀,        (simulateQ eagerRandomOracle (liftM (query t) >>= f)).run' seed =        (eagerRandomOracle t >>= fun u => simulateQ eagerRandomOracle (f u)).run' seed :=      fun _ => by congr 1    simp_rw [hsimQ]    rw [probOutput_bind_eq_tsum (liftM (query t)) f x]    simp_rw [probOutput_query t]    rw [probOutput_bind_eq_tsum]    by_cases hcount : qc t * js.count t = 0    · exact eagerRandomOracle_evalDist_generateSeed_bind_step_zero t f qc js x ih hcount    · exact eagerRandomOracle_evalDist_generateSeed_bind_step_pos t f qc js x ih        (Nat.pos_of_ne_zero hcount)