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>
structure Lens (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) where
  toFunA : P.A → Q.A
  toFunB : ∀ a, Q.B (toFunA a) → P.B a

structure Chart (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) where
  toFunA : P.A → Q.A
  toFunB : ∀ a, P.B a → Q.B (toFunA a)

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

structure SecretMessage where
  content : String
  nonce : BitVec 256
  deriving Repr

Id in Init.Control.Id

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

instReprString in Init.Data.Repr

CategoryTheory.EnrichedCategory in Mathlib.CategoryTheory.Enriched.Basic

def fst {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} :
    Lens.{max uA₁ uA₂, max uB₁ uB₂, uA₁, uB₁} (P * Q) P :=
  Prod.fst ⇆ (fun _ => Sum.inl)

def negligible (f : ℕ → ℝ≥0∞) : Prop :=
  SuperpolynomialDecay atTop (λ x ↦ ↑x) f

Equiv.Perm in Mathlib.Logic.Equiv.Defs

def cast {P Q : PFunctor.{uA, uB}} (hA : P.A = Q.A) (hB : ∀ a, P.B a = Q.B (cast hA a)) :
    P ≃ₚ Q where
  equivA := _root_.Equiv.cast hA
  equivB := fun a => _root_.Equiv.cast (hB a)

CategoryTheory.NatTrans.mk in Mathlib.CategoryTheory.NatTrans

Unit in Init.Prelude

ReaderT.adapt in Init.Prelude

structure SignatureAlg (m : Type → Type v) (M PK SK S : Type)
    extends ExecutionMethod m where
  keygen : m (PK × SK)
  sign (pk : PK) (sk : SK) (msg : M) : m S
  verify (pk : PK) (msg : M) (σ : S) : m Bool

example {σ} : StateT σ (MonoContProp) = fun α => σ → MonoContProp (α × σ) := rfl

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

instance : MonadLift P (FreeM P) where
  monadLift x := FreeM.lift x

def IND_CPA_parallelTesting_reduction
    (adversary : (elgamalAsymmEnc G P).IND_CPA_adversary) :
    parallelTestingAdversary G P := fun x x₁ x₂ x₃ => do
  let so : QueryImpl (P × P →ₒ P × P) ProbComp := ⟨fun (query () (m₁, _m₂)) =>
    return (x₂, m₁ * x₃)⟩
  simulateQ (idOracle ++ₛₒ so) (adversary (x, x₁))

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

def mock_hmac_sha256_out_type : Type := String

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

instance {comp : StateM σ α} {Q : PostCondition σ α} :
    Subsingleton (WeakestPrecondition comp Q) :=

instance instComonad [Comonad w] : Comonad (StoreT s w) where

List.filterMap in Init.Data.List.Basic

instance hasEvalDist : HasEvalDist SPMF where
  evalDist := id
  evalDist_pure _ := rfl
  evalDist_bind _ _ := rfl

Function.uncurry in Init.Data.Function

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

@[simp] def head_nel (nel : NonEmptyList α) : α := nel.head

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

dite in Init.Prelude

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

Functor.mapConst in Init.Prelude

Fin.sub in Init.Data.Fin.Basic

def zeroComp : 0 ◃ P ≃ₚ 0 where
  equivA := Equiv.equivPEmpty _
  equivB := fun a => a.1.elim

Set in Mathlib.Data.Set.Defs

instance : Inhabited (OracleSpec ι) := ⟨λ _ ↦ (PUnit, PUnit)⟩

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

instance : Functor NonEmptyList where
  map := NonEmptyList.map

class LawfulRelativeMonad (j : Type u → Type w) (m : Type u → Type v)
    [RelativeMonad j m] extends LawfulRelativeFunctor j m where

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

HAdd in Init.Prelude

ContinuousAdd in Mathlib.Topology.Algebra.Monoid.Defs

MonadControl in Init.Control.Basic

def isFailure {α : Type v} : OracleComp spec α → Bool
  | FreeMonad.pure x => Option.isNone x
  | _ => false

class StrongestPostcondition (P : PreCondition σ) (comp : StateM σ α) where
  Q : PostCondition σ α
  hQ : HoareTriple P comp Q
  hStrong : ∀ Q', HoareTriple P comp Q' → Q' ≤ Q

def coseq (za : Zipper α) (zb : Zipper β) : Zipper (α × β) :=
  sorry

ULift in Init.Prelude

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)

Set.image in Mathlib.Data.Set.Defs

class RelativeMonad (j : Type u → Type w) (m : Type u → Type v)
    extends RelativePure j m, RelativeBind j m, RelativeFunctor j m where
  mapᵣ f x := bindᵣ x (pureᵣ ∘ f)

structure FrankingTag where
  tag : mock_hmac_sha256_out_type 
  deriving Repr

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

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

class Complete (encAlg : SymmEncAlg m M K C) : Prop where
  decrypt_encrypt_eq_message (msg : M) : [= some msg | encAlg.exec
    do let k ← encAlg.keygen; return encAlg.decrypt k (← encAlg.encrypt k msg)] = 1

instance : Comonad (Prod ε) where

def XComp : X ◃ P ≃ₚ P where
  equivA := (_root_.Equiv.uniqueSigma _).trans (Equiv.punitArrowEquiv P.A)
  equivB := fun _ => by admit /- proof elided -/

