You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
inductive FreeMonad (f : Type u → Type v) (α : Type w) : Type (max (u + 1) v w)
  | protected pure (x : α) : FreeMonad f α
  | roll {β : Type u} (x : f β) (r : β → FreeMonad f α) : FreeMonad f α

@[elab_as_elim]
protected def inductionOn {C : FreeMonad f α → Prop}
    (pure : ∀ x, C (pure x))
    (roll : ∀ {β} (x : f β), (r : β → FreeMonad f α) →
      (∀ y, C (r y)) → C (x >>= r)) :
    (oa : FreeMonad f α) → C oa
  | FreeMonad.pure x => pure x
  | FreeMonad.roll x r => roll x _ (λ u ↦
      FreeMonad.inductionOn pure roll (r u))

@[elab_as_elim]
protected def construct {C : FreeMonad f α → Type*}
    (pure : (x : α) → C (pure x))
    (roll : {β : Type u} → (x : f β) → (r : β → FreeMonad f α) →
      ((y : β) → C (r y)) → C (x >>= r)) :
    (oa : FreeMonad f α) → C oa
  | .pure x => pure x
  | .roll x r => roll x _ (λ u ↦ FreeMonad.construct pure roll (r u))

def supportWhen (oa : OracleComp spec α)
    (possible_outputs : {α : Type v} → OracleQuery spec α → Set α) : Set α :=

inductive OracleQuery {ι : Type u} (spec : OracleSpec.{u,v} ι) : Type v → Type (max u v)
  | query (i : ι) (t : spec.domain i) : OracleQuery spec (spec.range i)

def OracleComp {ι : Type u} (spec : OracleSpec.{u,v} ι) :
    Type w → Type (max u (v + 1) w) :=
  OptionT (FreeMonad (OracleQuery.{u,v} spec))

@[elab_as_elim]
protected def inductionOn {C : OracleComp spec α → Prop}
    (pure : (a : α) → C (pure a))
    (query_bind : (i : ι) → (t : spec.domain i) →
      (oa : spec.range i → OracleComp spec α) → (∀ u, C (oa u)) → C (query i t >>= oa))
    (failure : C failure) (oa : OracleComp spec α) : C oa :=
  FreeMonad.inductionOn (Option.rec failure pure) (λ (query i t) ↦ query_bind i t) oa

@[elab_as_elim]
protected def induction {C : OracleComp spec α → Prop}
    (oa : OracleComp spec α) (pure : (a : α) → C (pure a))
    (query_bind : (i : ι) → (t : spec.domain i) →
      (oa : spec.range i → OracleComp spec α) → (∀ u, C (oa u)) → C (query i t >>= oa))
    (failure : C failure) : C oa :=
  FreeMonad.inductionOn (Option.rec failure pure) (λ (query i t) ↦ query_bind i t) oa

@[elab_as_elim]
protected def construct {C : OracleComp spec α → Type*}
    (pure : (a : α) → C (pure a))
    (query_bind : {β : Type v} → (q : OracleQuery spec β) →
      (oa : β → OracleComp spec α) → ((u : β) → C (oa u)) → C (q >>= oa))
    (failure : C failure) (oa : OracleComp spec α) : C oa :=
  FreeMonad.construct (Option.rec failure pure) query_bind oa

def OracleSpec (ι : Type u) : Type (max u (v + 1)) :=
  (i : ι) → Type v × Type v

@[inline, reducible]
protected def domain (spec : OracleSpec ι) (i : ι) : Type v := (spec i).1

@[inline, reducible]
protected def range (spec : OracleSpec ι) (i : ι) : Type w := (spec i).2

@[simp]
def map (f : α → β) (z : Zipper α) : Zipper β :=
  ⟨ List.map f z.left, f z.focus, List.map f z.right ⟩

@[inline] def lift [Bind m] {α : Type u} (x : m α) : FreeContT f m α :=
  fun _ handlePure => x >>= handlePure

def generate_franking_tag (nonce : BitVec 256) (msg : String) : FrankingTag :=
  let (msg_bv, _) := serialize_message_data msg nonce
  let tf := mock_hmac_sha256 nonce msg_bv 
  { tag := tf }

