Fs Abort Sign Loop cache invariant

lemma fsAbortSignLoop_cache_invariant    (ro : QueryImpl (M × Commit →ₒ Chal)      (StateT ((M × Commit →ₒ Chal).QueryCache) ProbComp))    (hro : ro = randomOracle)    (hc : ids.Complete) {pk : Stmt} {sk : Wit} (hrel : rel pk sk = true)    (msg : M) (n : ℕ) (s₀ : (M × Commit →ₒ Chal).QueryCache)    (w : Commit) (z : Resp) (s : (M × Commit →ₒ Chal).QueryCache)    (hsup : (some (w, z), s) ∈ support      ((simulateQ (unifFwdImpl (M × Commit →ₒ Chal) + ro)        (fsAbortSignLoop ids M pk sk msg n)).run s₀)) :    ∃ c : Chal, s (msg, w) = some c ∧ ids.verify pk w c z = true := by  subst hro  set impl := unifFwdImpl (M × Commit →ₒ Chal) +    (randomOracle : QueryImpl (M × Commit →ₒ Chal) _)  have hSimQuery : ∀ (q : M × Commit),      simulateQ impl (HasQuery.query q) =        (randomOracle : QueryImpl (M × Commit →ₒ Chal) _) q :=    roSim.simulateQ_HasQuery_query _  induction n generalizing s₀ with  | zero =>    simp [fsAbortSignLoop, simulateQ_pure, StateT.run_pure, support_pure] at hsup  | succ n ih =>    simp only [fsAbortSignLoop, simulateQ_bind] at hsup    rw [StateT.run_bind] at hsup    obtain ⟨⟨⟨w_a, oz⟩, s₁⟩, h_attempt, h_rest⟩ :=      (mem_support_bind_iff _ _ _).mp hsup    cases oz with    | none => exact ih s₁ (by simpa using h_rest)    | some z_a =>      obtain ⟨⟨rfl, rfl⟩, rfl⟩ : (some (w, z), s) = (some (w_a, z_a), s₁) := by simpa using h_rest      simp only [fsAbortSignAttempt, simulateQ_bind, hSimQuery, simulateQ_pure,        StateT.run_bind, mem_support_bind_iff, StateT.run_pure, support_pure,        Set.mem_singleton_iff, Prod.mk.injEq] at h_attempt      obtain ⟨⟨⟨w_cm, st⟩, s_cm⟩, h_commit, ⟨c_q, s_ro⟩, h_query,        ⟨oz_r, s_resp⟩, h_respond, ⟨rfl, rfl⟩, rfl⟩ := h_attempt      change _ ∈ support ((simulateQ impl (liftM (ids.commit pk sk))).run s₀) at h_commit      rw [roSim.run_liftM, support_map] at h_commit      obtain ⟨⟨w_c, st_c⟩, h_cm_mem, h_cm_eq⟩ := h_commit      simp only [Prod.mk.injEq] at h_cm_eq      obtain ⟨⟨rfl, rfl⟩, rfl⟩ := h_cm_eq      change _ ∈ support ((simulateQ impl        (liftM (ids.respond pk sk st_c c_q))).run s_ro) at h_respond      rw [roSim.run_liftM, support_map] at h_respond      obtain ⟨_, h_rsp_mem, rfl, rfl⟩ := h_respond      refine ⟨c_q, ?_, ?_⟩      · simp only [randomOracle, QueryImpl.withCaching_apply,          StateT.run_bind, StateT.run_get, pure_bind] at h_query        cases hs : s₀ (msg, w_c) with        | some c_cached =>          simp only [hs, StateT.run_pure, support_pure,            Set.mem_singleton_iff, Prod.mk.injEq] at h_query          rw [h_query.2, hs, h_query.1]        | none =>          simp only [hs, StateT.run_bind, mem_support_bind_iff, StateT.run_modifyGet,            support_pure, Set.mem_singleton_iff, Prod.mk.injEq] at h_query          obtain ⟨x, -, rfl, rfl⟩ := h_query          exact QueryCache.cacheQuery_self _ (msg, w_c) x.1      · apply ids.verify_of_complete hc hrel        rw [IdenSchemeWithAbort.honestExecution, support_bind]        refine Set.mem_iUnion₂.mpr ⟨(w_c, st_c), h_cm_mem, ?_⟩        rw [support_bind]        refine Set.mem_iUnion₂.mpr ⟨c_q, mem_support_uniformSample _, ?_⟩        simp only [support_bind, Set.mem_iUnion₂,          support_pure, Set.mem_singleton_iff]        exact ⟨some z, h_rsp_mem, by simp [Option.map]⟩