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))

class HasEvalDist (m : Type u → Type v) [Monad m] where
  evalDist {α : Type u} (mx : m α) : SPMF α
  evalDist_pure {α : Type u} (x : α) : evalDist (pure x : m α) = pure x
  evalDist_bind {α β : Type u} (mx : m α) (my : α → m β) :
    evalDist (mx >>= my) = evalDist mx >>= fun x => evalDist (my x)

noncomputable def probOutput (oa : OracleComp spec α) (x : α) : ℝ≥0∞ :=
  (evalDist oa).run (some x)

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

def support (oa : OracleComp spec α) : Set α :=
  oa.supportWhen fun _ => Set.univ

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

protected class DecidableEq (spec : OracleSpec ι) where
  domain_decidableEq' (i : ι) : DecidableEq (spec.domain i)
  range_decidableEq' (i : ι) : DecidableEq (spec.range i)

class FiniteRange (spec : OracleSpec ι) where
    range_inhabited' (i : ι) : Inhabited (spec.range i)
    range_fintype' (i : ι) : Fintype (spec.range i)

@[simp]
def extract (z : Zipper α) : α := z.focus

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

Vector.insertIdx in Init.Data.Vector.Basic

def rangeInhabited [spec.FiniteRange] : OracleQuery spec α → Inhabited α
  | query i t => inferInstance

id in Init.Prelude

List.range in Init.Data.List.Basic

instance : LawfulMonad MonoContProp := inferInstanceAs (LawfulMonad (MonoCont Prop))

MonadStateOf.get in Init.Prelude

List.foldr in Init.Data.List.Basic

def probSpec : OracleSpec.{0,0} ℕ :=
  fun n => (ℕ, Fin (n + 1))

List.Vector.mmap in Mathlib.Data.Vector.Basic