@[trans]
def trans {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    (e₁ : P ≃ₗ Q) (e₂ : Q ≃ₗ R) : P ≃ₗ R :=
  ⟨e₂.toLens ∘ₗ e₁.toLens, e₁.invLens ∘ₗ e₂.invLens,
    by admit /- proof elided -/
      ⟩

ExceptT.mk in Init.Control.Except

LE.le in Init.Prelude

@[inline, reducible] def unifSpec : OracleSpec.{0,0} ℕ :=
  λ n ↦ (Unit, Fin (n + 1))

def tildeR {P : PFunctor.{uA, uB}} : Lens P (P ◃ X) :=
  (fun a => ⟨a, fun _ => PUnit.unit⟩) ⇆ (fun _a => fun ⟨b, _⟩ => b)

BitVec.ofFin in Init.Prelude

Set.indicator in Mathlib.Algebra.Notation.Indicator

Unit in Init.Prelude

local instance instPreorderProp : Preorder Prop where
  le := fun p q => p → q
  le_refl := fun p => id
  le_trans := fun p q r h1 h2 => h2 ∘ h1

MonadState in Init.Prelude

ENat in Mathlib.Data.ENat.Defs

instance : coinSpec.DecidableEq where
  domain_decidableEq' := inferInstance
  range_decidableEq' := inferInstance

def piPUnit (P : PFunctor.{uA, uB}) :
    pi (fun (_ : PUnit) => P) ≃ₚ P where
  equivA := sorry
  equivB := sorry

instance {m} [Monad m] [Commutative m] {α β} (ma : m α) (mb : m β) :
    CommutativeAt m ma mb := bind_comm ma mb

instance : LawfulMonad (FreeM P) :=
  LawfulMonad.mk' (FreeM P)
    (λ x ↦ by admit /- proof elided -/
      )
    (λ x f ↦ rfl)
    (λ x f g ↦ by admit /- proof elided -/
      )

def LWE_Game_1 (adv : LWE_Adversary n m p) : ProbComp Bool := do
  let distr ← LWE_Uniform_Distr n m p
  let b ← adv distr
  return b

instance {β} : Unique (A (purePower β)) := inferInstanceAs (Unique PUnit)

structure ReportingTag where
  tag : mock_hmac_sha256_out_type 
  deriving Repr

def terminal {P : PFunctor.{uA, uB}} : Lens P 1 :=
  (fun _ => PUnit.unit) ⇆ (fun _ => PEmpty.elim)

instance : MonadFunctor f (FreeMonad f) where
  monadMap g
    | FreeMonad.pure x => FreeMonad.pure x
    | FreeMonad.roll x r => g x >>= r

List.range in Init.Data.List.Basic

instance {P : PreCondition σ} {s' : σ} :
  StrongestPostcondition P (set s' : StateM σ Unit) := default

instance instLawfulComonad [Comonad w] [LawfulComonad w] : LawfulComonad (StoreT s w) where
  map_eq_extend_extract := sorry 
  extend_extract := sorry 
  extract_extend := by admit /- proof elided -/

ExceptT in Init.Control.Except

def unzipCommits (x₀ pk : P) (zs : Vector G n)
    (hash : Vector Bool n) : Vector P n :=
  Vector.zipWith (λ z b ↦ if b then z +ᵥ pk else z +ᵥ x₀) zs hash

def prodComm (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}):
    Lens.Equiv.{max uA₁ uA₂, max uB₁ uB₂, max uA₁ uA₂, max uB₁ uB₂} (P * Q) (Q * P) where
  toLens := Prod.swap ⇆ (fun _ => Sum.elim Sum.inr Sum.inl)
  invLens := Prod.swap ⇆ (fun _ => Sum.elim Sum.inr Sum.inl)
  left_inv := by admit /- proof elided -/

instance : Functor Stream' where
  map := Stream'.map

List.singleton in Init.Data.List.Basic

instance : MonadFunctor (OracleQuery spec) (OracleComp spec) where
  monadMap f := (OptionT.instMonadFunctor).monadMap
    ((FreeMonad.instMonadFunctor).monadMap f)

def prodZero :
    Lens.Equiv.{max uA₁ uA₂, max uB₁ uB₂, uA₁, uB₁} (P * (0 : PFunctor.{uA₂, uB₂})) 0 where
  toLens := (fun a => PEmpty.elim a.2) ⇆ (fun _ x => PEmpty.elim x)
  invLens := PEmpty.elim ⇆ (fun pe _ => PEmpty.elim pe)
  left_inv := by admit /- proof elided -/

inline in Init.Core

instReprString in Init.Data.Repr

Function.Injective2 in Mathlib.Logic.Function.Basic

instance [hι : DecidableEq ι] [hd : ∀ i, DecidableEq (spec.domain i)] {α : Type u} :
    DecidableEq (OracleQuery spec α)
  | query i t => λ q ↦ match hι i q.index with
    | isTrue h => by admit /- proof elided -/
    | isFalse h => isFalse λ h' ↦ h (congr_arg index h')

instance : Coseq NonEmptyList where
  coseq := NonEmptyList.zip

bind_assocᵣ {α β γ : Type u} (x : m α) (f : j α → m β) (g : j β → m γ) :
    x >>=ᵣ f >>=ᵣ g = x >>=ᵣ fun x ↦ f x >>=ᵣ g

List.Vector.cons in Mathlib.Data.Vector.Defs

PMF.uniformOfFintype in Mathlib.Probability.Distributions.Uniform

Finite in Mathlib.Data.Finite.Defs

instance {m n o} [Monad m] [Monad n] [Monad o] [MonadFunctor n o] [MonadFunctorT m n]
    [LawfulMonadFunctor n o] [LawfulMonadFunctorT m n] : LawfulMonadFunctorT m o where
  monadMap_id := by admit /- proof elided -/

def loggingOracle : QueryImpl spec (WriterT (QueryLog spec) (OracleComp spec)) :=
  idOracle.withLogging

instance {P : PreCondition σ} {s' : σ} :
    Inhabited (StrongestPostcondition P (set s' : StateM σ Unit)) where
  default := ⟨fun s _ s'' => P s ∧ s'' = s', HoareTriple.set_rule_forward P s',
    fun Q' hQ' _ => by admit /- proof elided -/
    ⟩

instance : Extend Zipper where
  extend z f := map f (duplicate z)

instance : unifSpec.DecidableEq where
  domain_decidableEq' := inferInstance
  range_decidableEq' := inferInstance

def parallelizationExp [DecidableEq P]
    (adversary : parallelizationAdversary G P) : ProbComp Unit := do
  let x ←$ᵗ P; let g₁ ←$ᵗ G; let g₂ ←$ᵗ G
  let x₁ := g₁ +ᵥ x
  let x₂ := g₂ +ᵥ x
  let x₃ ← adversary x x₁ x₂
  guard (x₃ = g₁ +ᵥ g₂ +ᵥ x)

noncomputable def ProbComp.advantage₂ (p q : ProbComp Unit) : ℝ :=
  |([= () | p]).toReal - ([= () | q]).toReal|

instance [RelativePure Id f] : Pure f where
  pure := @pureᵣ Id f _

def decrypt_message (encrypted_msg : EncryptedMessage) (nonce : BitVec 256) : String :=
  let decrypted_bv := mock_decrypt encrypted_msg.ciphertext
  let (msg, _) := deserialize_message_data (decrypted_bv, nonce)
  msg

@[inline, reducible] def seededOracle [DecidableEq ι] :
    QueryImpl spec (ReaderT (QuerySeed spec) (OracleComp spec)) :=
  idOracle.withPregen

def IsQueryBound (oa : OracleComp spec α) (qb : ι → ℕ) : Prop :=
    ∀ qc ∈ (snd <$> (simulateQ countingOracle oa).run).support, qc ≤ qb

def verify_message_package
    (package : MessagePackage) : OracleComp unifSpec (Option SecretMessage) := do
  let content := decrypt_message package.encrypted_message package.nonce
  let (msg_bv, _) := serialize_message_data content package.nonce
  let computed_tf := mock_hmac_sha256 package.nonce msg_bv
  if computed_tf = package.franking_tag.tag then
    return some { content := content, nonce := package.nonce }
  else
    return none

Finset.card in Mathlib.Data.Finset.Card

instance : LawfulComonad (Prod ε) where
  
  map_eq_extend_extract := by admit /- proof elided -/

def tensorAssoc : (P ⊗ Q) ⊗ R ≃ₗ P ⊗ (Q ⊗ R) where
  toLens := (_root_.Equiv.prodAssoc _ _ _).toFun ⇆
            (fun _ => (_root_.Equiv.prodAssoc _ _ _).invFun)
  invLens := (_root_.Equiv.prodAssoc _ _ _).invFun ⇆
            (fun _ => (_root_.Equiv.prodAssoc _ _ _).toFun)
  left_inv := rfl
  right_inv := rfl

def IND_CPA_oracleSpec (_encAlg : AsymmEncAlg ProbComp M PK SK C) :=
  unifSpec ++ₒ (M × M →ₒ C)

def LHL_Consequence_Adv (n p : ℕ) := (Vector (Fin p) n) × (Fin p) → ProbComp Bool

def tails : NonEmptyList α → NonEmptyList (NonEmptyList α)
  | nel@⟨_, t⟩ =>
    
    let head_tail : NonEmptyList α := nel
    
    let rest_tails_list : List (NonEmptyList α) :=
      List.filterMap NonEmptyList.fromList? (List.tails t)
    ⟨head_tail, rest_tails_list⟩

def speedup {S : Type u} {P : PFunctor.{uA, uB}} (l : Lens (selfMonomial S) P) :
    Lens (selfMonomial S) (P ◃ P) :=
  (l ◃ₗ l) ∘ₗ fixState

PMF.toOuterMeasure in Mathlib.Probability.ProbabilityMassFunction.Basic

@[inline, reducible] def cachingOracle :
    QueryImpl spec (StateT spec.QueryCache (OracleComp spec)) :=
  idOracle.withCaching

def single [DecidableEq ι] (i : ι) : QueryCount spec := Function.update 0 i 1

@[always_inline, inline]
def liftPos (a : P.A) : FreeM P (P.B a) := FreeM.roll a FreeM.pure

CategoryTheory.aesop_cat in Mathlib.CategoryTheory.Category.Basic

def test_abuse_report_validation : IO Unit := do
  let message_content := "Hello world"
  let manipulated_message := "Hell world"
  let maybeData ← OracleComp.runIO (simulation_setup message_content)
  match maybeData with
  | none =>
    IO.println "setup failed"
  | some data =>
    let valid_abuse_report := {
      message := data.verified_msg,
      franking_tag := data.message_package.franking_tag,
      reporting_tag := data.message_package.reporting_tag,
      context := data.message_package.context }
    let is_valid := validate_abuse_report valid_abuse_report data.facebook_key
    IO.println s!"valid abuse report validation result: {is_valid}"

Stream'.zip in Mathlib.Data.Stream.Defs

AddGroup in Mathlib.Algebra.Group.Defs

Array.flatMapM in Init.Data.Array.Basic

FunLike in Mathlib.Data.FunLike.Basic

def uniformErrSamp {p : ℕ} (χ : ℕ) (hχ : p > 2*χ) : ProbComp (Fin p) := do
  let e ←$ᵗ Fin (2*χ + 1)
  haveI : NeZero p := ⟨by admit /- proof elided -/
  ⟩
  return (Fin.castLE hχ e) - ⟨χ, by admit /- proof elided -/
  ⟩

Stream'.map in Mathlib.Data.Stream.Defs

structure AsymmEncAlg (m : Type → Type u) (M PK SK C : Type)
    extends ExecutionMethod m where
  keygen : m (PK × SK)
  encrypt : (pk : PK) → (msg : M) →  m C
  decrypt : (sk : SK) → (c : C) → Option M

instance [Monoid ω] [LawfulMonad m] : LawfulMonadLift m (WriterT ω m) where
  monadLift_pure x := map_pure (·, 1) x
  monadLift_bind {α β} x y := by admit /- proof elided -/

def invTildeL {P : PFunctor.{uA, uB}} : Lens (X ◃ P) P :=
  (fun ⟨_, f⟩ => f PUnit.unit) ⇆ (fun _ b => ⟨PUnit.unit, b⟩)

def prod (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) :
    PFunctor.{max uA₁ uA₂, max uB₁ uB₂} :=
  ⟨P.A × Q.A, fun ab => P.B ab.1 ⊕ Q.B ab.2⟩

NeZero in Init.Data.NeZero

instance instOfMonadMorphism {m n} [Monad m] [Monad n] [h : MonadLiftT m n]
    [h' : LawfulMonadLiftT m n] :
      DijkstraMonad n (fun na => { ma : m _ // monadLift ma = na }) :=
  @instOfMonadRelation m n _ _ (@instOfMonadLiftT m n h) (@instOfLawfulMonadLiftT m n _ _ h h')

def tensorZero : P ⊗ 0 ≃ₚ 0 where
  equivA := Equiv.prodPEmpty P.A
  equivB := fun a => Equiv.prodPEmpty (P.B a.1)

semiOutParam in Init.Prelude

@[simps]
def sumCongr {P Q} {R : PFunctor.{uA₃, uB₁}} {S : PFunctor.{uA₄, uB₁}} (e₁ : P ≃ₚ R) (e₂ : Q ≃ₚ S) :
    P + Q ≃ₚ (R + S : PFunctor.{max uA₃ uA₄, uB₁}) where
  equivA := _root_.Equiv.sumCongr e₁.equivA e₂.equivA
  equivB := (Sum.casesOn · (e₁.equivB ·) (e₂.equivB ·))

instance {σ : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] [MonadStateOf σ m]
    [LawfulMonadStateOf σ m] : LawfulMonadState σ m where
  modifyGet_eq f := LawfulMonadStateOf.modifyGet_eq f
  get_get := LawfulMonadStateOf.get_get
  set_set := LawfulMonadStateOf.set_set
  get_set := LawfulMonadStateOf.get_set
  set_get := LawfulMonadStateOf.set_get

def Hybrid_2 : ProbComp Bool := do
  let b ←$ᵗ Bool
  let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
  let u ←$ᵗ Vector (Fin p) m
  let ⟨_, _, st⟩ ← adv.chooseMessages (A, u)
  
  let c₁ ←$ᵗ Vector (Fin p) n
  let c₂ ←$ᵗ Fin p
  let b' ← adv.distinguish st (c₁, c₂)
  return b = b'

@[simp]
noncomputable def depthBindAux {f : Type u → Type v} {α β : Type u} :
    FreeMonad f α → (α → FreeMonad f β) → ℕ∞
  | .pure x, g => depth (g x)
  | .roll _ r, g => 1 + iSup (λ u ↦ depthBindAux (r u) g)

structure MonadHom (m : Type u → Type v) [Pure m] [Bind m]
    (n : Type u → Type w) [Pure n] [Bind n] extends NatHom m n, PureHom m n, BindHom m n

Vector.zero in Init.Data.Vector.Algebra

PFunctor.M.head in Mathlib.Data.PFunctor.Univariate.M

instance range_decidableEq {i : ι} [h : spec.DecidableEq] :
    DecidableEq (spec.range i) := h.range_decidableEq' i

Array in Init.Prelude

instance : MonadTransformer (StateT σ) where
  mapMonad _ := inferInstance
  transform _ := inferInstance

def LHL_Consequence_Game_1 (adv : LHL_Consequence_Adv n p) : ProbComp Bool := do
  let x ←$ᵗ Vector (Fin p) n
  let y ←$ᵗ Fin p
  adv (x, y)

instance : MonoidalCategory (Preord) where
  tensorObj X Y := ⟨X.carrier × Y.carrier⟩
  whiskerLeft X Y := fun f => ofHom ⟨fun x => (x.1, f.1 x.2),
      (by admit /- proof elided -/
      )⟩
  whiskerRight f Y := ofHom ⟨fun y => (f.hom y.1, y.2),
      (by admit /- proof elided -/
      )⟩
  tensorUnit := ⟨PUnit⟩
  associator X Y Z := {
    hom := ofHom ⟨fun ⟨⟨x, y⟩, z⟩ => ⟨x, ⟨y, z⟩⟩, by admit /- proof elided -/
      ⟩
    inv := ofHom ⟨fun ⟨x, ⟨y, z⟩⟩ => ⟨⟨x, y⟩, z⟩, by admit /- proof elided -/
      ⟩ }
  leftUnitor X := {
    hom := ofHom ⟨Prod.snd, (by admit /- proof elided -/
    )⟩
    inv := ofHom ⟨fun x => (PUnit.unit, x), by admit /- proof elided -/
    ⟩ }
  rightUnitor X := {
    hom := ofHom ⟨Prod.fst, (by admit /- proof elided -/
    )⟩
    inv := ofHom ⟨fun x => (x, PUnit.unit), by admit /- proof elided -/
    ⟩ }
  tensorHom_def f g := rfl
  
  tensor_comp f₁ f₂ g₁ g₂ := rfl
  whiskerLeft_id _ _ := rfl
  id_whiskerRight _ _ := rfl
  associator_naturality f₁ f₂ f₃ := rfl
  leftUnitor_naturality f := rfl
  rightUnitor_naturality f := rfl
  pentagon _ _ _ _ := rfl
  triangle _ _ := rfl

def tensor (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) :
    PFunctor.{max uA₁ uA₂, max uB₁ uB₂} :=
  ⟨P.A × Q.A, fun ab => P.B ab.1 × Q.B ab.2⟩

Nat in Init.Prelude

@[always_inline, inline]
protected def bind : FreeMonad f α → (α → FreeMonad f β) → FreeMonad f β
  | FreeMonad.pure x, g => g x
  | FreeMonad.roll x r, g => FreeMonad.roll x (λ u ↦ FreeMonad.bind (r u) g)

@[inherit_doc] scoped[PFunctor] infixl:25 " ≃ₚ " => PFunctor.Equiv

class SubSpec (spec : OracleSpec.{u,w} ι) (superSpec : OracleSpec τ)
  extends MonadLift (OracleQuery spec) (OracleQuery superSpec) where

instance [MonadLift (OracleQuery spec) (OracleQuery superSpec)] :
    MonadLift (OracleComp spec) (OracleComp superSpec) where
  monadLift oa := liftComp oa superSpec

CategoryTheory.NatTrans.mk in Mathlib.CategoryTheory.NatTrans

IO.rand in Init.Data.Random

def prodOne :
    Lens.Equiv.{max uA₁ uA₂, max uB₁ uB₂, uA₁, uB₁} (P * (1 : PFunctor.{uA₂, uB₂})) P where
  toLens := Prod.fst ⇆ (fun _ => Sum.inl)
  invLens := (fun p => (p, PUnit.unit)) ⇆ (fun _ => Sum.elim id PEmpty.elim)
  left_inv := by admit /- proof elided -/

instance (m : Type u → Type v) [Pure m] [Bind m]
    (n : Type u → Type w) [Pure n] [Bind n] (F : m →ᵐ n) :
    IsMonadHom m n F.toFun where
  map_pure := F.toFun_pure'
  map_bind := F.toFun_bind'

Function.update in Mathlib.Logic.Function.Basic

def unforgeableExp {sigAlg : SignatureAlg (OracleComp spec) M PK SK S}
    (adv : unforgeableAdv sigAlg) : ProbComp Bool :=
  sigAlg.exec do
    let (pk, sk) ← sigAlg.keygen
    
    let sim_adv : WriterT (QueryLog (M →ₒ S)) (OracleComp spec) (M × S) :=
      simulateQ (idOracle ++ₛₒ sigAlg.signingOracle pk sk) (adv.main pk)
    
    let ((m, σ), log) ← sim_adv.run
    return !(log.wasQueried () m) && (← sigAlg.verify pk m σ)

@[simp]
def duplicate {α : Type u} (wa : w α) : w (w α) :=
  extend wa id

instance : Comonad (CofreeC F) where
  extract := extract
  extend := sorry
  coseq := sorry

def PerfectlyCorrect (encAlg : AsymmEncAlg m M PK SK C) : Prop :=
  ∀ (msg : M), [⊥ | CorrectExp encAlg msg] = 0

Decidable.isFalse in Init.Prelude

StateT.failure in Init.Control.State

abbrev ProbComp : Type z → Type (max z 1) := OracleComp unifSpec

set_set : {s₁ s₂ : σ} → (do set s₁; set s₂) = set s₂

bind_pure_compᵣ {α β : Type u} (f : j α → j β) (x : m α) :
    x >>=ᵣ (fun y => pureᵣ (f y)) = f <$>ᵣ x

Equiv in Mathlib.Logic.Equiv.Defs

class LawfulMonadControlT (m : Type u → Type v) (n : Type u → Type w)
    [Monad m] [Monad n] [MonadControlT m n] : Prop where

OfNat in Init.Prelude

def withCaching (so : QueryImpl spec m) : QueryImpl spec (StateT spec.QueryCache m) where
  impl | query i t => do match (← get) i t with
    | Option.some u => return u
    | Option.none =>
        let u ← so.impl (query i t)
        modifyGet fun cache => (u, cache.cacheQuery i t u)

instance instLawfulCoapplicative [Comonad w] [LawfulCoapplicative w] : LawfulCoapplicative (StoreT s w) where
  coseqLeft_eq := sorry 
  coseqRight_eq := sorry 
  coseq_assoc := sorry

def selfMonomial (S : Type uA) : PFunctor.{uA, uA} :=
  S X^ S

Bind.bind in Init.Prelude

instance : LawfulMonad (OracleComp spec) :=
  inferInstanceAs (LawfulMonad (OptionT (FreeMonad (OracleQuery spec))))

protected def id (P : PFunctor.{uA, uB}) : Lens P P where
  toFunA := id
  toFunB := fun _ => id

def sum (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) :
    PFunctor.{max uA₁ uA₂, uB} :=
  ⟨P.A ⊕ Q.A, Sum.elim P.B Q.B⟩

Subsingleton in Init.Core

LawfulMonadLiftT in Init.Control.Lawful.MonadLift.Basic

def XComp : X ◃ P ≃ₗ P where
  toLens := invTildeL
  invLens := tildeL
  left_inv := rfl
  right_inv := rfl

instance : Coapplicative Zipper where
  coseq := coseq

Prod in Init.Prelude

structure Context where
  sender_id : BitVec 256
  recipient_id : BitVec 256
  timestamp : Nat
  message_id : Nat
  deriving Repr

instance {T U : Type v} [DecidableEq T] [DecidableEq U] : (T →ₒ U).DecidableEq where
  domain_decidableEq' := inferInstance
  range_decidableEq' := inferInstance

def prodAssoc : Lens.Equiv.{max uA₁ uA₂ uA₃, max uB₁ uB₂ uB₃, max uA₁ uA₂ uA₃, max uB₁ uB₂ uB₃}
    ((P * Q) * R) (P * (Q * R)) where
  toLens := (_root_.Equiv.prodAssoc P.A Q.A R.A).toFun ⇆
              (fun _ d => (_root_.Equiv.sumAssoc _ _ _).invFun d)
  invLens := (_root_.Equiv.prodAssoc P.A Q.A R.A).invFun ⇆
               (fun _ d => _root_.Equiv.sumAssoc _ _ _ d)
  left_inv := by admit /- proof elided -/

instance : LawfulMonadState σ (StateT σ m) := inferInstance

def invNatHom (e : NatEquiv m n) : NatHom n m where
  toFun := e.invFun

def simulation_setup (message_content : String) : OracleComp unifSpec (Option SimulationData) := do
  let facebook_key := BitVec.ofNat 256 123456789
  let context : Context := {
    sender_id := BitVec.ofNat 256 1001, recipient_id := BitVec.ofNat 256 1002,
    timestamp := 1730230302,
    message_id := 123 }
  let nonce ← generate_nonce
  let franking_tag  := generate_franking_tag nonce message_content
  let encrypted_msg := prepare_encrypted_message message_content nonce
  let reporting_tag := generate_reporting_tag franking_tag context facebook_key
  let package : MessagePackage := {
    encrypted_message := encrypted_msg,
    franking_tag := franking_tag,
    reporting_tag := reporting_tag,
    context := context,
    nonce := nonce }
  let maybeVerifiedMsg ← verify_message_package package
  match maybeVerifiedMsg with
  | none => 
    return none
  | some verified_msg =>
    return some { verified_msg := verified_msg
                  message_package := package
                  facebook_key := facebook_key }

class Monad.IsOrdered (m : Type u → Type v) [Monad m] where
  [monadOrder {α : Type u} : Preorder (m α)]
  bind_mono {α β : Type u} {ma ma' : m α} {f f' : α → m β} (ha : ma ≤ ma') (hf : ∀ a, f a ≤ f' a) :
    ma >>= f ≤ ma' >>= f'

CategoryTheory.EnrichedCategory in Mathlib.CategoryTheory.Enriched.Basic

MonadStateOf.get in Init.Prelude

def parallelTestingAdversary (_G P : Type) := P → P → P → P → ProbComp Bool

instance : coinSpec.FiniteRange where
  range_inhabited' := inferInstance
  range_fintype' := inferInstance

class LawfulMonadRelationHom (m₁ : Type u → Type v₁) (n₁ : Type u → Type w₁)
    (m₂ : Type u → Type v₂) (n₂ : Type u → Type w₂)
    [MonadRelation m₁ n₁] [MonadRelation m₂ n₂]
    [MonadRelationHom m₁ n₁ m₂ n₂] where
  monadRel_hom {α : Type u} {ma : m₁ α} {na : n₁ α} (h : ma ∼ₘ na) :
    (monadRelHomFst n₁ n₂ ma : m₂ α) ∼ₘ (monadRelHomSnd m₁ m₂ na : n₂ α)

structure SymmEncAlg (m : Type u → Type v)
    (M K C : Type u) extends ExecutionMethod m where
  keygen : m K
  encrypt (k : K) (msg : M) : m C
  decrypt (k : K) (c : C) : Option M

PFunctor.W in Mathlib.Data.PFunctor.Univariate.Basic

class LawfulMonadFunctor (m : semiOutParam (Type u → Type v)) (n : Type u → Type w)
    [Monad m] [Monad n] [MonadFunctor m n] : Prop where
   
  monadMap_id {α : Type u} :
    MonadFunctor.monadMap (fun {β} => (id : m β → _)) = (id : n α → _)

def LWE_Search_Adversary :=
  Matrix (Fin n) (Fin m) (Fin p) × Vector (Fin p) m → ProbComp (Vector (Fin p) n)

@[reducible] def QueryCount (_spec : OracleSpec ι) : Type u := ι → ℕ

Functor.map in Init.Prelude

@[simp] def negligible_iff (f : ℕ → ℝ≥0∞) :
    negligible f ↔ SuperpolynomialDecay atTop (λ x ↦ ↑x) f := Iff.rfl

def liftComp (oa : OracleComp spec α) (superSpec : OracleSpec τ)
      [h : MonadLift (OracleQuery spec) (OracleQuery superSpec)] :
      OracleComp superSpec α := simulateQ ⟨liftM⟩ oa

PFunctor.B in Mathlib.Data.PFunctor.Univariate.Basic

instance : CoseqRight Stream' where
  coseqRight _ s₂ := s₂

Matrix in Mathlib.LinearAlgebra.Matrix.Defs

Equiv.pemptyProd in Mathlib.Logic.Equiv.Prod

Fintype.card in Mathlib.Data.Fintype.Card

def refl (m : Type u → Type v) : NatEquiv m m where
  toFun := id
  invFun := id
  left_inv := by admit /- proof elided -/

instance [IsEmpty I] {F : I → PFunctor.{u}} {a : (sigma F).A} : IsEmpty ((sigma F).B a) :=
  isEmptyElim a

class Extend (w : Type u → Type v) where
   
  extend {α β : Type u} : w α → (w α → β) → w β

class LawfulDijkstraMonadLift (w₁ : Type u → Type v) (w₂ : Type u → Type w)
    (d₁ : {α : Type u} → w₁ α → Type z) (d₂ : {α : Type u} → w₂ α → Type z)
    [Monad w₁] [Monad w₂] [MonadLiftT w₁ w₂] [DijkstraMonad w₁ d₁] [DijkstraMonad w₂ d₂]
    [inst : DijkstraMonadMorphism w₁ w₂ d₁ d₂]
    [LawfulMonad w₁] [LawfulMonad w₂] [LawfulMonadLiftT w₁ w₂] where
  dMorphism_dPure {α : Type u} (a : α) :
    (monadLift_pure (m := w₁) (n := w₂) a) ▸ (dMorphism (dPure a : d₁ _)) = (dPure a : d₂ _)
  dMorphism_dBind {α β : Type u} {a : w₁ α} {f : α → w₁ β} (x : d₁ a) (g : (a : α) → d₁ (f a)) :
    (monadLift_bind (m := w₁) (n := w₂) a f) ▸ (dMorphism x >>=ᵈ (fun a => dMorphism (g a))) =
      inst.dMorphism (x >>=ᵈ g)

instance {n : Type u → Type v} [MonadLiftT m n] : MonadLiftT (FreeContT f m) (FreeContT f n) where
  monadLift := fun x => fun handleEff handlePure => by admit /- proof elided -/

instance : LawfulFunctor NonEmptyList where
  id_map := by admit /- proof elided -/

def sumZero :
    Lens.Equiv.{max uA uA₁, uB, uA₁, uB} (P + (0 : PFunctor.{uA, uB})) P where
  toLens := Lens.sumPair (Lens.id P) Lens.initial
  invLens := Lens.inl
  left_inv := by admit /- proof elided -/

structure StoreT (s : Type u₂) (w : Type u₂ → Type v₂) (a : Type u₂) where
   
  runStoreT : w (s → a)
   
  pos : s

def symm (e : NatEquiv m n) : NatEquiv n m where
  toFun := e.invFun
  invFun := e.toFun
  left_inv := e.right_inv
  right_inv := e.left_inv

def trans (e₁ : NatEquiv m n) (e₂ : NatEquiv n p) : NatEquiv m p where
  toFun := e₂.toFun ∘ e₁.toFun
  invFun := e₁.invFun ∘ e₂.invFun
  left_inv := by admit /- proof elided -/

@[inline, reducible] def coinSpec : OracleSpec.{0,0} Unit := Unit →ₒ Bool

List.foldlM in Init.Data.List.Control

instance : Extract Id where
  extract := id

instance : LawfulCoapplicative NonEmptyList where
  coseqLeft_eq := by admit /- proof elided -/

instance (n : ℕ) : SelectableType (Fin (n + 1)) where
  selectElem := $[0..n]
  mem_support_selectElem := by admit /- proof elided -/

def PFunctor.FreeContT (P : PFunctor.{z, y}) (m : Type u → Type v) (α : Type w) :
    Type (max (u + 1) v w y z) :=
  {r : Type u} → ((a : P.A) → ContT r m (P.B a)) → ContT r m α

def replicate {ι : Type u} {spec : OracleSpec ι} {α : Type v}
    (n : ℕ) (oa : OracleComp spec α) : OracleComp spec (List α) :=
  (List.replicate n ()).mapM fun () => oa

def finSupport [∀ i, Fintype (spec.range i)] [DecidableEq α] (oa : OracleComp spec α) : Finset α :=
  oa.finSupportWhen fun | query _ _ => Finset.univ

def LWE_Adversary := Matrix (Fin n) (Fin m) (Fin p) × Vector (Fin p) m → ProbComp Bool

instance instMonadLift [Bind m] : MonadLift m (FreeContT f m) where
  monadLift := lift

def PerfectlyComplete (sigAlg : SignatureAlg m M PK SK S) : Prop :=
  ∀ msg : M, [= true | sigAlg.exec do
    let (pk, sk) ← sigAlg.keygen
    let sig ← sigAlg.sign pk sk msg
    sigAlg.verify pk msg sig] = 1

PMF.uniformOfFinset in Mathlib.Probability.Distributions.Uniform

def tensorX : P ⊗ X ≃ₗ P where
  toLens := Prod.fst ⇆ (fun _ b => (b, PUnit.unit))
  invLens := (fun p => (p, PUnit.unit)) ⇆ (fun _ bp => bp.1)
  left_inv := rfl
  right_inv := rfl

Id in Init.Control.Id
</all_available_defs>

<all_available_lemmas>
@[simp low]
lemma probEvent_eq_zero_iff : [p | oa] = 0 ↔ ∀ x ∈ oa.support, ¬ p x

@[simp]
lemma liftComp_pure (x : α) : liftComp (pure x : OracleComp spec α) superSpec = pure x

lemma probOutput_cons_seq_map_cons_eq_mul' [spec.FiniteRange] [spec.DecidableEq] (x : α)
    (xs : List α) : [= x :: xs | (λ xs x ↦ x :: xs) <$> ob <*> oa] = [= x | oa] * [= xs | ob]

@[simp]
lemma liftM_query_readerT {ρ : Type v} {α : Type v} (q : OracleQuery spec α) :
  (liftM q : ReaderT ρ (OracleComp spec) α) = liftM (liftM q : OracleComp spec α)

lemma evalDist_seq_map [spec.FiniteRange] :
    evalDist (f <$> oa <*> ob) = f <$> evalDist oa <*> evalDist ob

lemma evalDist_apply_some (oa : OracleComp spec α) (x : α) :
    (evalDist oa).run (some x) = [= x | oa]

@[simp]
lemma liftComp_map (oa : OracleComp spec α) (f : α → β) :
    liftComp (f <$> oa) superSpec = f <$> liftComp oa superSpec

@[simp]
lemma probOutput_eq_zero_iff' [spec.DecidableEq] [DecidableEq α] :
    [= x | oa] = 0 ↔ x ∉ oa.finSupport

@[simp]
lemma probOutput_vector_toList [spec.FiniteRange] [spec.DecidableEq]
    {n : ℕ} (oa : OracleComp spec (List.Vector α n))
    (xs : List α) : [= xs | List.Vector.toList <$> oa] =
      if h : xs.length = n then [= ⟨xs, h⟩ | oa] else 0

lemma mem_support_map {oa : OracleComp spec α} {x : α}
    (hx : x ∈ oa.support) (f : α → β) : f x ∈ (f <$> oa).support

@[simp] lemma apply_eq [spec.FiniteRange] (q : OracleQuery spec α) :
    defaultOracle.impl q = return q.defaultOutput

lemma not_mem_support_iff_probOutput_eq_zero : x ∉ oa.support ↔ [= x | oa] = 0

@[simp]
lemma evalDist_simulateQ [spec.FiniteRange] (oa : OracleComp spec α) :
    evalDist (simulateQ unifOracle oa) = evalDist oa

@[simp] lemma support_uniformSelectList (xs : List α) :
    ($ xs).support = if xs.isEmpty then ∅ else {y | y ∈ (xs)}

@[simp]
theorem getThe_eq [MonadStateOf σ m] : getThe σ (m := m) = MonadStateOf.get

@[simp]
theorem comp_id {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : Lens P Q) :
    f ∘ₗ (Lens.id P) = f

@[simp]
theorem sumMap_id :
    Lens.sumMap (Lens.id P) (Lens.id Q) = Lens.id.{max uA₁ uA₂, uB₁} (P + Q)

@[simp] lemma C_A (A : Type u) : (C A).A = A

@[simp]
lemma probFailure_replicate [spec.FiniteRange] :
    [⊥ | oa.replicate n] = 1 - (1 - [⊥ | oa]) ^ n

@[simp] lemma simulateQ_seq (og : OracleComp spec (α → β)) (oa : OracleComp spec α) :
    simulateQ so (og <*> oa) = simulateQ so og <*> simulateQ so oa

@[simp] theorem id_mapᵣ' [RelativeFunctor j f] [LawfulRelativeFunctor j f] (x : f α) :
    (fun a : j α => a) <$>ᵣ x = x

@[simp]
lemma probOutput_replicate [spec.FiniteRange] (xs : List α) :
    [= xs | oa.replicate n] = if xs.length = n then (xs.map ([= · | oa])).prod else 0

@[simp] lemma query_ne_pure : (q : OracleComp spec β) ≠ pure y

@[simp]
theorem id_comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : Lens P Q) :
    (Lens.id Q) ∘ₗ f = f

@[simp]
theorem symm_comp_self {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P ≃ₚ Q) :
    e.symm.equivA ∘ e.equivA = id

@[ext (iff := false)]
theorem ext {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (c₁ c₂ : Chart P Q)
    (h₁ : ∀ a, c₁.toFunA a = c₂.toFunA a) (h₂ : ∀ a, c₁.toFunB a = (h₁ a) ▸ c₂.toFunB a) :
    c₁ = c₂

@[simp] lemma query_bind_ne_failure : (q : OracleComp spec β) >>= oa ≠ failure

@[simp]
lemma countQ_append (log log' : QueryLog spec) (i : ι) :
    (log ++ log').countQ i = log.countQ i + log'.countQ i

@[simp] -- mathlib?
lemma vector_eq_nil {α : Type*} (xs : List.Vector α 0) : xs = Vector.nil

lemma BitVec.toFin_bijective (n : ℕ) :
    Function.Bijective (BitVec.toFin : BitVec n → Fin (2 ^ n))

@[simp]
lemma liftM_inj (q q' : OracleQuery spec α) : (q : OracleComp spec α) = q' ↔ q = q'

@[simp] lemma input_query (i : ι) (t : spec.domain i) : (query i t).input = t

lemma liftM_def (x : m α) :
    (liftM x : WriterT ω m α) = WriterT.mk ((·, 1) <$> x)

lemma probEvent_seq_map_eq_mul {ι : Type u} {spec : OracleSpec ι}
    {α β γ : Type v} (f : α → β → γ) [spec.FiniteRange]
    (oa : OracleComp spec α) (ob : OracleComp spec β)
    (p : γ → Prop) (q1 : α → Prop) (q2 : β → Prop)
    (h : ∀ x ∈ oa.support, ∀ y ∈ ob.support, p (f x y) ↔ q1 x ∧ q2 y) :
    [p | f <$> oa <*> ob] = [q1 | oa] * [q2 | ob]

lemma mem_finSupport_bind_iff [spec.FiniteRange]
    (oa : OracleComp spec α) (ob : α → OracleComp spec β)
    [hoa : DecidableEq α] [hob : DecidableEq β] (y : β) : y ∈ (oa >>= ob).finSupport ↔
      ∃ x ∈ oa.finSupport, y ∈ (ob x).finSupport

lemma probEvent_bind_eq_sum_fintype [Fintype α] (q : β → Prop) :
    [q | oa >>= ob] = ∑ x : α, [= x | oa] * [q | ob x]

@[simp]
theorem vectorofFn_get {α : Type} {n : ℕ} (v : Fin n → α) : (Vector.ofFn v).get = v

@[simp low]
lemma probOutput_eq_zero_iff : [= x | oa] = 0 ↔ x ∉ oa.support

lemma probOutput_map_eq_sum_fintype_ite [Fintype α] [DecidableEq β] (y : β) :
    [= y | f <$> oa] = ∑ x : α, if y = f x then [= x | oa] else 0

@[simp] lemma probOutput_eq : probOutput p = p

@[simp]
lemma probOutput_bitVec_ofFin_map {n : ℕ} (oa : OracleComp spec (Fin (2 ^ n)))
    (x : BitVec n) : [= x | ofFin <$> oa] = [= toFin x | oa]

@[simp]
lemma probOutput_coin (b : Bool) : [= b | coin] = 2⁻¹

@[simp]
lemma mmap_bind (F : m →ᵐ n) (x : m α) (y : α → m β) :
    F (x >>= y) = F x >>= fun x => F (y x)

@[simp] lemma monoid_mul_def (qc qc' : QueryCount spec) :
  (@HMul.hMul _ _ _ (@instHMul _ (Monoid.toMulOneClass.toMul)) qc qc')
     = (qc : ι → ℕ) + (qc' : ι → ℕ)

@[simp] theorem toMonadState_get_eq_monadStateOf_get {m : Type u → Type v} {σ : Type u}
    [MonadStateOf σ m] : (MonadState.get : m σ) = MonadStateOf.get

lemma probEvent_seq_map_eq_probEvent [spec.FiniteRange] (p : γ → Prop) :
    [p | f <$> oa <*> ob] = [λ z ↦ p (f z.1 z.2) | Prod.mk <$> oa <*> ob]

@[simp low]
lemma finSupport_seq [spec.DecidableEq] [spec.FiniteRange]
    [DecidableEq α] [DecidableEq β] [DecidableEq (α → β)] :
    (og <*> oa).finSupport = og.finSupport.biUnion (λ g ↦ oa.finSupport.image g)

@[simp]
lemma support_generateSeed : (generateSeed spec qc js).support =
    {seed | ∀ i, (seed i).length = qc i * js.count i}

theorem PMF.heq_iff {α β : Type u} {pa : PMF α} {pb : PMF β} (h : α = β) :
    HEq pa pb ↔ ∀ x, pa x = pb (cast h x)

@[simp] -- NOTE: shouldn't actually need finiteness here.
lemma support_liftComp [spec.FiniteRange] [superSpec.FiniteRange]
    (oa : OracleComp spec α) : (liftComp oa superSpec).support = oa.support

lemma probOutput_prod_mk_seq_map_eq_mul' [spec.FiniteRange] (oa : OracleComp spec α)
    (ob : OracleComp spec β) (x : α) (y : β) :
    [= (x, y) | ((·, ·) <$> oa <*> ob : OracleComp spec (α × β))] = [= x | oa] * [= y | ob]

@[simp] lemma finSupport_uniformOfFintype [Fintype α] [DecidableEq α] :
    ($ᵗ α).finSupport = Finset.univ

@[simp]
lemma isQueryBound_failure (qb : ι → ℕ) : IsQueryBound (failure : OracleComp spec α) qb

@[simp] lemma pure_ne_query : pure y ≠ (q : OracleComp spec β)

lemma probOutput_seq_eq_sum_finSupport_ite [spec.FiniteRange] [spec.DecidableEq]
    [DecidableEq α] [DecidableEq (α → β)] [DecidableEq β]
    (y : β) : [= y | og <*> oa] = ∑ g ∈ og.finSupport, ∑ x ∈ oa.finSupport,
      if y = g x then [= g | og] * [= x | oa] else 0

@[simp] lemma support_map (oa : OracleComp spec α) (f : α → β) :
    (f <$> oa).support = f '' oa.support

@[simp] lemma tsum_probOutput_ne_top : ∑' x : α, Pr[= x | mx] ≠ ⊤

@[simp]
theorem sumMap_comp_inr (l₁ : Lens P R) (l₂ : Lens Q W) :
    ((l₁ ⊎ₗ l₂) ∘ₗ Lens.inr) = (Lens.inr ∘ₗ l₂)

@[simp]
lemma addValues_apply (j : ι) : seed.addValues us j =
    Function.update seed i (seed i ++ us) j

@[simp] lemma evalDist_ite (p : Prop) [Decidable p] (mx mx' : m α) :
    evalDist (if p then mx else mx') = if p then evalDist mx else evalDist mx'

@[simp] lemma probEvent_uniformSelectList (xs : List α) (p : α → Prop) [DecidablePred p] :
    [p | $ xs] = if xs.isEmpty then 0 else (xs.countP p : ℝ≥0∞) / xs.length

lemma probFailure_bind_eq_tsum :
    [⊥ | oa >>= ob] = [⊥ | oa] + ∑' x : α, [= x | oa] * [⊥ | ob x]

@[simp] lemma probFailure_eq : probFailure p = 0

lemma liftM_def [Monad m] (x : m α) : (liftM x : StateT σ m α) = StateT.lift x

@[simp]
lemma snd_map_prod_map (oa : OracleComp spec (α × β)) (f : α → γ) (g : β → δ) :
    snd <$> map f g <$> oa = (g ∘ Prod.snd) <$> oa

lemma not_noFailure_of_probFailure_pos {oa : OracleComp spec α} (h : 0 < [⊥ | oa]) :
    ¬ neverFails oa

theorem exists_log_of_mem_support_fork (x₁ x₂ : α)
    (h : (x₁, x₂) ∈ (fork main qb js i cf).support) :
      ∃ s, cf x₁ = some s ∧ cf x₂ = some s ∧
      ∃ log₁ : QueryLog spec, ∃ hcf₁ : ↑s < log₁.countQ i,
      ∃ log₂ : QueryLog spec, ∃ hcf₁ : ↑s < log₂.countQ i,
      (log₁.getQ i)[s].1 = (log₂.getQ i)[s].1 ∧
      (log₁.getQ i)[s].2 ≠ (log₂.getQ i)[s].2 ∧
      (x₁, log₁) ∈ (simulateQ loggingOracle main).run.support ∧
      (x₂, log₂) ∈ (simulateQ loggingOracle main).run.support

theorem monadLift_optional [AlternativeMonad m] [AlternativeMonad n]
    [LawfulMonad m] [LawfulMonad n] [MonadLift m n] [LawfulAlternativeLift m n]
    [LawfulMonadLift m n]
    (x : m α) : monadLift (optional x) = optional (monadLift x : n α)

@[simp]
theorem sumComm_symm :
    (sumComm P Q).symm = sumComm Q P

@[simp]
lemma run_seqLeft {m : Type u → Type v} [Monad m] {ω : Type u} [Monoid ω] {α β : Type u}
    (x : WriterT ω m α) (y : WriterT ω m β) :
    (x *> y).run = x.run >>= fun z => Prod.map id (z.2 * ·) <$> y.run

@[simp] lemma not_one_lt_probEvent : ¬ 1 < [p | oa]

@[simp]
theorem ulift_B {a : P.A} : (P.ulift).B (ULift.up a) = ULift (P.B a)

lemma probEvent_seq_eq_tsum_ite [spec.FiniteRange] (p : β → Prop) [DecidablePred p] :
    [p | og <*> oa] = ∑' (g : α → β) (x : α),
      if p (g x) then [= g | og] * [= x | oa] else 0

@[simp]
lemma probOutput_seq_map_swap [spec.FiniteRange] (z : γ) :
    [= z | Function.swap f <$> ob <*> oa] = [= z | f <$> oa <*> ob]

@[simp] lemma neverFails_list_foldlM {f : s → α → OracleComp spec s} {init : s} {as : List α}
    (h : ∀ i, ∀ x ∈ as, neverFails (f i x)) : neverFails (foldlM f init as)

@[simp]
lemma probOutput_list_mapM {α β : Type*} [spec.FiniteRange] (xs : List α)
    (f : α → OracleComp spec β) (ys : List β) : [= ys | xs.mapM f] = if ys.length = xs.length
      then (List.zipWith (fun x y => [= y | f x]) xs ys).prod else 0

@[simp] lemma support_query (q : OracleQuery spec α) :
    (q : OracleComp spec α).support = Set.univ

@[simp]
lemma zero_eq_probEvent_iff' [spec.DecidableEq] [DecidableEq α] :
    0 = [p | oa] ↔ ∀ x ∈ oa.finSupport, ¬ p x

theorem comp_inl_inr (h : Lens.{max uA₁ uA₂, uB₁, uA₃, uB₃} (P + Q) R) :
    Lens.sumPair (h ∘ₗ Lens.inl) (h ∘ₗ Lens.inr) = h

@[simp] lemma neverFails_lift_comp_iff (oa : OracleComp spec α) :
    (liftComp oa superSpec).neverFails ↔ oa.neverFails

lemma probOutput_bind_ite_failure_eq_tsum [spec.FiniteRange] [DecidableEq β]
    (oa : OracleComp spec α) (f : α → β) (p : α → Prop) [DecidablePred p] (y : β) :
    [= y | oa >>= fun x => if p x then pure (f x) else failure] =
      ∑' x : α, if p x ∧ y = f x then [= x | oa] else 0

theorem PMF.bind_eq_zero {α β : Type _} {p : PMF α} {f : α → PMF β} {b : β} :
    (p >>= f) b = 0 ↔ ∀ a, p a = 0 ∨ f a b = 0

lemma probOutput_prod_mk_seq_map_eq_mul [spec.FiniteRange] (oa : OracleComp spec α)
    (ob : OracleComp spec β) (z : α × β) :
    [= z | ((·, ·) <$> oa <*> ob : OracleComp spec (α × β))] = [= z.1 | oa] * [= z.2 | ob]

lemma probEvent_pure_eq_zero {p : α → Prop} {x : α} (h : ¬ p x) :
    [p | (pure x : OracleComp spec α)] = 0

lemma finSupport_query [spec.FiniteRange] [DecidableEq α] (q : OracleQuery spec α) :
    (q : OracleComp spec _).finSupport = match q with

lemma probFailure_def (mx : m α) : Pr[⊥ | mx] = (evalDist mx).run none

@[simp] lemma supportWhen_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    (oa >>= ob).supportWhen poss = ⋃ x ∈ oa.supportWhen poss, (ob x).supportWhen poss

@[simp] lemma probOutput_pure [DecidableEq α] (x y : α) :
    Pr[= x | (pure y : m α)] = if x = y then 1 else 0

@[simp]
lemma bind_pure (x : α) (r : α → FreeM P β) :
    FreeM.bind (FreeM.pure x) r = r x

@[simp] lemma allWhen_pure (x : α) :
    (pure x : OracleComp spec α).allWhen Q F possible_outputs

lemma StateT_run'_simulateQ_eq_self {α} (so : QueryImpl spec (StateT σ (OracleComp spec)))
    (h : ∀ α (q : OracleQuery spec α) s, (so.impl q).run' s = q)
    (oa : OracleComp spec α) (s : σ) : (simulateQ so oa).run' s = oa

@[simp]
lemma query_inj (i : ι) (t t' : spec.domain i) :
    (query i t : OracleComp spec (spec.range i)) = query i t' ↔ t = t'

@[simp] lemma finSupport_query_bind [spec.FiniteRange] [Fintype α] [DecidableEq β]
    (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    (liftM q >>= ob).finSupport = Finset.univ.biUnion fun x => (ob x).finSupport

@[simp] lemma probOutput_eq : probOutput p = p

lemma subset_finSupport_iff_coe_subset_support : s ⊆ oa.finSupport ↔ ↑s ⊆ oa.support

lemma StateT_run_simulateQ_eq_map_run'_simulateQ {α} (oa : OracleComp spec α) (s s' : σ) :
    (simulateQ so oa).run s = (·, s') <$> (simulateQ so oa).run' s

@[simp] lemma probFailure_lt_top : Pr[⊥ | mx] < ∞

@[simp] lemma probOutput_uniformSelectList [DecidableEq α] (xs : List α) (x : α) :
    [= x | $ xs] = if xs.isEmpty then 0 else (xs.count x : ℝ≥0∞) / xs.length

@[simp] lemma probEvent_eq_eq_probOutput (oa : OracleComp spec α) (x : α) :
    [(· = x) | oa] = [= x | oa]

lemma probOutput_map_eq_sum_finSupport_ite [spec.DecidableEq] [DecidableEq α] [DecidableEq β]
    (y : β) : [= y | f <$> oa] = ∑ x ∈ oa.finSupport, if y = f x then [= x | oa] else 0

lemma probOutput_seq_map_eq_mul [spec.FiniteRange] (x : α) (y : β) (z : γ)
    (h : ∀ x' ∈ oa.support, ∀ y' ∈ ob.support, z = f x' y' ↔ x' = x ∧ y' = y) :
    [= z | f <$> oa <*> ob] = [= x | oa] * [= y | ob]

@[simp]
lemma probEvent_liftM_eq_mul_inv [Fintype α] (q : OracleQuery spec α)
    (p : α → Prop) [DecidablePred p] : [p | (q : OracleComp spec _)] =
      (Finset.univ.filter p).card * (↑(Fintype.card α))⁻¹

@[simp] lemma map_some_apply_some (p : PMF α) (x : α) : p.map some (some x) = p x

@[simp]
lemma probOutput_fst_map_eq_tsum [spec.FiniteRange] (oa : OracleComp spec (α × β)) (x : α) :
    [= x | fst <$> oa] = ∑' y, [= (x, y) | oa]

lemma eq_finSupport_iff_coe_eq_support : s = oa.finSupport ↔ ↑s = oa.support

@[simp]
lemma support_seq_map_swap [spec.FiniteRange] :
    (Function.swap f <$> ob <*> oa).support = (f <$> oa <*> ob).support

lemma probEvent_eq_tsum_indicator (mx : m α) (p : α → Prop) :
    Pr[p | mx] = ∑' x : α, {x | p x}.indicator (Pr[= · | mx]) x

@[simp] lemma finSupport_eqRec [spec.DecidableEq] [spec.FiniteRange]
    [hα : DecidableEq α] [hβ : DecidableEq β] (oa : OracleComp spec α) (h : α = β) :
    @finSupport _ _ _ _ hβ (h ▸ oa : OracleComp spec β) =
      h.symm ▸ @finSupport _ _ _ _ hα oa

@[simp] lemma probFailure_le_one : Pr[⊥ | mx] ≤ 1

lemma probFailure_bind_of_neverFails {oa : OracleComp spec α}
    (h : neverFails oa) (ob : α → OracleComp spec β) :
    [⊥ | oa >>= ob] = ∑' x : α, [= x | oa] * [⊥ | ob x]

@[simp]
lemma run_mk {ω : Type u} [LawfulMonad m] (x : m (α × ω)) :
  (WriterT.mk x).run = x

lemma exists_eq_of_isPure {oa : OracleComp spec α} (h : isPure oa) : ∃ x, oa = pure x

lemma probOutput_uniformSelect_bool_bind_eq_add {α : Type}
    (oa : Bool → ProbComp α) (x : α) : -- should be anything $ᵗ Bool can lift to
    [= x | ($ᵗ Bool) >>= oa] = [= x | oa true] / 2 + [= x | oa false] / 2

@[simp]
lemma probOutput_list_mapM_loop {α β : Type*} [DecidableEq β] [spec.FiniteRange]
    (xs : List α) (f : α → OracleComp spec β) (ys : List β)
    (zs : List β) : [= zs | List.mapM.loop f xs ys] =
      if zs.length = xs.length + ys.length ∧ zs.take ys.length = ys.reverse
      then (List.zipWith (λ x z ↦ [= z | f x]) xs (zs.drop ys.length)).prod else 0

@[simp] lemma tsum_probOutput_le_one : ∑' x : α, [= x | oa] ≤ 1

lemma finSupport_eq_iff_support_eq_coe : oa.finSupport = s ↔ oa.support = ↑s

@[simp]
lemma mapM_roll (x : P.A) (r : P.B x → FreeM P α) :
    (FreeM.roll x r).mapM s = s x >>= λ u ↦ (r u).mapM s

lemma mem_finSupport_seq_map_cons_iff' [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α]
    (xs : List α) : xs ∈ (cons <$> oa <*> ob).finSupport ↔
      xs.recOn False (λ x xs _ ↦ x ∈ oa.finSupport ∧ xs ∈ ob.finSupport)

@[simp]
theorem sumMap_comp_inl (l₁ : Lens P R) (l₂ : Lens Q W) :
    ((l₁ ⊎ₗ l₂) ∘ₗ Lens.inl) = (Lens.inl ∘ₗ l₁)

@[simp] lemma neverFails_uniformOfFintype : neverFails ($ᵗ α)

lemma probEvent_def (oa : OracleComp spec α) (p : α → Prop) :
    [p | oa] = (evalDist oa).run.toOuterMeasure (Option.some '' {x | p x})

@[simp] theorem duplicate_duplicate_eq_map_duplicate :
    duplicate (duplicate wa) = Functor.map duplicate (duplicate wa)

@[simp]
lemma liftComp_seq (og : OracleComp spec (α → β)) (oa : OracleComp spec α) :
    liftComp (og <*> oa) superSpec = liftComp og superSpec <*> liftComp oa superSpec

lemma probOutput_map_eq_tsum_ite [DecidableEq β] (y : β) :
    [= y | f <$> oa] = ∑' x : α, if y = f x then [= x | oa] else 0

@[simp] lemma one_le_probEvent_iff : 1 ≤ Pr[p | mx] ↔ Pr[p | mx] = 1

theorem prodMap_comp_prodPair (l₁ : Lens Q W) (l₂ : Lens R X) (f : Lens P Q) (g : Lens P R) :
    (l₁ ×ₗ l₂) ∘ₗ Lens.prodPair f g = Lens.prodPair (l₁ ∘ₗ f) (l₂ ∘ₗ g)

lemma probEvent_replicate_of_probEvent_cons [spec.FiniteRange]
    (p : List α → Prop) (hp : p []) (q : α → Prop) (hq : ∀ x xs, p (x :: xs) ↔ q x ∧ p xs) :
    [p | oa.replicate n] = [q | oa] ^ n

@[simp] lemma supportWhen_pure (x : α) :
    (pure x : OracleComp spec α).supportWhen poss = {x}

@[simp] theorem CommutativeAt.bind_comm_comp {m} [Monad m] [LawfulMonad m] {α β γ}
    (ma : m α) (mb : m β) (h : CommutativeAt m ma mb) (f : α × β → m γ) :
      (ma >>= fun a => mb >>= fun b => f (a, b)) = (mb >>= fun b => ma >>= fun a => f (a, b))

@[simp] lemma probOutput_uniformOfFintype [Fintype α] (x : α) :
    [= x | $ᵗ α] = (Fintype.card α : ℝ≥0∞)⁻¹

@[simp] lemma probEvent_lt_top : Pr[p | mx] < ∞

@[simp] lemma probFailure_uniformOfFintype : [⊥ | $ᵗ α] = 0

@[simp] lemma failure_ne_query : failure ≠ (q : OracleComp spec β)

@[simp]
lemma run_tell (w : ω) : (tell w : WriterT ω m PUnit).run = pure (⟨⟩, w)

@[simp] lemma one_le_probOutput_iff : 1 ≤ [= x | oa] ↔ [= x | oa] = 1

@[simp] lemma query_bind_ne_pure : (q : OracleComp spec β) >>= oa ≠ pure x

@[simp] theorem bind_pureᵣ [RelativeMonad j m] [LawfulRelativeMonad j m] (x : m α) :
    x >>=ᵣ pureᵣ (j := j) = x

@[simp]
lemma mapM_roll (x : f α) (r : α → FreeMonad f β) :
    (FreeMonad.roll x r).mapM s = s x >>= λ u ↦ (r u).mapM s

@[simp]
theorem set_rule_basic (s' : σ) :
    HoareTriple (fun _ => True) (set s' : StateM σ Unit) (fun _ _ s'' => s'' = s')

@[simp] lemma isFailure_pure : isFailure (pure x : OracleComp spec α) = false

lemma probFailure_writerT_run_simulateQ [spec.FiniteRange]
    {so : QueryImpl spec (WriterT ω (OracleComp spec))}
    (hso : ∀ {α}, ∀ q : OracleQuery spec α, fst <$> (so.impl q).run = q)
    (hso' : ∀ {α}, ∀ q : OracleQuery spec α, [⊥ | (so.impl q).run] = 0)
    (oa : OracleComp spec α) : [⊥ | (simulateQ so oa).run] = [⊥ | oa]

theorem bind_comm_quad_swap_23 {m} [Monad m] [LawfulMonad m] [Commutative m] {α β γ δ ε}
    (ma : m α) (mb : m β) (mc : m γ) (md : m δ) (f : α × β × γ × δ → m ε) :
    (ma >>= fun a => mb >>= fun b => mc >>= fun c => md >>= fun d => f (a, b, c, d)) =
    (ma >>= fun a => mc >>= fun c => mb >>= fun b => md >>= fun d => f (a, b, c, d))
</all_available_lemmas>

<local_ctx>
import VCVio.OracleComp.Support

open OracleSpec

namespace OracleComp

variable {ι : Type u} {spec : OracleSpec ι} {α β γ : Type v}

section When

variable (Q : {α : Type v} → OracleQuery spec α → Prop)
    (F : Prop) (oa : OracleComp spec α)
    (possible_outputs : {α : Type v} → OracleQuery spec α → Set α)

def allWhen (possible_outputs : {α : Type v} → OracleQuery spec α → Set α)
    (oa : OracleComp spec α) : Prop :=
</local_ctx>

<target_theorem>
@[simp] lemma allWhen_bind_iff (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    (oa >>= ob).allWhen Q F possible_outputs ↔ oa.allWhen Q F possible_outputs ∧
      ∀ x ∈ oa.supportWhen possible_outputs, (ob x).allWhen Q F possible_outputs :=
</target_theorem>