def Hybrid_1 : ProbComp Bool := do
  let b ←$ᵗ Bool
  let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
  let u ←$ᵗ Vector (Fin p) m
  let ⟨m₁, m₂, st⟩ ← adv.chooseMessages (A, u)
  let c ← if b then (uniformRegevAsymmEnc n m p χ he).encrypt (A, u) m₁
    else (uniformRegevAsymmEnc n m p χ he).encrypt (A, u) m₂
  let b' ← adv.distinguish st c
  return b = b'

def map (f : α → β) : NonEmptyList α → NonEmptyList β
  | ⟨h, t⟩ => ⟨f h, List.map f t⟩

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

instance instOfLawfulMonadLiftT {m n} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] :
    LawfulMonadRelation m n where
  monadRel_pure _ := by admit /- proof elided -/

instance : EmptyCollection (QueryCache spec) := ⟨fun _ _ => none⟩

Alternative in Init.Control.Basic

instance [Comonad f] [Comonad g] : Comonad (Day f g) where
  extract {a : Type u₃} := extract
  extend {a b : Type u₃} (day : Day f g a) (k : Day f g a → b) : Day f g b :=
    sorry 
    
  coseq {a b : Type u₃} := coseq

Sum.map in Init.Data.Sum.Basic

Equiv.pemptyArrowEquivPUnit in Mathlib.Logic.Equiv.Defs

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 }

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

def sumMap {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₂, uB₁, max uA₃ uA₄, uB₃} (P + Q) (R + W) :=
  (Sum.map l₁.toFunA l₂.toFunA) ⇆
    (fun psum => match psum with
      | Sum.inl pa => l₁.toFunB pa
      | Sum.inr qa => l₂.toFunB qa)

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

MonadControl.restoreM in Init.Control.Basic

Prod.fst in Init.Prelude

liftWith_bind {α β : Type u} (ma : m α) (f : α → m β) :
    liftWith (fun _ => ma) >>= liftWith ∘ (fun a _ => f a) = liftWith (n := n) (fun _ => ma >>= f)

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

List.foldlM in Init.Data.List.Control

class DijkstraMonad (w : Type u → Type v) (d : {α : Type u} → w α → Type z) [Monad w] where
  
  dPure {α : Type u} : (x : α) → d (pure x)
  dBind {α β : Type u} {wa : w α} {wb : α → w β} : d wa → ((a : α) → d (wb a)) → d (wa >>= wb)

instance : FiniteRange []ₒ where
  range_inhabited' := inferInstance
  range_fintype' := inferInstance

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

cast in Init.Prelude

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

example : Hybrid_0 adv = IND_CPA_OneTime_Game adv :=

protected def mapM' (m : Type u → Type w) [Monad m] [LawfulMonad m]
    (s : {α : Type u} → f α → m α) : FreeMonad f →ᵐ m where
  toFun := FreeMonad.mapM_aux s
  toFun_pure' x := rfl
  toFun_bind' x y := by admit /- proof elided -/

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

HMul in Init.Prelude

instance {P} {a : (P ⊗ 1).A} : IsEmpty ((P ⊗ 1).B a) :=

Inhabited in Init.Prelude

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

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

let invalid_abuse_report := {
      message := {
        content := manipulated_message,
        nonce := data.verified_msg.nonce },
      franking_tag := data.message_package.franking_tag,
      reporting_tag := data.message_package.reporting_tag,
      context := data.message_package.context }
    let is_invalid := validate_abuse_report invalid_abuse_report data.facebook_key
    IO.println s!"false abuse report validation result: {is_invalid}"

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'

instance decidablePred_mem_support [spec.FiniteRange] [hα : DecidableEq α]
    (oa : OracleComp spec α) : DecidablePred (· ∈ oa.support) :=

IO.rand in Init.Data.Random

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⟩

Prod.mk in Init.Prelude

instance [Inhabited (f α)] : Inhabited (FreeMonad f α) := ⟨FreeMonad.lift default⟩

@[simp]
def compNth (P : PFunctor.{uA, uB}) : Nat → PFunctor.{max uA uB, uB}
  | 0 => X
  | Nat.succ n => P ◃ compNth P n

def addValues [DecidableEq ι] {i : ι}
    (us : List (spec.range i)) (seed : QuerySeed spec) : QuerySeed spec :=
  Function.update seed i (seed i ++ us)

def takeAtIndex [DecidableEq ι] (seed : QuerySeed spec) (i : ι) (n : ℕ) : QuerySeed spec :=
  Function.update seed i ((seed i).take n)

Function.LeftInverse in Init.Data.Function

Equiv.sigmaUnique in Mathlib.Logic.Equiv.Prod

structure BindHom (m : Type u → Type v) [Bind m] (n : Type u → Type w) [Bind n]
    extends NatHom m n where
  toFun_bind' {α β : Type u} (x : m α) (y : α → m β) :
    toFun (x >>= y) = toFun x >>= (fun a => toFun (y a))

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

