Query Log length le of nma Hash Query Bound

theorem queryLog_length_le_of_nmaHashQueryBound    [DecidableEq M] [DecidableEq Commit] [SampleableType Chal] {α : Type}    {oa : OracleComp (unifSpec + (M × Commit →ₒ Chal)) α} {Q : ℕ}    (hQ : nmaHashQueryBound (M := M) (Commit := Commit) (Chal := Chal) (oa := oa) Q)    (st : SimState M Commit Chal) {z : α × SimState M Commit Chal}    (hz : z ∈ support ((simulateQ (unifForward M Commit Chal + roImpl M Commit Chal) oa).run st)) :    z.2.2.length ≤ st.2.length + Q := by  induction oa using OracleComp.inductionOn generalizing Q st z with  | pure x =>      obtain rfl : z = (x, st) := by        simpa [simulateQ_pure, StateT.run_pure, support_pure] using hz      simp  | query_bind t mx ih =>      rw [nmaHashQueryBound_query_bind_iff (M := M) (Commit := Commit) (Chal := Chal)] at hQ      rw [simulateQ_query_bind, StateT.run_bind, support_bind] at hz      simp only [Set.mem_iUnion] at hz      obtain ⟨us, hus, hz'⟩ := hz      cases t with      | inl n =>          rcases st with ⟨cache, log⟩          obtain ⟨u, rfl⟩ : us ∈ Set.range (fun u => (u, cache, log)) := by            simpa [QueryImpl.add_apply_inl, unifForward, support_map] using hus          simpa using ih u (hQ.2 u) (cache, log) hz'      | inr mc =>          rcases st with ⟨cache, log⟩          cases hcache : cache mc with          | some v =>              have hus' : us ∈ ({(v, cache, log)} : Set _) := by                convert hus using 1 <;>                  simp [QueryImpl.add_apply_inr, roImpl, StateT.run_bind, StateT.run_get,                    hcache, support_pure]              obtain rfl := Set.mem_singleton_iff.mp hus'              have hrec : z.2.2.length ≤ log.length + (Q - 1) := by                simpa using ih v (hQ.2 v) (cache, log) hz'              exact le_trans hrec (Nat.add_le_add_left (Nat.sub_le _ _) _)          | none =>              obtain ⟨u, rfl⟩ : us ∈ Set.range (fun u : Chal =>                  (u, cache.cacheQuery mc u, log ++ [mc])) := by                convert hus using 1 <;>                  simp [QueryImpl.add_apply_inr, roImpl, StateT.run_bind, StateT.run_get,                    hcache, StateT.run_set, support_map]              have hrec : z.2.2.length ≤ (log ++ [mc]).length + (Q - 1) := by                simpa using                  ih u (hQ.2 u)                    ((cache.cacheQuery mc u : (M × Commit →ₒ Chal).QueryCache), log ++ [mc]) hz'              have hQpos : 0 < Q := hQ.1              simp only [List.length_append, List.length_singleton] at hrec ⊢              lia