def uliftSumEquiv (Q : PFunctor.{uA₂, uB₁}) :
    (PFunctor.ulift.{_, _, u, v} (P + Q : PFunctor.{max uA₁ uA₂, uB₁})) ≃ₚ
    ((PFunctor.ulift.{_, _, uA, uB} P : PFunctor.{max uA₁ uA, max uB₁ uB}) +
      (Q.ulift : PFunctor.{max uA₂ uA', max uB₁ uB}) : PFunctor.{max uA₁ uA uA₂ uA', max uB₁ uB}) :=
  sorry

ExceptT in Init.Control.Except

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

noncomputable def LWE_Search_Advantage (adv : LWE_Search_Adversary n m p) : ℝ :=
  (LWE_Search_Experiment n m p errSamp adv).advantage'

instance : Add PFunctor.{uA, uB} where
  add := sum

def serialize_message_data (msg : String) (nonce : BitVec 256) : BitVec 256 × BitVec 256 :=
  let msg_bv := string_to_bitvec msg
  (msg_bv, nonce)

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

Function.support in Mathlib.Algebra.Notation.Support

def relabelM : (t : Tree' α) → StateM ℕ (Tree' ℕ)
  | .leaf _ => do
    let n ← get
    set (n + 1)
    return .leaf n
  | .node l r => do
    let l' ← relabelM l
    let r' ← relabelM r
    return .node l' r'

structure Day (f : Type u₁ → Type v₁) (g : Type u₂ → Type v₂) (a : Type u₃) where
   
  {α : Type u₁}
   
  {β : Type u₂}
   
  map' : α → β → a
   
  fa : f α
   
  gb : g β

ExceptT.bind in Init.Control.Except

def withCounting (so : QueryImpl spec m) : QueryImpl spec (WriterT spec.QueryCount m) where
  impl | q => tell (QueryCount.single q.index) *> ↑(so.impl q)

instance : Extract Stream' where
  extract := Stream'.head

Option.isNone in Init.Data.Option.Basic

Option.elimM in Init.Data.Option.Basic

MonadFunctorT in Init.Prelude

@[reducible, inline] def uniformFin' (n m : ℕ) : OracleComp probSpec (Fin (m + 1)) :=
  probSpec.query m n

Finset.card in Mathlib.Data.Finset.Card

instance : Commutative PMF where
  bind_comm := fun ma mb => by admit /- proof elided -/

Function.const in Init.Prelude

@[inline, reducible]
def emptySpec : OracleSpec PEmpty := λ _ ↦ (PUnit, PUnit)

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

instance : Coapplicative NonEmptyList where

class MonadIso (m : Type u → Type v) (n : Type u → Type w) where
  toLift : MonadLiftT m n
  invLift : MonadLiftT n m
  monadLift_left_inv {α : Type u} :
    Function.LeftInverse (toLift.monadLift (α := α)) (invLift.monadLift (α := α))
  monadLift_right_inv {α : Type u} :
    Function.RightInverse (toLift.monadLift (α := α)) (invLift.monadLift (α := α))

DecidableEq in Init.Prelude

PFunctor.M.dest in Mathlib.Data.PFunctor.Univariate.M

WriterT.mk in Mathlib.Control.Monad.Writer

instance [MonadLift m m'] : MonadLift (StateT σ m) (StateT σ m') where
  monadLift x := StateT.mk fun s => liftM ((x.run) s)

instance subSpec_left_append_left_append_of_subSpec [h : spec₁ ⊂ₒ spec₃] :
    spec₁ ++ₒ spec₂ ⊂ₒ spec₃ ++ₒ spec₂ where
  monadLift
    | query (inl i) t => liftM (query i t)
    | query (inr i) t => query (inr i) t

def relabel (t : Tree' α) (n : ℕ) : Tree' ℕ × ℕ := match t with
  | .leaf _ => (.leaf n, n + 1)
  | .node l r =>
    let (l', n') := relabel l n
    let (r', n'') := relabel r n'
    (.node l' r', n'')

@[inline, reducible]
def singletonSpec (T U : Type v) : OracleSpec.{u,v} PUnit :=
  λ _ ↦ (T, U)

def tensorMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    {W : PFunctor.{uA₄, uB₄}} (l₁ : Lens P R) (l₂ : Lens Q W) :
    Lens.{max uA₁ uA₂, max uB₁ uB₂, max uA₃ uA₄, max uB₃ uB₄} (P ⊗ Q) (R ⊗ W) :=
  (fun ⟨pa, qa⟩ => (l₁.toFunA pa, l₂.toFunA qa)) ⇆
    (fun ⟨_pa, qa⟩ ⟨rb, wb⟩ => (l₁.toFunB _pa rb, l₂.toFunB qa wb))

instance : Coapplicative Zipper where
  coseq := coseq

OptionT in Init.Control.Option

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)

liftWith_pure {α : Type u} (a : α) :
    MonadControl.liftWith (m := m) (n := n) (fun _ => pure a) = pure a

instance [RelativeFunctor Id f] : Functor f where
  map := @mapᵣ Id f _
  mapConst := @mapConstᵣ Id f _

def validate_abuse_report (report : AbuseReport) (facebook_key : BitVec 256) : Bool :=
  let (msg_bv, _) := serialize_message_data report.message.content report.message.nonce
  let computed_tf := mock_hmac_sha256 report.message.nonce msg_bv
  let context_bv := BitVec.ofNat 256 report.context.timestamp
  let serialized := report.franking_tag.tag.append (bitvec_to_string context_bv)
  let computed_rf := mock_hmac_sha256 facebook_key (string_to_bitvec serialized)
  (computed_tf = report.franking_tag.tag) && (computed_rf = report.reporting_tag.tag)

@[always_inline, inline, simp]
abbrev MonadTransformer.liftOf [MonadTransformer t] (m) [Monad m] : m α → t m α :=
  (transform m).monadLift

def sumCompDistrib {R : PFunctor.{uA₃, uB₂}} :
    Lens.Equiv.{max uA₁ uA₂ uA₃ uB₂, max uB₁ uB₂, max uA₁ uA₂ uA₃ uB₂, max uB₁ uB₂}
      ((Q + R : PFunctor.{max uA₂ uA₃, uB₂}) ◃ P) ((Q ◃ P) + (R ◃ P)) where
  toLens := (fun a => match a with
              | ⟨Sum.inl qa, pf⟩ => Sum.inl ⟨qa, pf⟩
              | ⟨Sum.inr ra, pf⟩ => Sum.inr ⟨ra, pf⟩) ⇆
            (fun ⟨qr, pf⟩ b => match qr with
              | Sum.inl _ => b
              | Sum.inr _ => b)
  invLens := (fun a => match a with
              | Sum.inl ⟨qa, pf⟩ => ⟨Sum.inl qa, pf⟩
              | Sum.inr ⟨ra, pf⟩ => ⟨Sum.inr ra, pf⟩) ⇆
            (fun qprp b => match qprp with
              | Sum.inl _ => b
              | Sum.inr _ => b)
  left_inv := by admit /- proof elided -/

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 }

Classical.arbitrary in Mathlib.Logic.Nonempty

structure NonEmptyList (α : Type u) where
  head : α
  tail : List α

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

def IND_CPA_queryImpl (encAlg : AsymmEncAlg ProbComp M PK SK C)
    (pk : PK) (b : Bool) : QueryImpl encAlg.IND_CPA_oracleSpec
      (StateT (M × M →ₒ C).QueryCache ProbComp) :=
  have so : QueryImpl (M × M →ₒ C) ProbComp := ⟨fun (query () (m₁, m₂)) =>
    encAlg.encrypt pk (if b then m₁ else m₂)⟩
  idOracle ++ₛₒ so

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 : Functor Stream' where
  map := Stream'.map

def sumAssoc :
    Lens.Equiv.{max uA₁ uA₂ uA₃, uB, max uA₁ uA₂ uA₃, uB} ((P + Q) + R) (P + (Q + R)) where
  toLens := 
    Lens.sumPair
      (Lens.sumPair 
        (Lens.inl) 
        (Lens.inr ∘ₗ Lens.inl) 
      )
      (Lens.inr ∘ₗ Lens.inr) 
  invLens := 
    Lens.sumPair
      (Lens.inl ∘ₗ Lens.inl) 
      (Lens.sumPair 
        (Lens.inl ∘ₗ Lens.inr) 
        (Lens.inr) 
      )
  left_inv := by admit /- proof elided -/

Finite in Mathlib.Data.Finite.Defs

instance : CoeFun (NatHom m n) (λ _ ↦ {α : Type u} → m α → n α) where
  coe f {_} x := f.toFun x

instance : Monoid (QueryLog spec) where
  mul := List.append
  mul_assoc := List.append_assoc
  one := List.nil
  one_mul := List.nil_append
  mul_one := List.append_nil

class Monad.AssertAssume (m : Type u → Type v) [∀ α, Preorder (m α)] where
  assert_assume {α} : _root_.AssertAssume (m α)

@[always_inline, inline]
def lift (x : P.Obj α) : FreeM P α := FreeM.roll x.1 (fun y ↦ FreeM.pure (x.2 y))

List.filterMap in Init.Data.List.Basic

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

Stream'.get in Mathlib.Data.Stream.Defs

Array.mapM' in Init.Data.Array.BasicAux

instReprString in Init.Data.Repr

def uniformRegevAsymmEnc (n m p : ℕ) [hp2 : p.AtLeastTwo] [NeZero m]
    (χ : ℕ) (he : p > 4*(χ*m + 1)) :=
  regevAsymmEnc n m p (uniformErrSamp χ (relax_p_bound he))

PMF.instMonad in Mathlib.Probability.ProbabilityMassFunction.Monad

ENNReal in Mathlib.Data.ENNReal.Basic

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

def perfectSecrecy (encAlg : SymmEncAlg m M K C) : Prop :=
  ∀ mgen : ProbComp M, ∀ msg : M, ∀ σ : C,
    [= (msg, σ) | encAlg.exec do
      let msg' ← encAlg.lift_probComp mgen
      (msg', ·) <$> encAlg.encrypt (← encAlg.keygen) msg'] =
    [= msg | mgen]

def fixState {S : Type u} : Lens (selfMonomial S) (selfMonomial S ◃ selfMonomial S) :=
  (fun s₀ => ⟨s₀, fun s₁ => s₁⟩) ⇆ (fun _s₀ => fun ⟨_s₁, s₂⟩ => s₂)

def pi {I : Type v} (F : I → PFunctor.{uA, uB}) : PFunctor.{max uA v, max uB v} :=
  ⟨(i : I) → (F i).A, fun f => Σ i, (F i).B (f i)⟩

instance {w d} [Monad w] [DijkstraMonad w d] : MonadLiftT (fun α => (w : w α) × d w) w where
  monadLift x := x.1

def tensorOne : P ⊗ 1 ≃ₚ C P.A where
  equivA := Equiv.prodPUnit P.A
  equivB := fun _ => Equiv.equivPEmpty _

class Commutative (m : Type u → Type v) [Monad m] where
  bind_comm {α β} (ma : m α) (mb : m β) : CommutativeAt m ma mb

def zeroProd : 0 * P ≃ₚ 0 where
  equivA := Equiv.pemptyProd P.A
  equivB := fun a => a.1.elim

AddGroup in Mathlib.Algebra.Group.Defs

def PreCondition (σ : Type*) := σ → Prop

def LHL_Consequence_Game_0 (adv : LHL_Consequence_Adv n p) : ProbComp Bool := do
  let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
  let u ←$ᵗ Vector (Fin p) m
  let r2 ←$ᵗ Vector (Fin 2) m
  let r := (r2.map (Fin.castLE hp2.one_lt)).get
  adv (Vector.ofFn (Matrix.mulVec A r), dotProduct u.get r)

@[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)

instance (m : Type u → Type v) [Pure m] [Bind m] (n : Type u → Type w) [Pure n] [Bind n] :
    CoeFun (m →ᵐ n) (λ _ ↦ {α : Type u} → m α → n α) where
  coe f {_} x := f.toFun x

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

IO.println in Init.System.IO

instance : LawfulMonadTransformer (ReaderT ρ) where
  monad_functor := inferInstance
  liftOf_pure _ := rfl
  liftOf_bind _ _ := rfl

Array.foldlM in Init.Data.Array.Basic

def Hybrid_12_Reduction : LHL_Consequence_Adv n p := fun x => 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 b' ← adv.distinguish st x
  return b = b'

@[simps]
def inducedFunctor (M : RelativeMonad C D J) : EnrichedFunctor (Bundled c) C D where
  obj A := M.T A
  map f := sorry

instance : Commutative Id where
  bind_comm := fun _ _ => rfl

PEmpty.instIsEmpty in Mathlib.Logic.IsEmpty

protected def ulift (P : PFunctor.{uA, uB}) : PFunctor.{max uA vA, max uB vB} :=
  ⟨ULift P.A, fun a => ULift (P.B (ULift.down a))⟩

@[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)

def trans {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    (E : P ≃ₚ Q) (F : Q ≃ₚ R) : P ≃ₚ R where
  equivA := E.equivA.trans F.equivA
  equivB := fun a => (E.equivB a).trans (F.equivB (E.equivA a))

@[ext]
structure QueryImpl {ι : Type w} (spec : OracleSpec ι) (m : Type u → Type v) where
  impl {α : Type u} (q : OracleQuery spec α) : m α

def simulateQ [AlternativeMonad m] (so : QueryImpl spec m) (oa : OracleComp spec α) : m α :=
  do Option.getM (← FreeMonad.mapM oa.run so.impl)

Seq in Init.Prelude

Functor.map in Init.Prelude

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 -/

class Extract (w : Type u → Type v) where
   
  extract {α : Type u} : w α → α

alias fromZero := initial
alias toOne := terminal

T2Space in Mathlib.Topology.Separation.Hausdorff

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

def input : (q : OracleQuery spec α) → spec.domain q.index | query i t => t

structure RelativeMonad (J : C ⥤ D) where
   
  T : C → D
   
  η : ∀ {X}, J.obj X ⟶ T X
   
  μ : ∀ {X Y}, ((J.obj X) ⟶ (T Y)) → ((T X) ⟶ (T Y))
   
  left_unit : ∀ {X}, μ η = 𝟙 (T X) := by admit /- proof elided -/

def IND_CPA_queryImpl' (encAlg : AsymmEncAlg ProbComp M PK SK C)
    (pk : PK) (b : Bool) : QueryImpl encAlg.IND_CPA_oracleSpec
      (StateT (M × M →ₒ C).QueryCache ProbComp) :=
  have so : QueryImpl (M × M →ₒ C) ProbComp := ⟨fun (query () (m₁, m₂)) =>
    encAlg.encrypt pk (if b then m₁ else m₂)⟩
  idOracle ++ₛₒ so.withCaching

Decidable in Init.Prelude

String in Init.Prelude

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

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

instance [RelativeFunctor Id f] [LawfulRelativeFunctor Id f] : LawfulFunctor f where
  map_const := @map_constᵣ Id f _ _
  id_map := @id_mapᵣ Id f _ _
  comp_map := @comp_mapᵣ Id f _ _

liftWith_restoreM {α : Type u} (t : n α) :
    liftWith (m := m) (fun run => run t) >>= restoreM = t

OfNat.ofNat in Init.Prelude

structure NatHom (m : Type u → Type v) (n : Type u → Type w) where
  toFun : {α : Type u} → m α → n α

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 -/

instance : Unique (A 1) := inferInstanceAs (Unique PUnit)

def lift (q : OracleQuery spec α) : OracleComp spec α :=
  OptionT.lift (FreeMonad.lift q)

@[ext]
structure Equiv (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) where
  toLens : Lens P Q
  invLens : Lens Q P
  left_inv : comp invLens toLens = Lens.id P := by admit /- proof elided -/

alias coprod := sum

ReaderT.bind in Init.Prelude

Except in Init.Prelude

instance : Comonad Zipper where

associator in Mathlib.Algebra.Ring.Associator

structure MessagePackage where
  encrypted_message : EncryptedMessage
  franking_tag : FrankingTag
  reporting_tag : ReportingTag
  context : Context
  nonce : BitVec 256
  deriving Repr

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

instance {σ : Type*} : PartialOrder (PreCondition σ) where
  le P₁ P₂ := ∀ s, P₂ s → P₁ s
  le_refl P := by admit /- proof elided -/

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

def withPregen (so : QueryImpl spec m) : QueryImpl spec (ReaderT spec.QuerySeed m) where
  impl | query i t => do
    let seed ← read
    do match seed i with
      | u :: us => ReaderT.adapt (fun seed => seed.update i us) (return u)
      | [] => so.impl (query i t)

def prodMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    {W : PFunctor.{uA₄, uB₄}} (l₁ : Lens P R) (l₂ : Lens Q W) :
    Lens.{max uA₁ uA₂, max uB₁ uB₂, max uA₃ uA₄, max uB₃ uB₄} (P * Q) (R * W) :=
  (fun pq => (l₁.toFunA pq.1, l₂.toFunA pq.2)) ⇆
    (fun pq => Sum.elim (Sum.inl ∘ l₁.toFunB pq.1) (Sum.inr ∘ l₂.toFunB pq.2))

getThe in Init.Prelude

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

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

@[inline, reducible] def randomOracle [(i : ι) → SelectableType (spec.range i)] :
    QueryImpl spec (StateT spec.QueryCache (OracleComp unifSpec)) :=
  unifOracle.withCaching

instance instIsEmptySigma {α : Sort u} {β : α → Sort v} [inst : IsEmpty α] :
    IsEmpty ((a : α) ×' β a) where
  false := fun a => inst.elim a.1

StateM in Init.Control.State

monadMap_comp {α : Type u} (f : {β : Type u} → m β → m β) (g : {γ : Type u} → m γ → m γ) :
    (@monadMap m n _ α f) ∘ (@monadMap m n _ α g) = @monadMap m n _ α (f ∘ g)

class MonadAlgebra (m : Type u → Type v) where
  monadAlg {α : Type u} : m α → α

ENNReal.log in Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

@[reducible]
def QueryLog (spec : OracleSpec ι) : Type _ :=
  List ((i : ι) × spec.domain i × spec.range i)

AddTorsor in Mathlib.Algebra.AddTorsor.Defs

instance QueryImpl.Inhabited [∀ i, Inhabited (spec.range i)] [Pure m] :
  Inhabited (QueryImpl spec m) := ⟨{impl q := pure q.defaultOutput}⟩

Decidable.isFalse in Init.Prelude

instance : Coapplicative Stream' where

Vector.zero in Init.Data.Vector.Algebra

structure PureEquiv (m : Type u → Type v) [Pure m] (n : Type u → Type w) [Pure n]
    extends NatEquiv m n where
  map_pure' {α : Type u} (x : α) : toFun (pure x) = (pure x : n α)

modify in Init.Prelude

class CoseqRight (w : Type u → Type v) where
   
  coseqRight : {α β : Type u} → w α → w β → w β

instance instMonadSigma {w d} [Monad w] [DijkstraMonad w d] :
    Monad (fun α => (w : w α) × d w) where
  pure x := ⟨pure x, dPure x⟩
  bind x f := ⟨x.1 >>= (fun a => (f a).1), x.2 >>=ᵈ (fun a => (f a).2)⟩

instance {ω} {m} [Monad m] [Commutative m] [CommMonoid ω] : Commutative (WriterT ω m) where
  bind_comm := fun ma mb => by admit /- proof elided -/

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

instance instFunctor [Functor w] : Functor (StoreT s w) where
  map f storet := { runStoreT := Functor.map (fun g => f ∘ g) storet.runStoreT, pos := storet.pos }

instance : Coe (PureEquiv m n) (NatEquiv m n) where
  coe f := f.toNatEquiv

instance : Coe (PureEquiv m n) (PureHom m n) where
  coe f := ⟨f.toNatEquiv, f.map_pure'⟩

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

def generateSeed (spec : OracleSpec ι) [∀ i, SelectableType (spec.range i)]
    (qc : ι → ℕ) (js : List ι) : ProbComp (QuerySeed spec) := do
  let mut seed : QuerySeed spec := ∅
  for j in js do
    seed := seed.addValues (← ($ᵗ spec.range j).replicate (qc j))
  return seed

instance : Extend Id where
  extend wx f := f wx

Prod.map in Init.Core

CategoryTheory.aesop_cat in Mathlib.CategoryTheory.Category.Basic

instance : LawfulComonad NonEmptyList where
  map_eq_extend_extract := sorry 
  extend_extract := sorry 
  extract_extend := sorry 
  extend_assoc := sorry

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

inductive FreeM (f : Type v → Type w) (α : Type u) where
  | pure (a : α) : FreeM f α
  | roll {β : Type v} (x : f β) (k : β → FreeM f α) : FreeM f α

Or.inl in Init.Prelude

@[simps]
instance instProduct : EnrichedCategory V (C × D) where
  Hom X Y := (𝒞.Hom X.1 Y.1) ⊗ (𝒟.Hom X.2 Y.2)
  id X := (λ_ _).inv ≫ (sorry)
  
  comp X Y Z := by admit /- proof elided -/

instance support_fintype [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) :
    Fintype ↥oa.support :=

def LWE_Game_0 (adv : LWE_Adversary n m p) : ProbComp Bool := do
  let distr ← LWE_Distr n m p errSamp
  let b ← adv distr
  return b

instance : OracleSpec.DecidableEq []ₒ where
  domain_decidableEq' := inferInstance
  range_decidableEq' := inferInstance

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

def FreeMonad.toFreeContM : FreeMonad f α → FreeContM f α :=
  fun x => match x with
    | FreeMonad.pure a => fun _ handlePure => handlePure a
    | FreeMonad.roll x k => fun handleEff handlePure =>
      handleEff x (fun a => FreeMonad.toFreeContM (k a) handleEff handlePure)

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

noncomputable def unforgeableAdv.advantage
    {sigAlg : SignatureAlg (OracleComp spec) M PK SK S}
    (adv : unforgeableAdv sigAlg) : ℝ≥0∞ := [= true | unforgeableExp adv]

structure SigmaAlg
    (S W PC SC Ω P : Type) (p : S → W → Bool) where
   
  commit (s : S) (w : W) : ProbComp (PC × SC)
   
  respond (s : S) (w : W) (sc : SC) (ω : Ω) : ProbComp P
   
  verify (s : S) (pc : PC) (ω : Ω) (p : P) : Bool
   
  sim (s : S) : ProbComp PC
   
  extract (ω₁ : Ω) (p₁ : P) (ω₂ : Ω) (p₂ : P) : ProbComp W

def zeroTensor : 0 ⊗ P ≃ₗ 0 where
  toLens := (fun a => PEmpty.elim a.1) ⇆ (fun _ b => PEmpty.elim b)
  invLens := PEmpty.elim ⇆ (fun a _ => PEmpty.elim a)
  left_inv := by admit /- proof elided -/

CategoryTheory.inv in Mathlib.CategoryTheory.Iso

Monad in Init.Prelude

LawfulMonadLiftT in Init.Control.Lawful.MonadLift.Basic

structure SecAdv {ι : Type u} [DecidableEq ι]
    (spec : OracleSpec ι) (α β : Type u) where
  run : α → OracleComp spec β
  qb : ι → ℕ
  qb_isQueryBound (x : α) : IsQueryBound (run x) (qb)
  activeOracles : List ι
  mem_activeOracles_iff (i : ι) : i ∈ activeOracles ↔ qb i ≠ 0

deriving Repr, DecidableEq

def idOracle : QueryImpl spec (OracleComp spec) where impl q := OracleComp.lift q

List.nil in Init.Prelude

ExceptT.lift in Init.Control.Except

Functor.mapConst in Init.Prelude

One in Init.Prelude
</all_available_defs>

<all_available_lemmas>
@[simp]
lemma mem_support_evalDist_iff (oa : OracleComp spec α) (x : α) :
    some x ∈ (evalDist oa).run.support ↔ x ∈ oa.support

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

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

lemma probOutput_bind_eq_tsum (y : β) :
    [= y | oa >>= ob] = ∑' x : α, [= x | oa] * [= y | ob x]

lemma FreeContM.toFreeContM_toFreeMonad (x : FreeContM f α):
    @FreeMonad.toFreeContM f α (FreeContM.toFreeMonad x) = @x

@[simp] lemma evalDist_eq : evalDist p = p

@[simp]
lemma evalDist_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    evalDist (oa >>= ob) = (evalDist oa) >>= (evalDist ∘ ob)

lemma mem_support_eqRec_iff (oa : OracleComp spec α) (h : α = β) (y : β) :
    y ∈ (h ▸ oa).support ↔ h.symm ▸ y ∈ oa.support

@[simp] lemma purePower_A (B : Type u) : (purePower B).A = PUnit

lemma probOutput_generateSeed' [spec.FiniteRange]
    [DecidableEq spec.QuerySeed] (seed : QuerySeed spec)
    (h : seed ∈ (generateSeed spec qc js).support) : [= seed | generateSeed spec qc js] =
    ((generateSeed spec qc js).finSupport.card : ℝ≥0∞)⁻¹

lemma probOutput_bind_eq_tsum (y : β) :
    Pr[= y | mx >>= my] = ∑' x : α, Pr[= x | mx] * Pr[= y | my x]

@[simp]
lemma probOutput_guard {p : Prop} [Decidable p] :
    [= () | (guard p : OracleComp spec _)] = if p then 1 else 0

@[simp] -- NOTE: debatable if this should be simp
lemma guard_eq {ι : Type} {spec : OracleSpec ι} (p : Prop) [Decidable p] :
    (guard p : OracleComp spec Unit) = if p then pure () else failure

lemma probFailure_seq [spec.FiniteRange] :
    [⊥ | og <*> oa] = [⊥ | og] + [⊥ | oa] - [⊥ | og] * [⊥ | oa]

lemma probEvent_eq_tsum_indicator (oa : OracleComp spec α) (p : α → Prop) :
    [p | oa] = ∑' x : α, {x | p x}.indicator ([= · | oa]) x

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

@[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

lemma probOutput_seq_map_prod_mk_eq_mul :
    [= (x, y) | Prod.mk <$> oa <*> ob] = [= x | oa] * [= y | ob]

example : support (do
    let b ← coin; let b' ← coin
    let x ← (if b && b' then return 0 else return 1);
    let z ← (if b && b' then return x else return 0);
    return (x * z)) = {0}

@[simp] lemma probOutput_ne_top : Pr[= x | mx] ≠ ∞

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

lemma probOutput_bind_of_const (y : β) (r : ℝ≥0∞) (h : ∀ x, [= y | ob x] = r) :
    [= y | oa >>= ob] = (1 - [⊥ | oa]) * r

@[simp] lemma probFailure_uniformSelectList (xs : List α) :
    [⊥ | $ xs] = if xs.isEmpty then 1 else 0

@[simp]
lemma construct_pure (y : α) : FreeMonad.construct h_pure h_roll (pure y) = h_pure y

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

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

@[simp]
lemma probEvent_failure (p : α → Prop) :
    [p | (failure : OracleComp spec α)] = 0

lemma probOutput_map_eq_tsum (y : β) :
    [= y | f <$> oa] = ∑' x, [= x | oa] * [= y | (pure (f x) : OracleComp spec β)]

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

lemma cacheQuery_eq_ite_ite (i : ι) (t : spec.domain i) (u : spec.range i) :
    cache.cacheQuery i t u = λ j t' ↦
      if h : j = i then (if h ▸ t' = t then some (h ▸ u) else cache j t') else cache j t'

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

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

@[simp] lemma selfMonomial_unit : selfMonomial PUnit = X

@[simp] lemma simulateQ_comp_pure_comp (f : α → β) : simulateQ so ∘ pure ∘ f = pure ∘ f

lemma mem_support_iff_probOutput_ne_zero : x ∈ oa.support ↔ [= x | oa] ≠ 0

@[simp] lemma support_uniformSelectFinset [DecidableEq α] (s : Finset α) :
    ($ s).support = if s.Nonempty then ↑s else ∅

@[simp] theorem Finset.image_const_univ {α β} [DecidableEq β]  [Fintype α]
    [Nonempty α] (b : β) : (Finset.univ.image fun _ : α => b) = singleton b

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

lemma monad_pure_def [Monad m] (x : α) :
    (pure x : StateT σ m α) = StateT.pure x

@[simp] lemma monoid_one_def :
    (@OfNat.ofNat (QueryCount spec) 1 (@One.toOfNat1 _ (Monoid.toOne))) = (0 : ι → ℕ)

@[simp] lemma evalDist_liftM [superSpec.FiniteRange] [Fintype α] [Nonempty α]
    (q : OracleQuery spec α) :
    evalDist (q : OracleComp superSpec α) =
      OptionT.lift (PMF.uniformOfFintype α)

theorem Option.cast_eq_some_iff {α β : Type u} {x : Option α} {b : β} (h : α = β) :
    cast (congrArg Option h) x = some b ↔ x = some (cast h.symm b)

lemma mem_support_seq_map_iff_of_injective2 (hf : f.Injective2) (x : α) (y : β) :
    f x y ∈ (f <$> oa <*> ob).support ↔ x ∈ oa.support ∧ y ∈ ob.support

lemma probOutput_ne_zero' [DecidableEq α] (h : x ∈ oa.finSupport) : [= x | oa] ≠ 0

@[simp] theorem liftM_optional [AlternativeMonad m] [AlternativeMonad n]
    [LawfulMonad m] [LawfulMonad n] [MonadLift m n] [LawfulAlternativeLift m n]
    [LawfulMonadLift m n]
    (x : m α) : liftM (optional x) = optional (liftM x : n α)

@[simp] lemma evalDist_eq : evalDist p = liftM p

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

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

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

lemma tsum_option {α β : Type*} [AddCommMonoid α] [TopologicalSpace α]
    [ContinuousAdd α] [T2Space α]
    (f : Option β → α) (hf : Summable (Function.update f none 0)) :
    ∑' x : Option β, f x = f none + ∑' x : β, f (some x)

lemma probOutput_seq_map_eq_mul_of_injective2 [spec.FiniteRange]
    (hf : f.Injective2) (x : α) (y : β) :
    [= f x y | f <$> oa <*> ob] = [= x | oa] * [= y | ob]

@[simp low + 1]
lemma finSupport_seq_map_eq_image2 [spec.FiniteRange] [spec.DecidableEq]
    [DecidableEq α] [DecidableEq β] [DecidableEq γ] :
    (f <$> oa <*> ob).finSupport = Finset.image₂ f oa.finSupport ob.finSupport

@[simp]
lemma BitVec.xor_xor_cancel_right {n : ℕ} (bv1 bv2 : BitVec n) :
    bv1 ^^^ bv2 ^^^ bv2 = bv1

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

@[simp] lemma simulateQ_ite (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) :
    simulateQ so (ite p oa oa') = ite p (simulateQ so oa) (simulateQ so oa')

@[simp]
lemma construct_pure (y : α) : FreeM.construct h_pure h_roll (pure y) = h_pure y

lemma probOutput_bind_congr_le_add {γ₁ γ₂ : Type u}
    {oa : OracleComp spec α} {ob : α → OracleComp spec β}
      {oc₁ : α → OracleComp spec γ₁} {oc₂ : α → OracleComp spec γ₂}
    {y : β} {z₁ : γ₁} {z₂ : γ₂}
    (h : ∀ x ∈ oa.support, [= y | ob x] ≤ [= z₁ | oc₁ x] + [= z₂ | oc₂ x]) :
    [= y | oa >>= ob] ≤ [= z₁ | oa >>= oc₁] + [= z₂ | oa >>= oc₂]

@[simp] theorem monadLift_mono' {m n} [OrderedMonad m] [OrderedMonad n] [OrderedMonadLiftT m n]
    {α} {a b : m α} (h : a ≤ₘ b) : monadLift a ≤ₘ (monadLift b : n α)

@[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 query_bind_ne_failure : (q : OracleComp spec β) >>= oa ≠ failure

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

@[simp] lemma support_uniformFin (n : ℕ) : ($[0..n]).support = Set.univ

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

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

@[simp]
lemma probEvent_uniformFin (p : Fin (n + 1) → Prop) [DecidablePred p] :
    [p | $[0..n]] = (Finset.univ.filter p).card * (n + 1 : ℝ≥0∞)⁻¹

@[simp] lemma finSupport_uniformSelectFinset [DecidableEq α] (s : Finset α) :
    ($ s).finSupport = if s.Nonempty then s else ∅

@[simp]
lemma fst_map_run_simulateQ (oa : OracleComp spec α) :
    Prod.fst <$> (simulateQ countingOracle oa).run = oa

lemma probOutput_bind_eq_sum_finSupport [spec.DecidableEq] [DecidableEq α] (y : β) :
    [= y | oa >>= ob] = ∑ x ∈ oa.finSupport, [= x | oa] * [= y | ob x]

@[simp]
lemma support_orElse {ι : Type u} {spec : OracleSpec ι} {α : Type u}
    (oa oa' : OracleComp spec α) [Decidable oa.neverFails] : (oa <|> oa').support =
      if oa.neverFails then oa.support else oa.support ∪ oa'.support

lemma X_eq_purePower_pUnit : X = purePower PUnit

protected lemma orElse_def (oa oa' : OracleComp spec α) : (oa <|> oa') = OptionT.mk
      (do match ← OptionT.run oa with | some a => pure (some a) | _  => OptionT.run oa')

@[simp] lemma support_map_prod_map_fork : (Prod.map cf cf <$> main.fork qb js i cf).support =
    (fun s => (s, s)) '' (cf <$> main).support

@[simp]
lemma generateSeed_cons : generateSeed spec qc (j :: js) =
    ($ᵗ (spec.range j)).replicate (qc j) >>= λ xs ↦
      generateSeed spec qc js

@[simp] lemma probOutput_none_map_fork_right (s : Option (Fin (qb i + 1))) :
    [= (s, none) | Prod.map cf cf <$> main.fork qb js i cf] = 0

lemma probOutput_seq_map_prod_mk_eq_mul' :
    [= (x, y) | (λ x y ↦ (y, x) : β → α → α × β) <$> ob <*> oa] = [= x | oa] * [= y | ob]

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

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

@[simp]
theorem prodComm_symm : (prodComm P Q).symm = prodComm Q P

@[simp] lemma probFailure_eq : probFailure p = 0

theorem probFailure_fork_le :
    let acc : ℝ≥0∞ := ∑ s, [= some s | cf <$> main]
    let h : ℝ≥0∞ := Fintype.card (spec.range i)
    let q := qb i + 1
    [⊥ | fork main qb js i cf] ≤ 1 - acc * (acc / q - h⁻¹)

@[simp] lemma neverFails_list_filterMapM {f : α → OracleComp spec (Option β)} {as : List α}
    (h : ∀ x ∈ as, neverFails (f x)) : neverFails (filterMapM f as)

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

lemma query_eq_pure_iff_false : (q : OracleComp spec β) = pure y ↔ False

lemma probEvent_comp (q : β → Prop) : [q ∘ f | oa] = [q | f <$> oa]

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

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

lemma X_eq_linear_pUnit : X = linear PUnit

protected lemma bind_congr' {oa oa' : OracleComp spec α} {ob ob' : α → OracleComp spec β}
    (h : oa = oa') (h' : ∀ x, ob x = ob' x) : oa >>= ob = oa' >>= ob'

@[simp] lemma apply_eq_run_some (p : SPMF α) (x : α) : p x = p.run (some x)

@[simp] lemma finSupportWhen_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β)
    [DecidableEq α] [DecidableEq β] :
    (oa >>= ob).finSupportWhen fin_poss =
      (oa.finSupportWhen fin_poss).biUnion fun x => (ob x).finSupportWhen fin_poss

theorem Correct [DecidableEq P] : (elgamalAsymmEnc G P).PerfectlyCorrect

lemma depth_bind_le {x : FreeMonad f α} {g : α → FreeMonad f β} :
    depth (x >>= g) ≤ depth x + iSup (λ u ↦ depth (g u))

@[simp]
lemma monad_pure_def (x : α) : (pure x : FreeM P α) = FreeM.pure x

lemma neverFails_eq_oracleComp_construct (oa : OracleComp spec α) :
    oa.neverFails = OracleComp.construct
      (fun _ ↦ True) (fun {β} _ _ r ↦ ∀ (x : β), r x) False oa

@[simp] lemma C_unit : C PUnit = 1

@[simp]
lemma liftM_query_stateT {σ : Type v} {α : Type v} (q : OracleQuery spec α) :
  (liftM q : StateT σ (OracleComp spec) α) = liftM (liftM q : OracleComp spec α)

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

lemma probEvent_eqRec (q : β → Prop) :
    [q | h ▸ oa] = [λ x ↦ q (h ▸ x) | oa]

lemma apply_eq_apply_of_mem_support_fork (x₁ x₂ : α)
    (h : (x₁, x₂) ∈ (fork main qb js i cf).support) : cf x₁ = cf x₂

@[simp]
lemma Fin_Bound_add {n b₁ b₂ : ℕ} {x y : Fin n} (h₁ : Fin_Bound x b₁)
 (h₂ : Fin_Bound y b₂) : Fin_Bound (x + y) (b₁ + b₂)

lemma liftM_query_eq_liftM_liftM {m : Type v → Type z} [MonadLift (OracleComp spec) m] {α : Type v}
    (q : OracleQuery spec α) : (liftM q : m α) = liftM (liftM q : OracleComp spec α)

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

lemma uniformSelectVector_def {α : Type} {n : ℕ} (xs : Vector α (n + 1)) :
    ($ xs) = ($ xs.toList)

@[simp] theorem comonad_id_map {α : Type u} (wa : w α) : Functor.map id wa = wa

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

lemma probOutput_map_eq_tsum_subtype (y : β) :
    [= y | f <$> oa] = ∑' x : {x ∈ oa.support | y = f x}, [= x | oa]

lemma probOutput_true_eq_probOutput_false_not {ob : OracleComp spec Bool} :
    [= true | ob] = [= false | do let b ← ob; return !b]

@[simp] lemma tsum_run_some_ne_top (p : SPMF α) :
    ∑' x, p.run (some x) ≠ ⊤

@[simp] lemma PerfectlyCorrect_iff (encAlg : AsymmEncAlg m M PK SK C) :
    PerfectlyCorrect encAlg ↔ ∀ (msg : M),
      [⊥ | CorrectExp encAlg msg] = 0

@[simp] lemma neverFails_array_mapM {f : α → OracleComp spec β} {as : Array α}
    (h : ∀ x ∈ as, neverFails (f x)) : neverFails (mapM f as)

theorem RelativeFunctor.map_unitᵣ [RelativeMonad j m] [LawfulRelativeMonad j m] {a : m PUnit} :
    (fun y : j PUnit => y) <$>ᵣ a = a

@[simp] lemma supportWhen_query (q : OracleQuery spec α) :
    (q : OracleComp spec α).supportWhen poss = poss q

@[simp]
lemma finSupport_simulateQ [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α]
    (oa : OracleComp spec α) : (simulateQ unifOracle oa).finSupport = oa.finSupport

lemma probEvent_eq_tsum_subtype_mem_support :
    [p | oa] = ∑' x : {x ∈ oa.support | p x}, [= x | oa]

@[simp]
theorem liftM_elimM [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
    [MonadLift m n] [LawfulMonadLift m n] (x : m (Option α)) (y : m β) (z : α → m β) :
      liftM (Option.elimM x y z) = Option.elimM (x : n (Option α)) (y) (fun x => z x)

@[simp] lemma tsum_probOutput_add_probFailure (oa : m α) :
    ∑' x, Pr[= x | oa] + Pr[⊥ | oa] = 1

@[simp] lemma support_coin : coin.support = {true, false}

@[simp] lemma not_one_lt_probFailure : ¬ 1 < Pr[⊥ | mx]

@[simp]
lemma liftM_query_writerT {ω : Type v} [Monoid ω] {α : Type v} (q : OracleQuery spec α) :
  (liftM q : WriterT ω (OracleComp spec) α) = liftM (liftM q : OracleComp spec α)

lemma ProbComp.advantage_eq_half_sub_probFailure (p : ProbComp Unit) :
    p.advantage = |1 / 2 - ([⊥ | p]).toReal

lemma mul_abs_of_nonpos (h : a < 0) : a * |b

@[simp]
lemma mem_support_evalDist_iff' [spec.DecidableEq] [DecidableEq α]
    (oa : OracleComp spec α) (x : α) :
    some x ∈ (evalDist oa).run.support ↔ x ∈ oa.finSupport

@[simp] lemma probOutput_ne_top : [= x | oa] ≠ ∞

@[simp] lemma support_eqRec (oa : OracleComp spec α) (h : α = β) :
    (h ▸ oa).support = h.symm ▸ oa.support

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

lemma mem_support_iff_of_evalDist_eq {oa : OracleComp spec α} {oa' : OracleComp spec' α}
    (h : evalDist oa = evalDist oa') (x : α) : x ∈ oa.support ↔ x ∈ oa'.support

lemma probOutput_query (u : spec.range i) :
    [= u | (query i t : OracleComp spec _)] = (Fintype.card (spec.range i) : ℝ≥0∞)⁻¹

theorem IND_CPA_advantage_eq_parallelTesting_advantage [DecidableEq G] [DecidableEq P]
    (adversary : (elgamalAsymmEnc G P).IND_CPA_adversary) :
    (IND_CPA_advantage adversary) =
      (parallelTestingAdvantage (IND_CPA_parallelTesting_reduction adversary))

@[simp]
lemma snd_map_prod_mk_of_subsingleton [Subsingleton α]
    (ob : OracleComp spec β) (x : α) : snd <$> (x, ·) <$> ob = ob

@[simp]
lemma probFailure_add_tsum_probOutput (oa : OracleComp spec α) :
    [⊥ | oa] + ∑' x, [= x | oa] = 1

lemma probFailure_eq_sub_probEvent (oa : OracleComp spec α) :
    [⊥ | oa] = 1 - [λ _ ↦ true | oa]

lemma simulateQ_eq [spec.FiniteRange] (oa : OracleComp spec α) :
    simulateQ defaultOracle oa = oa.defaultResult.getM

protected lemma liftM_def (q : OracleQuery spec α) :
    (q : OracleComp spec α) = OptionT.lift (FreeMonad.lift q)

@[simp]
lemma liftM_eq_liftComp (oa : OracleComp spec α) :
    (liftM oa : OracleComp superSpec α) = liftComp oa superSpec

lemma probOutput_map_eq_probOutput_inverse (f : α → β) (g : β → α)
    (hl : Function.LeftInverse f g) (hr : Function.RightInverse f g)
    (y : β) : [= y | f <$> oa] = [= g y | oa]

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

theorem bind_comm_triple_swap_12 {m} [Monad m] [LawfulMonad m] [Commutative m] {α β γ δ}
    (ma : m α) (mb : m β) (mc : m γ) (f : α × β × γ → m δ) :
    (do let a ← ma; let b ← mb; let c ← mc; f (a, b, c)) =
    (do let b ← mb; let a ← ma; let c ← mc; f (a, b, c))

theorem get_set {s : σ} : (do StateT.set (m := m) s; StateT.get) = (do StateT.set s; pure s)

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

lemma evalDist_lift_query [superSpec.FiniteRange] [Fintype α] [Nonempty α]
    (q : OracleQuery spec α) :
    evalDist ((q : OracleQuery superSpec α) : OracleComp superSpec α) =
      OptionT.lift (PMF.uniformOfFintype α)

@[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 evalDist_uniformOfFintype [Fintype α] [Inhabited α] :
    evalDist ($ᵗ α) = OptionT.lift (PMF.uniformOfFintype α)

lemma mapM_bind [LawfulMonad m] (oa : OracleComp spec α) (ob : α → OracleComp spec β)
    (hfail : ∀ f : α → m β, fail >>= f = fail) :
    (oa >>= ob).mapM fail qm =
      oa.mapM fail qm >>= λ x ↦ (ob x).mapM fail qm

lemma ProbComp.advantage_eq_half_of_sub (p : ProbComp Unit) :
    p.advantage = 2⁻¹ * |([⊥ | p]).toReal - ([= () | p]).toReal

@[simp]
lemma depth_roll {x : f α} {r : α → FreeMonad f β} :
    depth (roll x r : FreeMonad f β) = 1 + iSup (λ u ↦ depth (r u))

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

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

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))

@[simp]
lemma coe_finSupport [spec.FiniteRange] [DecidableEq α]
    (oa : OracleComp spec α) : ↑oa.finSupport = oa.support

lemma mul_abs_of_nonneg (h : 0 ≤ a) : a * |b
</all_available_lemmas>

<local_ctx>
import VCVio.OracleComp.DistSemantics.Monad

namespace OracleComp

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

variable (oa : OracleComp spec α) (og : OracleComp spec (α → β))

section seq_map

variable (oa : OracleComp spec α) (ob : OracleComp spec β) (f : α → β → γ)

section swap

end swap

section injective2

end injective2
</local_ctx>

<target_theorem>
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] :=
</target_theorem>