def fork (main : OracleComp spec α)
    (qb : ι → ℕ) (js : List ι) (i : ι)
    (cf : α → Option (Fin (qb i + 1))) :
    OracleComp spec (α × α) := do
  let seed ← generateSeed spec qb js
  let x₁ ← (simulateQ seededOracle main).run seed
  let s : Fin (qb i + 1) ← (cf x₁).getM
  let u ←$ᵗ spec.range i 
  guard ((seed i)[s + 1]? ≠ some u) 
  let seed' := (seed.takeAtIndex i s).addValue i u
  let x₂ ← (simulateQ seededOracle main).run seed'
  guard (cf x₂ = some s) 
  return (x₁, x₂)

class Coapplicative (w : Type u → Type v) extends
    Functor w, Extract w, Coseq w, CoseqLeft w, CoseqRight w where
   
  coseqLeft wa wb := Functor.map Prod.fst (coseq wa wb)
   
  coseqRight wa wb := Functor.map Prod.snd (coseq wa wb)

def tail (t : CofreeC F α) : F (CofreeC F α) :=
  let d := M.dest t       
  ⟨d.1.2, d.2⟩

def compX : P ◃ X ≃ₚ P where
  equivA := Equiv.sigmaUnique P.A (fun a => P.B a → PUnit.{_ + 1})
  equivB := fun _ => _root_.Equiv.sigmaPUnit _

liftWith_bind {α β : Type u} (ma : m α) (f : α → m β) :
    MonadControl.liftWith (fun _ => ma) >>= MonadControl.liftWith ∘ (fun a _ => f a) =
        MonadControl.liftWith (n := n) (fun _ => ma >>= f)

def rangeDecidableEq [spec.DecidableEq] : OracleQuery spec α → DecidableEq α
  | query i t => inferInstance

class LawfulMonadStateOf (σ : outParam (Type u)) (m : Type u → Type v) [Monad m] [MonadStateOf σ m]
    : Prop where

comp_mapᵣ {α β γ : Type u} (g : j α → j β) (h : j β → j γ) (x : f α) :
    (h ∘ g) <$>ᵣ x = h <$>ᵣ g <$>ᵣ x

Finset.filter in Mathlib.Data.Finset.Filter

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

optional in Init.Control.Basic

instance instOfMonadLiftT {m n} [MonadLiftT m n] : MonadRelation m n where
  monadRel := fun ma na => liftM ma = na

instance instCoapplicative [Comonad w] : Coapplicative (StoreT s w) where

def IND_CCA_oracleImpl [DecidableEq C] (encAlg : AsymmEncAlg m M PK SK C)
    (pk : PK) (sk : SK) (b : Bool) : QueryImpl (IND_CCA_oracleSpec encAlg)
      (StateT (Option C) m) where impl
  | query (Sum.inl ()) c => do
      guard ((← get) ≠ some c)
      return encAlg.decrypt sk c
  | query (Sum.inr ()) (m₁, m₂) => do
      guard (← get).isNone
      let c ← encAlg.encrypt pk (if b then m₁ else m₂)
      set (some c)
      return c

alias fromZero := initial
alias toOne := terminal

ExceptT.lift in Init.Control.Except

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

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

def purePower (B : Type uB) : PFunctor.{uA, uB} :=
  PUnit X^ B

ExceptT.bind in Init.Control.Except

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

instance : Functor Zipper where
  map := map

def string_to_bitvec (s : String) : BitVec 256 :=
  s.foldl (λ acc c => (acc.shiftLeft 8) + BitVec.ofNat 256 c.toNat) 0

instance [h₁ : spec₁.DecidableEq] [h₂ : spec₂.DecidableEq] :
    (spec₁ ++ₒ spec₂).DecidableEq where
  domain_decidableEq' := Sum.rec h₁.domain_decidableEq' h₂.domain_decidableEq'
  range_decidableEq' := Sum.rec h₁.range_decidableEq' h₂.range_decidableEq'

def PFunctor.FreeContM (P : PFunctor.{z, y}) (α : Type w) : Type _ :=
  FreeContT P Id.{u} α

set_get : (do let s ← MonadStateOf.get (m := m); set (σ := σ) s) = pure ⟨⟩

Vector.zero in Init.Data.Vector.Algebra

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 deserialize_message_data (data : BitVec 256 × BitVec 256) : String × BitVec 256 :=
  let (msg_bv, nonce) := data
  (bitvec_to_string msg_bv, nonce)

@[inline] def pure (a : α) : FreeContT f m α :=
  fun _ handlePure => handlePure a

alias fromZero := initial
alias toOne := terminal

LawfulFunctor in Init.Control.Lawful.Basic

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

class LawfulMonadRelation (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n]
    [MonadRelation m n] where
  monadRel_pure {α : Type u} (a : α) : monadRel (pure a : m α) (pure a : n α)
  monadRel_bind {α β : Type u} {ma : m α} {mb : α → m β} {na : n α} {nb : α → n β}
    (ha : monadRel ma na) (hb : ∀ a, monadRel (mb a) (nb a)) : monadRel (ma >>= mb) (na >>= nb)

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

Or.inr in Init.Prelude

structure ExecutionMethod (m : Type u → Type v) where
    exec {α : Type u} : m α → ProbComp α
    lift_probComp {α : Type u} : ProbComp α → m α
    exec_lift_probComp {α : Type u} (px : ProbComp α) :
      exec (lift_probComp px) = px

