Log entry in cache and mono

theorem log_entry_in_cache_and_mono {α : Type}    (oa : OracleComp spec α)    (cache₀ : QueryCache spec)    (z : (α × QueryLog spec) × QueryCache spec)    (hmem : z ∈ support ((simulateQ cachingOracle        ((simulateQ loggingOracle oa).run)).run cache₀)) :    (∀ entry ∈ z.1.2, z.2 entry.1 = some entry.2) ∧ cache₀ ≤ z.2 := by  induction oa using OracleComp.inductionOn generalizing cache₀ z with  | pure a =>    simp only [simulateQ_pure] at hmem    change z ∈ support (pure ((a, ([] : QueryLog spec)), cache₀)) at hmem    rw [support_pure, Set.mem_singleton_iff] at hmem    subst hmem    exact ⟨by simp, le_refl _⟩  | query_bind t mx ih =>    obtain ⟨u, cache_mid, ⟨⟨x', log'⟩, cache_final⟩,      hcache₀_le_mid, hcache_mid_entry, _, hmem_cont, rfl⟩ :=      exists_cont_of_run_simulateQ_query_bind t mx cache₀ z hmem    obtain ⟨ih_entries, ih_mono⟩ := ih u cache_mid ((x', log'), cache_final) hmem_cont    exact ⟨fun entry hentry => by      cases hentry with      | head => exact ih_mono hcache_mid_entry      | tail _ hentry' => exact ih_entries entry hentry',      le_trans hcache₀_le_mid ih_mono⟩