With Query Log self log eq

theorem withQueryLog_self_log_eq    {ι : Type} {spec : OracleSpec.{0, 0} ι} {α : Type}    (oa : OracleComp spec α) {v : α} {l₁ l₂ : spec.QueryLog}    (hmem : ((v, l₁), l₂) ∈ support oa.withQueryLog.withQueryLog) :    l₁ = l₂ := by  induction oa using OracleComp.inductionOn generalizing v l₁ l₂ with  | pure x =>      rw [withQueryLog_pure, withQueryLog_pure, mem_support_pure_iff] at hmem      grind  | query_bind t mx ih =>      -- `grind` is slow / crashes on the fully-unfolded support membership; the      -- staged destructuring below keeps the search space small.      rw [withQueryLog_bind, withQueryLog_bind, mem_support_bind_iff] at hmem      obtain ⟨⟨⟨u₁, log_q1⟩, log_q2⟩, h₁, hmem⟩ := hmem      rw [withQueryLog_query, withQueryLog_bind, mem_support_bind_iff] at h₁      obtain ⟨⟨u₂, log_qa⟩, h₁a, h₁b⟩ := h₁      simp only [withQueryLog_query, mem_support_bind_iff,        mem_support_pure_iff, Prod.mk.injEq] at h₁a      obtain ⟨u, _, rfl, rfl⟩ := h₁a      rw [support_map, Set.mem_image] at h₁b      obtain ⟨⟨⟨u', l_inner⟩, l_outer⟩, h_pure, h_eq_b⟩ := h₁b      simp only [withQueryLog_pure, mem_support_pure_iff, Prod.mk.injEq] at h_pure      obtain ⟨⟨rfl, rfl⟩, rfl⟩ := h_pure      simp only [Prod.map_apply, id_eq, Prod.mk.injEq, List.append_nil] at h_eq_b      obtain ⟨⟨rfl, rfl⟩, rfl⟩ := h_eq_b      rw [support_map, Set.mem_image] at hmem      obtain ⟨⟨⟨v', l₁'⟩, l₂'⟩, h_inner_outer, h_eq⟩ := hmem      simp only [Prod.map_apply, id_eq, Prod.mk.injEq] at h_eq      obtain ⟨⟨rfl, rfl⟩, rfl⟩ := h_eq      simp only [map_eq_pure_bind, withQueryLog_bind, mem_support_bind_iff] at h_inner_outer      obtain ⟨⟨⟨v', l₁'⟩, l₂'⟩, h_inner, ⟨pX, lX⟩, h_pX, h_eq_X⟩ := h_inner_outer      simp only [withQueryLog_pure, mem_support_pure_iff, Prod.map_apply, id_eq,        Prod.mk.injEq] at h_pX h_eq_X      obtain ⟨⟨rfl, rfl⟩, rfl⟩ := h_pX      obtain ⟨⟨rfl, rfl⟩, rfl⟩ := h_eq_X      simp [ih u' h_inner]