abbrev PreordEnrichedCategory (C : Type u) := EnrichedCategory Preord C

instance chartCategory : Category PFunctor.{uA, uB} where
  Hom P Q := Chart P Q
  id P := Chart.id P
  comp f g := Chart.comp g f 
  id_comp _ := rfl
  comp_id _ := rfl
  assoc _ _ _ := rfl

instance [Monad m] [LawfulMonad m] : LawfulMonadLift m (FreeContT f m) where
  monadLift_pure := by admit /- proof elided -/

abbrev addValue (seed : QuerySeed spec) (i : ι) (u : spec.range i) : QuerySeed spec :=
  seed.addValues [u]

Array.flatMapM in Init.Data.Array.Basic

noncomputable def ProbComp.advantage (p : ProbComp Unit) : ℝ := |1 / 2 - ([= () | p]).toReal|

instance : Extend Stream' where
  extend s f := fun n => f (Stream'.drop n s)

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

Seq in Init.Prelude

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'

instance [MonadTransformer t] [Monad m] : MonadLift m (t m) := MonadTransformer.transform m

Function.update in Mathlib.Logic.Function.Basic

instance : Coseq NonEmptyList where
  coseq := NonEmptyList.zip

instance instLawfulFunctor [Comonad w] [LawfulFunctor w] : LawfulFunctor (EnvT e w) where
  id_map := by admit /- proof elided -/

instance {w d} [Monad w] [DijkstraMonad w d] : MonadRelation (fun α => (w : w α) × d w) w :=
  instOfMonadLiftT

inductive FreeDijkstra (m : Type u → Type v) [Monad m] : {α : Type u} → m α → Type _ where
  | protected pure {α} (x : α) : FreeDijkstra m (pure x)
  | roll {α β} (x : m α) {f : α → m β} (r : α → FreeDijkstra m (x >>= f)) : FreeDijkstra m (x >>= f)

@[inline, reducible]
def rename (spec : OracleSpec ι) (f : τ → ι) : OracleSpec τ := spec ∘ f

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

def tensorSigmaDistrib :
    P ⊗ sigma F ≃ₚ sigma (fun i => P ⊗ F i) where
  equivA := sorry
  equivB := sorry

class OrderedMonadTransformer (t : (Type u → Type v) → Type u → Type w)
    extends MonadTransformer t where
  mapOrderedMonad {m} [OrderedMonad m] : OrderedMonad (t m)
  liftOf_mono {m n} [OrderedMonad m] [OrderedMonad n] [OrderedMonadLiftT m n] :
    OrderedMonadLiftT (t m) (t n)

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

OptionT in Init.Control.Option

instance : Coapplicative NonEmptyList where

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

Summable in Mathlib.Topology.Algebra.InfiniteSum.Defs

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

Equiv.pemptyProd in Mathlib.Logic.Equiv.Prod

instance support_finite [spec.FiniteRange] (oa : OracleComp spec α) :
    Finite ↥(oa.support) := supportWhen_finite _ oa

require "leanprover-community" / "mathlib" @ git "v4.24.0-rc1"

instance : Coe (MonadEquiv m n) (MonadHom n m) where
  coe f := ⟨f.invNatHom, f.map_pure_inv, f.map_bind_inv⟩

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

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

def pointwiseRelation {α β : Type u} (r : β → β → Prop) (f g : α → β) : α → α → Prop :=
  fun a b => r (f a) (g b)

MonadStateOf.get in Init.Prelude

Sum.inl in Init.Core

Group in Mathlib.Algebra.Group.Defs

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

Function.support in Mathlib.Algebra.Notation.Support

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

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

List in Init.Prelude

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

def ofList [DecidableEq ι] {i : ι} (xs : List (spec.range i)) : QuerySeed spec :=
  fun j => if h : i = j then h ▸ xs else []

def FreeContT (f : Type z → Type y) (m : Type u → Type v) (α : Type w) :
    Type (max (u + 1) v w y (z + 1)) :=
  {r : Type u} → ({x : Type z} → f x → ContT r m x) → ContT r m α

Bind.bind in Init.Prelude

def MonoContProp : Type u → Type u := @MonoCont Prop instPreorderProp

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

Computation in Mathlib.Data.Seq.Computation

def generateSingleSeed (spec : OracleSpec ι) (i : ι) [SelectableType (spec.range i)]
    (n : ℕ) : ProbComp (QuerySeed spec) :=
  QuerySeed.ofList <$> ($ᵗ spec.range i).replicate n

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)

AddCommMonoid in Mathlib.Algebra.Group.Defs

Classical.decEq in Mathlib.Logic.Basic

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)

StateM in Init.Control.State

CategoryTheory.Bundled in Mathlib.CategoryTheory.ConcreteCategory.Bundled

instance [RelativeBind Id m] : Bind m where
  bind := @bindᵣ Id m _

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

List.foldr in Init.Data.List.Basic

Vector.zipWith in Init.Data.Vector.Basic
</all_available_defs>

<all_available_lemmas>
@[simp]
lemma mapM_query [LawfulMonad m] (q : OracleQuery spec α) :
    (q : OracleComp spec α).mapM fail qm = qm q

@[simp]
lemma monad_bind_def (x : FreeM P α) (g : α → FreeM P β) :
    x >>= g = FreeM.bind x g

@[simp] lemma supportWhen_monadLift (q : OracleQuery spec α)
    (poss : {α : Type w} → OracleQuery superSpec α → Set α) :
    supportWhen (q : OracleComp superSpec α) poss = poss q

@[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 apply_eq (q : OracleQuery spec α) :
    unifOracle.impl q = match q with

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 generateSeed_cons : generateSeed spec qc (j :: js) =
    ($ᵗ (spec.range j)).replicate (qc j) >>= λ xs ↦
      generateSeed spec qc js

lemma probFailure_bind_of_const [Nonempty α] (r : ℝ≥0∞) (h : ∀ x, [⊥ | ob x] = r) :
    [⊥ | oa >>= ob] = [⊥ | oa] + r - [⊥ | oa] * r

@[simp]
theorem sumPair_comp_inl (f : Lens P R) (g : Lens Q R) :
    Lens.sumPair f g ∘ₗ Lens.inl = f

lemma mem_support_vector_mapM {n} {f : α → OracleComp spec β} {as : Vector α n} {x : Vector β n} :
    x ∈ (Vector.mapM f as).support ↔ ∀ i : Fin n, x[i] ∈ (f as[i]).support

@[simp]
lemma neverFails_query_bind_iff {q : OracleQuery spec α} {oa : α → OracleComp spec β} :
    (liftM q >>= oa).neverFails ↔ ∀ x, neverFails (oa x)

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

@[simp]
lemma probEvent_ite (q : α → Prop) : [q | if p then oa else oa'] =
    if p then [q | oa] else [q | oa']

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

lemma simulation_setup_succeeds (message_content : String) :
    [⊥ | do
      let maybeData ← simulation_setup message_content
      match maybeData with
      | none => return true
      | some _ => return false] = 0

@[simp]
lemma probEvent_pure (p : α → Prop) [DecidablePred p] :
    [p | (pure x : OracleComp spec α)] = if p x then 1 else 0

@[simp] lemma probEvent_uniformOfFintype [Fintype α] (p : α → Prop) [DecidablePred p] :
    [p | $ᵗ α] = (Finset.univ.filter p).card / Fintype.card α

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

@[simp] lemma isFailure_failure : isFailure (failure : OracleComp spec α) = true

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

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

lemma liftComp_def (oa : OracleComp spec α) :
    liftComp oa superSpec = simulateQ (m := OracleComp superSpec) ⟨liftM⟩ oa

@[simp] lemma isFailure_query_bind : isFailure ((q : OracleComp spec β) >>= oa) = false

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

theorem comp_assoc {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    {S : PFunctor.{uA₄, uB₄}} (c : Chart R S) (c' : Chart Q R) (c'' : Chart P Q) :
    (c ∘c c') ∘c c'' = c ∘c (c' ∘c c'')

theorem monadLift_guard [AlternativeMonad m] [AlternativeMonad n] [MonadLift m n]
    [LawfulAlternativeLift m n] [LawfulMonadLift m n] (p : Prop) [Decidable p] :
    monadLift (guard p : m Unit) = (guard p : n Unit)

@[simp]
lemma probOutput_prod_mk_fst_map [spec.FiniteRange] (oa : OracleComp spec α) (y : β) (z : α × β) :
    [= z | (·, y) <$> oa] = [= z.1 | oa] * [= z.2 | (pure y : OracleComp spec β)]

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]

theorem conj_rule {P₁ P₂ : PreCondition σ} {Q₁ Q₂ : PostCondition σ α}
    {comp : StateM σ α}
    (h₁ : HoareTriple P₁ comp Q₁) (h₂ : HoareTriple P₂ comp Q₂) :
    HoareTriple (fun s => P₁ s ∧ P₂ s) comp (fun s x s' => Q₁ s x s' ∧ Q₂ s x s')

lemma probEvent_coin_eq_add (p : Bool → Prop) [DecidablePred p] :
    [p | coin] = (if p true then 2⁻¹ else 0) + (if p false then 2⁻¹ else 0)

lemma mapM_map [LawfulMonad m] (oa : OracleComp spec α) (f : α → β)
    (hfail : ∀ f : α → β, f <$> fail = fail) :
    (f <$> oa).mapM fail qm = f <$> oa.mapM fail qm

@[simp]
lemma Fin_bound_neg {n b : ℕ} {x : Fin n} (h : Fin_Bound x b) :
  Fin_Bound (-x) b

@[simp]
lemma countQ_logQuery {α} (log : QueryLog spec) (q : OracleQuery spec α) (u : α)
    (i : ι) : (log.logQuery q u).countQ i = log.countQ i + if q.index = i then 1 else 0

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

@[simp] lemma finSupport_pure [spec.FiniteRange] [DecidableEq α] (x : α) :
    (pure x : OracleComp spec α).finSupport = {x}

lemma abs_mul_of_nonpos (h : b < 0) : |a

@[simp]
lemma evalDist_liftComp [spec.FiniteRange] [superSpec.FiniteRange]
    (oa : OracleComp spec α) : evalDist (liftComp oa superSpec) = evalDist oa

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

lemma probEvent_congr' {p q : α → Prop} {oa : OracleComp spec α} {oa' : OracleComp spec' α}
    (h1 : ∀ x, x ∈ oa.support → x ∈ oa'.support → (p x ↔ q x))
    (h2 : evalDist oa = evalDist oa') : [p | oa] = [q | oa']

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

@[simp]
lemma replicateTR_zero : replicate 0 oa = return []

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

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 probOutput_pure_eq_one {x y : α} (h : y = x) :
    [= y | (pure x : OracleComp spec α)] = 1

@[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 α))⁻¹

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

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

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

lemma probOutput_generateSeed [spec.FiniteRange] (seed : QuerySeed spec)
    (h : seed ∈ (generateSeed spec qc js).support) : [= seed | generateSeed spec qc js] =
    1 / (js.map (λ j ↦ (Fintype.card (spec.range j)) ^ qc j)).prod

@[simp] lemma Finset.sum_boole' {ι β : Type*} [AddCommMonoid β] (r : β)
    (p) [DecidablePred p] (s : Finset ι) :
    (∑ x ∈ s, if p x then r else 0 : β) = (s.filter p).card • r

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

@[simp]
lemma probOutput_liftM [Fintype α] (q : OracleQuery spec α) (u : α) :
    [= u | (q : OracleComp spec α)] = (Fintype.card α : ℝ≥0∞)⁻¹

lemma probEvent_coin_eq_sum_subtype (p : Bool → Prop) :
    [p | coin] = ∑' _ : {x | p x}, 2⁻¹

lemma probOutput_IND_CPA_experiment_eq_add {encAlg : AsymmEncAlg ProbComp M PK SK C}
    (adversary : encAlg.IND_CPA_adversary) :
    [= () | IND_CPA_experiment adversary] =
      [= () | do
        let (pk, _sk) ← encAlg.keygen
        let b ← (simulateQ (encAlg.IND_CPA_queryImpl' pk true) (adversary pk)).run' ∅
        guard b] / 2 +
      [= () | do
        let (pk, _sk) ← encAlg.keygen
        let b ← (simulateQ (encAlg.IND_CPA_queryImpl' pk false) (adversary pk)).run' ∅
        guard ¬b] / 2

@[simp]
lemma mapM_ite (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) :
    (ite p oa oa').mapM fail qm = ite p (oa.mapM fail qm) (oa'.mapM fail qm)

@[simp] lemma neverFails_list_vector_mmap {f : α → OracleComp spec β} {as : List.Vector α n}
    (h : ∀ x ∈ as.toList, neverFails (f x)) : neverFails (List.Vector.mmap f as)

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

lemma mem_finSupport_of_mem_support {x : α} (hx : x ∈ oa.support) : x ∈ oa.finSupport

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

lemma probEvent_seq_map_prod_mk_eq_mul' :
    [λ z ↦ p z.1 ∧ q z.2 | (λ x y ↦ (y, x) : β → α → α × β) <$> ob <*> oa] = [p | oa] * [q | ob]

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

@[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 simulateQ_seqLeft (oa : OracleComp spec α) (ob : OracleComp spec β) :
    simulateQ so (oa <* ob) = simulateQ so oa <* simulateQ so ob

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

@[simp] lemma evalDist_eq : evalDist p = p

@[simp]
lemma evalDist_orElse [h : spec.FiniteRange] (oa oa' : OracleComp spec α) :
    evalDist (oa <|> oa') = (evalDist oa <|> evalDist oa')

@[ext]
protected lemma ext (seed₁ seed₂ : QuerySeed spec) (h : ∀ i, seed₁ i = seed₂ i) : seed₁ = seed₂

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

@[simp]
lemma liftM_right_append_right_append_eq [h : spec₂ ⊂ₒ spec₃]
    (q : OracleQuery (spec₁ ++ₒ spec₂) α) : (liftM q : OracleQuery (spec₁ ++ₒ spec₃) α) =
    match q with

@[simp]
lemma run_simulateQ_bind_fst (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    ((simulateQ countingOracle oa).run >>= fun x => ob x.1) = oa >>= ob

lemma probOutput_prod_mk_apply_seq_map_eq_mul [spec.FiniteRange] (oa : OracleComp spec α)
    (ob : OracleComp spec β)
    (f : α → γ) (g : β → δ) (z : γ × δ) :
    [= z | (f ·, g ·) <$> oa <*> ob] = [= z.1 | f <$> oa] * [= z.2 | g <$> ob]

theorem Hybrid_2_advantage_zero : (Hybrid_2 adv).advantage' = 0

@[simp] lemma supportWhen_failure : (failure : OracleComp spec α).supportWhen poss = ∅

lemma query_bind_eq_roll (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    (q : OracleComp spec α) >>= ob = OptionT.mk (FreeMonad.roll q ob)

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

@[simp] lemma C_B (A : Type u) (a : (C A).A) : (C A).B a = PEmpty

@[simp]
lemma liftComp_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    liftComp (oa >>= ob) superSpec =
      liftComp oa superSpec >>= λ x ↦ liftComp (ob x) superSpec

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

lemma isQueryBound_mono {oa : OracleComp spec α} (qb : ι → ℕ) {qb' : ι → ℕ}
    (h' : IsQueryBound oa qb) (h : qb ≤ qb') : IsQueryBound oa qb'

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

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

lemma probFailure_bind_le_of_forall {oa : OracleComp spec α} {s : ℝ≥0∞}
    -- TODO: this should be a general type of `uniformOutput` computations
    (h' : [⊥ | oa] = s) (ob : α → OracleComp spec β) {r : ℝ≥0∞}
    (hr : ∀ x ∈ oa.support, [⊥ | ob x] ≤ r) : [⊥ | oa >>= ob] ≤ s + (1 - s) * r

@[simp]
lemma Vector.getElem_eq_get {α n} (xs : List.Vector α n) (i : ℕ) (h : i < n) :
  xs[i]'h = xs.get ⟨i, h⟩

@[simp] lemma X_B (a : X.A) : X.B a = PUnit

@[simp]
lemma monadLift_eq_lift (x : f α) :
  (x : FreeMonad f α) = FreeMonad.lift x

@[simp] lemma support_failure : (failure : OracleComp spec α).support = ∅

lemma run_none_eq_one_sub (p : SPMF α) :
    p.run none = 1 - ∑' x, p.run (some x)

lemma sum_probOutput_eq_one [Fintype α] (oa : OracleComp spec α) (h : [⊥ | oa] = 0) :
    ∑ x : α, [= x | oa] = 1

@[simp] lemma simulateQ_pure (x : α) : simulateQ so (pure x) = pure x

@[simp low]
lemma probEvent_eq_one_iff : [p | oa] = 1 ↔ [⊥ | oa] = 0 ∧ ∀ x ∈ oa.support, p x

@[simp]
lemma neverFails_run_simulateQ_iff (oa : OracleComp spec α) :
    neverFails (simulateQ countingOracle oa).run ↔ neverFails oa

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

@[simp] -- This doesn't hold without lawful monad
lemma mmap_map [LawfulMonad m] [LawfulMonad n]
    (F : m →ᵐ n) (x : m α) (g : α → β) : F (g <$> x) = g <$> F x

@[simp] theorem extract_duplicate_eq_id : extract (duplicate wa) = wa

@[simp] lemma evalDist_comp_map [LawfulMonad m] (mx : m α) :
    evalDist ∘ (fun f => f <$> mx) = fun f : (α → β) => f <$> evalDist mx

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

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

lemma finSupport_def [∀ i, Fintype (spec.range i)] [DecidableEq α] (oa : OracleComp spec α) :
    oa.finSupport = oa.finSupportWhen fun

@[simp] lemma mapM_failure : (failure : OracleComp spec α).mapM fail qm = fail

@[simp] lemma one_le_probFailure_iff : 1 ≤ [⊥ | oa] ↔ [⊥ | oa] = 1

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

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

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

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

@[simp]
lemma run_failure [Monoid ω] {α : Type u} : (failure : WriterT ω m α).run = failure

@[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 evalDist_ite (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) :
    evalDist (if p then oa else oa') = if p then evalDist oa else evalDist oa'

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

lemma cons_mem_finSupport_seq_map_cons_iff [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α]
    (x : α) (xs : List α) : x :: xs ∈ (cons <$> oa <*> ob).finSupport ↔
      x ∈ oa.finSupport ∧ xs ∈ ob.finSupport

lemma apply_eq {α} (q : OracleQuery spec α) : cachingOracle.impl q =
  match q with

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

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

theorem weaken_rule {P : PreCondition σ} {Q : PostCondition σ α}
    {comp : StateM σ α} (h : HoareTriple P comp Q) (P' : PreCondition σ)
    (h_imp : ∀ s, P' s → P s) :
      HoareTriple P' comp Q

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

@[simp]
lemma probFailure_map : [⊥ | f <$> oa] = [⊥ | oa]

@[simp]
lemma probOutput_prod_mk_snd_map [spec.FiniteRange] (ob : OracleComp spec β) (x : α) (z : α × β) :
    [= z | (x, ·) <$> ob] = [= z.1 | (pure x : OracleComp spec α)] * [= z.2 | ob]

@[simp] theorem comonad_comp_map {α β γ : Type u} (f : β → γ) (g : α → β) (wa : w α) :
    Functor.map (f ∘ g) wa = Functor.map f (Functor.map g wa)

@[simp]
lemma mock_decrypt_mock_encrypt (msg : BitVec 256) :
    mock_decrypt (mock_encrypt msg) = msg

@[simp]
lemma probOutput_prod_mk_fst_map' [spec.FiniteRange] (oa : OracleComp spec α)
    (f : α → γ) (y : β) (z : γ × β) :
    [= z | (f ·, y) <$> oa] = [= z.1 | f <$> oa] * [= z.2 | (pure y : OracleComp spec β)]

lemma List.card_filter_getElem_eq {α : Type*} [DecidableEq α]
    (xs : List α) (x : α) :
    (Finset.filter (λ i : Fin (xs.length) ↦ xs[i] = x) Finset.univ).card =
      xs.count x

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

@[simp]
lemma liftComp_query (q : OracleQuery spec α) :
    liftComp (q : OracleComp spec _) superSpec = liftM q

@[simp] lemma run_lift {m : Type u → Type v} [Monad m]
    {α : Type u} (x : m α) : (OptionT.lift x).run = x

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 evalDist_coin : evalDist coin = OptionT.lift (PMF.uniformOfFintype Bool)

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

@[simp]
lemma liftM_of_liftM_eq [MonadLift m m'] (x : StateT σ m α) :
    (liftM x : StateT σ m' α) = StateT.mk fun s => liftM (x.run s)

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

lemma uniformSelectFinset_def {α : Type} [DecidableEq α] (s : Finset α) :
    ($ s) = ($ s.toList)

@[simp]
lemma mapM_query_bind (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    ((q : OracleComp spec α) >>= ob).mapM fail qm =
      (do let x ← qm q; (ob x).mapM fail qm)

@[simp]
lemma probOutput_failure (x : α) : [= x | (failure : OracleComp spec α)] = 0

lemma probOutput_bind_congr_le_sub {γ₁ γ₂ : 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 ulift_A : (P.ulift).A = ULift P.A

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

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

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

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

@[simp] lemma pure_ne_failure : (pure x : OracleComp spec α) ≠ failure

@[simp]
lemma run_bind [LawfulMonad m] (x : WriterT ω m α) (f : α → WriterT ω m β) :
    (x >>= f).run = x.run >>= fun (a, w₁) => Prod.map id (w₁ * ·) <$> (f a).run

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

@[simp] theorem RelativeFunctor.map_map [RelativeFunctor j f] [LawfulRelativeFunctor j f]
    (h : j α → j β) (g : j β → j γ) (x : f α) :
      g <$>ᵣ h <$>ᵣ x = (fun a => g (h a)) <$>ᵣ x

@[simp] lemma mapM_pure (x : α) : (pure x : OracleComp spec α).mapM fail qm = pure x

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

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

theorem IsCoupling.exists_bind {α₁ α₂ β₁ β₂ : Type u}
    {p : SPMF α₁} {q : SPMF α₂} {f : α₁ → SPMF β₁} {g : α₂ → SPMF β₂}
    (c : Coupling p q)
    (h : ∀ (a₁ : α₁) (a₂ : α₂), ∃ (d : SPMF (β₁ × β₂)), IsCoupling d (f a₁) (g a₂)) :
    ∃ (d : SPMF (β₁ × β₂)), IsCoupling d (p >>= f) (q >>= g) :=
  let d : (a₁ : α₁) → (a₂ : α₂) → SPMF (β₁ × β₂)

lemma countQ_singleton_self (i : ι) (t : spec.domain i) (u : spec.range i) :
    countQ (singleton (query i t) u) i = 1

lemma probOutput_map_eq_probEvent [spec.FiniteRange]
    (oa : OracleComp spec α) (f : α → β) (y : β) :
    [= y | f <$> oa] = [fun x => f x = y | oa]

@[simp] lemma probOutput_lt_top : Pr[= x | mx] < ∞

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

@[simp] lemma support_ite (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) :
    (if p then oa else oa').support = if p then oa.support else oa'.support

@[simp]
lemma probFailure_failure : [⊥ | (failure : OracleComp spec α)] = 1

@[simp]
lemma probEvent_seq_map_prod_mk_eq_mul :
    [λ z ↦ p z.1 ∧ q z.2 | Prod.mk <$> oa <*> ob] = [p | oa] * [q | ob]

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

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

lemma probEvent_eq_sum_filter_finSupport [spec.DecidableEq] [DecidablePred p] [DecidableEq α] :
    [p | oa] = ∑ x ∈ oa.finSupport.filter p, [= x | oa]

lemma probFailure_eq_sub_tsum (oa : OracleComp spec α) :
    [⊥ | oa] = 1 - ∑' x : α, [= x | oa]

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

<local_ctx>
import ToMathlib.PFunctor.Basic

section find_home

variable {α : Sort u} {β : α → Sort v} {γ : α → Sort v}

end find_home

namespace PFunctor

namespace Lens

@[inherit_doc] infixl:75 " ∘ₗ " => comp

@[inherit_doc] infix:50 " ≃ₗ " => Equiv

namespace Equiv

end Equiv

def prodPair {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    (l₁ : Lens P Q) (l₂ : Lens P R) :
    Lens.{uA₁, uB₁, max uA₂ uA₃, max uB₂ uB₃} P (Q * R) :=
  (fun p => (l₁.toFunA p, l₂.toFunA p)) ⇆
    (fun p => Sum.elim (l₁.toFunB p) (l₂.toFunB p))

@[inherit_doc] infixl:75 " ◃ₗ " => compMap

@[inherit_doc] infixl:75 " ×ₗ " => prodMap

@[inherit_doc] infixl:75 " ⊎ₗ " => sumMap

@[inherit_doc] infixl:75 " ⊗ₗ " => tensorMap

notation "[" l₁ "," l₂ "]ₗ" => sumPair l₁ l₂

notation "⟨" l₁ "," l₂ "⟩ₗ" => prodPair l₁ l₂

section Coprod

variable {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₁}}
  {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₃}} {X : PFunctor.{uA₅, uB₅}}
</local_ctx>

<target_theorem>
@[simp]
theorem sumPair_inl_inr :
    Lens.sumPair Lens.inl Lens.inr = Lens.id.{max uA₁ uA₂, uB₁} (P + Q) :=
</target_theorem>

