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>
Vector in Init.Data.Vector.Basic

List.flatten in Init.Prelude

instance : Coe (NonNeg α) α := ⟨(·.1)⟩

List.foldl in Init.Prelude

instance (priority := high) maybeInduced {α : Type} [Preorder α] : Preorder (Option α) :=
  let le : Option α → Option α → Prop := λ x y ↦
                                           match x, y with
                                           | .none, .none | .none, .some _ => True
                                           | .some x, .some y => x ≤ y
                                           | .some _, .none   => False
  {
    le := le
    lt := λ a b ↦ le a b ∧ ¬ le b a 
    le_refl := by admit /- proof elided -/

abbrev Τ (K₁ K₂ V : Type) [PreWithZero V] := { τ : Τ' K₁ K₂ V // τ.isValid }

Int.reduceAdd in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int

IsLUB in Mathlib.Order.Bounds.Defs

instance : LinearOrder (Key K₁ K₂) where
  le := Key.le
  le_refl := λ a ↦ by dsimp [Key.le]; aesop
  le_trans := IsTrans.trans
  le_antisymm := IsAntisymm.antisymm
  le_total := IsTotal.total
  decidableLE := inferInstance
  lt_iff_le_not_le := λ a b ↦ lt_iff_le_not_le

List.lookup in Init.Data.List.Basic

Iff in Init.Core

def f (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) : S K₁ K₂ V :=
  ⟨
    λ k ↦
      have : InfSet V := infV b T k
      ⨅ x : boundedBelow b T, fc x.1 k,
    by admit /- proof elided -/
  ⟩

List.finRange in Init.Data.List.FinRange

inductive Block (K₁ K₂ : Type) (C Sigma : Type) (V : Type) [PreWithZero V] where
   
  | deposit (recipient : K₂) (amount : V₊)
   
  | transfer (aggregator : K₁) (extradata : ExtraDataT) (commitment : C) (senders : List K₂) (sigma : Sigma)
   
  | withdrawal (withdrawals : K₁ → V₊)

instance : Coe K₁ (Key K₁ K₂) := ⟨.inl⟩

def First (x₁ x₂ : Option α) : Option α :=
  match x₁, x₂ with
  | .some x, .none => .some x
  | .some x, .some _ => .some x
  | .none, .some y => .some y
  | .none, .none => .none

Option.isNone in Init.Data.Option.Basic

def Key.lt (k₁ k₂ : Key K₁ K₂) : Prop :=
  match k₁, k₂ with
  | .inl k₁, .inl k₁' => k₁ < k₁'
  | .inl _,  .inr _   => True
  | .inr _,  .inl _   => False
  | .inr k₂, .inr k₂' => k₂ < k₂'

def fc (τcXb : Τc K₁ K₂ V × S K₁ K₂ V) : S K₁ K₂ V :=
  ⟨λ k : Kbar K₁ K₂ ↦
    match τcXb with
    | ⟨⟨⟨⟨s, r, v⟩, _⟩, hτ⟩, b⟩ =>
      let v' := v' (v.get hτ) b s
      b k + (e r - e s) k • v',
  by admit /- proof elided -/
  ⟩

noncomputable def attach (α : Type) [Finite α] : UniquelyIndexed α :=
  have := Finite.exists_equiv_fin α
  this.choose_spec.some.toEmbedding

instance : PreWithZero α₊ :=

def appendBlock! (σ : Scontract K₁ K₂ V C Sigma)
                 (request : Request K₁ K₂ C Sigma Pi V) : Scontract K₁ K₂ V C Sigma :=
  σ ++ [request.toBlock! σ]

def mkWithdrawalBlock (K₂ C Sigma : Type) (withdrawals : K₁ → V₊) : Block K₁ K₂ C Sigma V :=
  withdrawal withdrawals

Membership in Init.Prelude

IsTotal in Mathlib.Order.Defs.Unbundled

def le (v₁ v₂ : Vector α n) :=
  ∀ x ∈ (v₁.1.zip v₂.1), x.1 ≤ x.2

def attackGameBlocks'!r (requests : List (Request K₁ K₂ C Sigma Pi V))
                        (σ : Scontract K₁ K₂ V C Sigma) : Scontract K₁ K₂ V C Sigma :=
  match requests with
  | [] => σ
  | hd :: tl => attackGameBlocks'!r tl (σ.appendBlock! hd)

def TransactionsInBlock_transfer 
  (π : BalanceProof K₁ K₂ C Pi V) (b : { b : Block K₁ K₂ C Sigma V // b.isTransferBlock }) : List (Τ K₁ K₂ V) :=
  match h : b.1 with
  | .transfer _ _ commitment S _ =>
     
    let senderRecipient : Finset (K₂ × Key K₁ K₂) := { (k₂, k) | (k₂ : K₂) (k : Key K₁ K₂) (_h : k₂ ≠ₖ k) }
    let sorted : List (K₂ × Key K₁ K₂) := senderRecipient.sort Key.lexLe 
     
    let v (s : K₂) (r : Key K₁ K₂) : Option V₊ :=
      if s ∉ S
      then .some 0
      else 
        if h : (commitment, s) ∈ π.keys
        then let (_, t) := π[(commitment, s)]
             t r
        else .none
    sorted.attach.map λ ⟨(s, r), h⟩ ↦ ⟨(s, r, v s r), by admit /- proof elided -/
    ⟩
  | .deposit .. | .withdrawal .. => by admit /- proof elided -/

instance [Finite K₁] [Finite K₂] : Finite (Kbar K₁ K₂ : Type) :=
  Finite.of_equiv _ univKbar.symm

def TransactionsInBlock_withdrawal 
  (b : { b : Block K₁ K₂ C Sigma V // b.isWithdrawalBlock }) : List (Τ K₁ K₂ V) :=
  match h : b.1 with
  | .withdrawal withdrawals =>
     
    let k₁InOrder := { s | s : K₁ }.toFinset.sort (·≤·)
    k₁InOrder.attach.map λ s : K₁ ↦ ⟨(s, .Source, withdrawals s), by admit /- proof elided -/
    ⟩
  | .deposit r v | .transfer .. => by admit /- proof elided -/

private def TransactionsInBlocksFixed (π : BalanceProof K₁ K₂ C Pi V) (bs : List (Block K₁ K₂ C Sigma V)) :
  Vector (Τ K₁ K₂ V) (length_of_TransactionsInBlocks (Pi := Pi) bs).1 :=
  ⟨TransactionsInBlocks π bs, by admit /- proof elided -/
  ⟩

def exists_inf (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) : { s : S K₁ K₂ V // ∀ k, IsGLB (V' b T k) (s k) } :=
  ⟨
    f' b T,
    λ k ↦
      have f'_codomain : (f' b T) k ∈ V' b T k := by admit /- proof elided -/
  ⟩

lowerBounds in Mathlib.Order.Bounds.Defs

instance : Nonempty ExtraDataT := inferInstanceAs (Nonempty ℕ)

abbrev BalanceProof (K₁ K₂ : Type) [Finite K₁] [Finite K₂]
                    (C Pi V : Type) [PreWithZero V] : Type :=
  Dict (C × K₂) ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V)

IsBot in Mathlib.Order.Max

List.take in Init.Data.List.Basic

instance : IsTrans (K₂ × Key K₁ K₂) lexLe :=

def attackGameBlocks! (requests : List (Request K₁ K₂ C Sigma Pi V)) : Scontract K₁ K₂ V C Sigma :=
  attackGameBlocks'! requests []

instance : Preorder (Kbar K₁ K₂) := discretePreorder

List in Init.Prelude

Multiset.Nodup in Mathlib.Data.Multiset.Defs

Set.image in Mathlib.Data.Set.Defs

def codomainPred {α : Type} [DecidableEq α] {β : Type}
  (m : Finmap (λ _ : α ↦ β)) (P : β → Prop) : Prop :=
  ∀ key : α, (h : key ∈ m) → P (m.lookup_h h)

def Seed : Type := ℕ

Nat.card in Mathlib.SetTheory.Cardinal.Finite

instance latticePreorder : Preorder V := inferInstance

instance : Preorder (Option V₊) := inferInstance

Function.LeftInverse in Init.Data.Function

instance : Coe K₂ (Key K₁ K₂) := ⟨.inr⟩

abbrev KₛT : Type := ℕ

def iso {X : Type} [Preorder X] (a b : X) := a ≤ b ∧ b ≤ a

instance : LE (Key K₁ K₂) := ⟨Key.le⟩

def normalise (requests : List (Request K₁ K₂ C Sigma Pi V)) : List (Request K₁ K₂ C Sigma Pi V) :=
  requests.filter Request.isValid

List.zip in Init.Data.List.Basic

def value (τ : Τ K₁ K₂ V) : Option V₊ := τ.1.2.2

Nat in Init.Prelude

def mergeR''' (πs : List (BalanceProof K₁ K₂ C Pi V)) (acc : BalanceProof K₁ K₂ C Pi V) : BalanceProof K₁ K₂ C Pi V :=
  πs.foldl Dict.Merge acc

class ADScheme (K : Type)
               (M : Type)
               (C Pi : Type) where
  Commit : Dict K M → CommitT C K Pi
  Verify : Pi → K → M → C → Bool

def initial : Scontract K₁ K₂ V C Sigma := []

private instance [(a b : K₁) → Decidable (a ≤ b)] [(a b : K₂) → Decidable (a ≤ b)] :
         (a b : Key K₁ K₂) → Decidable (a ≤ b) :=
  λ a b ↦ by
    dsimp [(·≤·), Key.le]
    rcases a with a | a <;> rcases b with b | b <;> infer_instance

Int.reduceNeg in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int

private instance [IsAntisymm K₁ (·≤·)] [IsAntisymm K₂ (·≤·)] : IsAntisymm (Key K₁ K₂) (·≤·) :=
  {
    antisymm := λ a b ↦ by
      dsimp [(·≤·), Key.le]; intros h₁ h₂
      aesop (add safe forward IsAntisymm.antisymm)
  }

def TransactionsInBlock_deposit
  (b : { b : Block K₁ K₂ C Sigma V // b.isDepositBlock }) : List (Τ K₁ K₂ V) :=
  match h : b.1 with
  | .deposit r v => [⟨(.Source, r, v), by admit /- proof elided -/
  ⟩]
  | .withdrawal .. | .transfer .. => by admit /- proof elided -/

DecidableEq in Init.Prelude

Monotone in Mathlib.Order.Monotone.Defs

List.Ico in Mathlib.Data.List.Intervals

Sum in Init.Core

noncomputable instance : Fintype K₁ := Fintype.ofFinite _

abbrev isTransferBlock (b : Block K₁ K₂ C Sigma V) := b matches (Block.transfer _ _ _ _ _)

def e (i : Kbar K₁ K₂) : Kbar K₁ K₂ → ℤ := λ j ↦ if i = j then 1 else 0

Subtype.val in Init.Prelude

@[simp]
private def reindex : (a : ℕ) → a ∈ Finset.range (k + 1) \ {0} → ℕ :=
  λ a _ ↦ a.pred

instance (priority := high) vectorPreorder : Preorder (Vector α n) where
  le_refl := λ _ ↦ Vec.le_refl
  le_trans := λ _ _ _ ↦ Vec.le_trans

def Merge (D₁ D₂ : Dict α ω) : Dict α ω := D
  where D := λ x ↦ First (D₁ x) (D₂ x)

abbrev S' (K₁ K₂ V : Type) := Kbar K₁ K₂ → V

List.NodupKeys in Mathlib.Data.List.Sigma

noncomputable instance {α : Type} [Finite α] : Inhabited (UniquelyIndexed α) := ⟨attach α⟩

DecidableRel in Init.Prelude

abbrev Key (K₁ K₂ : Type) := K₁ ⊕ K₂

abbrev UniquelyIndexed (α : Type) [Finite α] : Type := α ↪ !α

Sigma.mk in Init.Core

def mergeR' (πs : List (BalanceProof K₁ K₂ C Pi V)) : Fin πs.length.succ → BalanceProof K₁ K₂ C Pi V :=
  λ i ↦ match h : i.1 with
        | 0 => .initial
        | k + 1 => Dict.Merge (mergeR' πs ⟨k, by admit /- proof elided -/
        ⟩) πs[k]
  termination_by i => i
  decreasing_by { simp_wf; next m => rcases m; aesop }

instance : DecidableRel (lexLe (K₁ := K₁) (K₂ := K₂)) :=
  λ a b ↦ by unfold lexLe; infer_instance

def Verify (π : BalanceProof K₁ K₂ C Pi V)
           [AD : ADScheme K₂ M C Pi] : Bool :=
  ∀ x, (h : x ∈ Dict.keys π) → let ((π', salt), t) := (π x).get (by admit /- proof elided -/
  )
                               AD.Verify π' x.2 (H _ (t, salt)) x.1

Classical.arbitrary in Mathlib.Logic.Nonempty

instance [Finite K₁] [Finite K₂] : Preorder (TransactionBatch K₁ K₂ V) := discretePreorder

instance [Finite K₁] [Finite K₂] : Preorder ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V) := inferInstance

def toBlock (σ : Scontract K₁ K₂ V C Sigma)
            (request : Request K₁ K₂ C Sigma Pi V) : Option (Block K₁ K₂ C Sigma V) :=
  if ¬request.isValid
  then .none
  else .some <|
  match request with
   
  | .deposit r v            => .deposit r v
   
  | .transfer a e c s sigma => .transfer a e c s sigma
   
  | .withdrawal π           => .withdrawal (π.toBalanceF σ)

List.attach in Init.Data.List.Attach

Coe in Init.Coe

inferInstanceAs in Init.Prelude

abbrev keys (ct : CommitT C K Pi) := ct.dict.keys

abbrev Scontract (K₁ K₂ V : Type) [PreWithZero V] (C Sigma : Type) :=
  List (Block K₁ K₂ C Sigma V)

abbrev boundedBelow (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) :=
  { a : Τc K₁ K₂ V × S K₁ K₂ V | (T, b) ≤ (↑a.1, a.2) }

def BalanceProof.compat (π₁ π₂ : BalanceProof K₁ K₂ C Pi V) : Prop :=
  ∀ k, π₁ k ≠ none ∧ π₂ k ≠ none → π₁ k ≅ π₂ k

def V' (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) (k : Kbar K₁ K₂) : Set V :=
  { v : V | v ∈ (fc · k) '' boundedBelow b T }

Std.Associative in Init.Core

instance : Preorder (S K₁ K₂ V) := inferInstance

instance : GetElem (Dict α ω) α ω Dict.is_mem where
  getElem := λ m x h ↦ (m x).get h

PartialOrder in Mathlib.Order.Defs.PartialOrder

def IsEquivRel {X : Type} [Preorder X] := ∀ a b : X, a ≤ b ↔ a ≅ b

def isCodomainNonneg {α : Type} [DecidableEq α] {β : Type} [LE β] [OfNat β 0]
  (m : Finmap (λ _ : α ↦ β)) : Prop := codomainPred m (0 ≤ ·)

IsLeast in Mathlib.Order.Bounds.Defs

instance : Preorder (Kbar K₁ K₂ × Kbar K₁ K₂ × Option V₊) := inferInstance

def TransactionsInBlock (π : BalanceProof K₁ K₂ C Pi V) (b : Block K₁ K₂ C Sigma V) : List (Τ K₁ K₂ V) := 
  match h : b with
  | .deposit ..    => TransactionsInBlock_deposit ↪b
  | .transfer ..   => TransactionsInBlock_transfer π ↪b
  | .withdrawal .. => TransactionsInBlock_withdrawal ↪b

Multiset in Mathlib.Data.Multiset.Defs

def NonNeg (α : Type) [PreWithZero α] := { a : α // 0 ≤ a }

noncomputable instance : Fintype (Key K₁ K₂) :=
  have := Fintype.ofFinite K₁
  have := Fintype.ofFinite K₂
  have : Finite (Key K₁ K₂) := inferInstance
  Fintype.ofFinite (Key K₁ K₂)

DecidablePred in Init.Prelude

instance : Preorder (Τ K₁ K₂ V × S K₁ K₂ V) := inferInstance

def getDeposit (b : Block K₁ K₂ C Sigma V) (_h : b.isDepositBlock) : K₂ × V₊ :=
  match b with | deposit r v => (r, v)

private abbrev length_of_TransactionsInBlocks (bs : List (Block K₁ K₂ C Sigma V)) :
  { n : ℕ // n = (TransactionsInBlocks (Classical.arbitrary _ : BalanceProof K₁ K₂ C Pi V) bs).length } :=
  ⟨(TransactionsInBlocks (Classical.arbitrary _ : BalanceProof K₁ K₂ C Pi V) bs).length, rfl⟩

def toBlock! (σ : Scontract K₁ K₂ V C Sigma)
             (request : Request K₁ K₂ C Sigma Pi V) : Block K₁ K₂ C Sigma V :=
  match request with
  | .deposit r v            => .deposit r v
  | .transfer a e c s sigma => .transfer a e c s sigma
  | .withdrawal π           => .withdrawal (π.toBalanceF σ)

upperBounds in Mathlib.Order.Bounds.Defs

def discretePreorder {α : Type} : Preorder α :=
  {
    lt := λ _ _ ↦ False
    le := (·=·)
    le_refl := Eq.refl
    le_trans := λ _ _ _ ↦ Eq.trans
    lt_iff_le_not_le := by admit /- proof elided -/

abbrev isDepositBlock (b : Block K₁ K₂ C Sigma V) := b matches (Block.deposit _ _)

Prod.mk in Init.Prelude

Inhabited in Init.Prelude

abbrev isWithdrawalBlock (b : Block K₁ K₂ C Sigma V) := b matches (Block.withdrawal _)

instance : Std.Associative
             (Dict.Merge (α := (C × K₂)) (ω := ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V))) :=
  ⟨λ _ _ _ ↦ Dict.Merge_assoc⟩

def attackGame : Scontract K₁ K₂ V C Sigma :=
  attackGameBlocks' requests []

GetElem in Init.GetElem

Finite in Mathlib.Data.Finite.Defs

instance [Finite K₁] [Finite K₂] : Preorder (BalanceProof K₁ K₂ C Pi V) :=

Prod.snd in Init.Prelude

List.map in Init.Prelude

Sum.inr in Init.Core

instance {k₂ : K₂} {k : Key K₁ K₂} [DecidableEq K₂] : Decidable (k₂ ≠ₖ k) :=

Finset.range in Mathlib.Data.Finset.Range

def getWithdrawal (b : Block K₁ K₂ C Sigma V) (_h : b.isWithdrawalBlock) : K₁ → V₊ :=
  match b with | .withdrawal B => B

Nonempty in Init.Prelude

def attackGameRGo (requests : List (Request K₁ K₂ C Sigma Pi V))
                  (σ : Scontract K₁ K₂ V C Sigma) : Scontract K₁ K₂ V C Sigma :=
  match requests with
  | [] => []
  | hd :: tl => hd.toBlock! σ :: attackGameRGo tl (σ.appendBlock! hd)

def BalanceProof.initial : BalanceProof K₁ K₂ C Pi V := λ _ ↦ .none

Function.eval in Mathlib.Logic.Function.Basic

Fintype in Mathlib.Data.Fintype.Defs

List.keys in Mathlib.Data.List.Sigma

binding : ComputationallyInfeasible <|
              ∃ (c : C) (k : K) (m₁ m₂ : M) (π₁ π₂ : Pi),
                Verify π₁ k m₁ c = true ∧
                Verify π₂ k m₂ c = true ∧
                m₁ ≠ m₂

OfNat in Init.Prelude

def attackGameBlocks' : Scontract K₁ K₂ V C Sigma :=
  requests.foldl Scontract.appendBlock σ

Prod.fst in Init.Prelude

def lexLe (a b : K₂ × Key K₁ K₂) : Prop :=
  a.1 < b.1 ∨ (a.1 = b.1 ∧ a.2 ≤ b.2)

CovariantClass in Mathlib.Algebra.Order.Monoid.Unbundled.Defs

LE.le in Init.Prelude

def Request.getWithdrawal (request : Request K₁ K₂ C Sigma Pi V) : Option (BalanceProof K₁ K₂ C Pi V) :=
  match request with
  | withdrawal π => .some π
  | transfer .. | deposit .. => .none

def isπ (requests : List (Request K₁ K₂ C Sigma Pi V)) :=
  ∀ (h₀ : ∀ request ∈ requests, request.isValid)
    (i : Fin (attackGameR requests []).length)
    (h : (attackGameR requests [])[i].isWithdrawalBlock),
    (attackGameR requests [])[i].getWithdrawal h =
    let π := getBalanceProof requests h₀ i h
    let σ := (attackGameR requests []).take i.1
    π.toBalanceF σ

Sigma in Init.Core

instance : CoeFun (S K₁ K₂ V) λ _ ↦ Kbar K₁ K₂ → V :=
  ⟨λ s k ↦ s.1 k⟩

def aggregateWithdrawals (σ : Scontract K₁ K₂ V C Sigma) : V :=
  ∑ i : Fin σ.length,
    if h : σ[i].isWithdrawalBlock
    then ∑ (k : K₁), (σ[i.1].getWithdrawal h) k
    else 0

Set in Mathlib.Data.Set.Defs

def adversaryWon (blocks : Scontract K₁ K₂ V C Sigma) : Prop :=
  ¬0 ≤ computeBalance blocks

instance : IsAntisymm (K₂ × Key K₁ K₂) lexLe :=

Preorder in Mathlib.Order.Defs.PartialOrder

Sum.inl in Init.Core

def AgreedUponAggregator {K₁ : Type} [Nonempty K₁] : K₁ := Classical.arbitrary _

Subtype in Init.Prelude

def keys (m : Dict α ω) : Set α := { x | Dict.is_mem m x }

abbrev ExtraDataT : Type := ℕ

def sender (τ : Τ K₁ K₂ V) : Kbar K₁ K₂ := τ.1.1

Decidable in Init.Prelude

instance : Preorder (Τ K₁ K₂ V) := inferInstance

def Block.isValid (block : Block K₁ K₂ C Sigma V) (π : BalanceProof K₁ K₂ C Pi V) : Bool :=
  match block with
   
  | .deposit .. => true
   
  | .transfer aggregator extradata commitment senders sigma =>
      let isValidSA := SA.Verify senders (commitment, aggregator, extradata) sigma
      let isValidAggregator := aggregator = AgreedUponAggregator
      isValidSA ∧ isValidAggregator
   
  | .withdrawal _ => π.Verify (M := (C × K₁ × ExtraDataT))

instance : GetElem (CommitT C K Pi) K Pi (λ ct k ↦ k ∈ ct.dict) := ⟨CommitT.lookup⟩

def mkTransferBlock (aggregator : K₁) (extradata : ExtraDataT)
                    (commitment : C) (senders : List K₂) (sigma : Sigma) : Block K₁ K₂ C Sigma V :=
  transfer aggregator extradata commitment senders sigma

instance [CovariantClass V V (· + ·) (· ≤ ·)] : OrderedAddCommMonoid V := ⟨by admit /- proof elided -/
⟩

abbrev Τ' (K₁ K₂ V : Type) [PreWithZero V] := Kbar K₁ K₂ × Kbar K₁ K₂ × Option V₊

instance : Inhabited (BalanceProof K₁ K₂ C Pi V) := ⟨BalanceProof.initial⟩

Finset.sort in Mathlib.Data.Finset.Sort

Int in Init.Data.Int.Basic

Lattice in Mathlib.Order.Lattice

instance : Finite (Key K₁ K₂) :=

def Key.le (k₁ k₂ : Key K₁ K₂) : Prop :=
  match k₁, k₂ with
  | .inl k₁, .inl k₁' => k₁ ≤ k₁'
  | .inl _,  .inr _   => True
  | .inr _,  .inl _   => False
  | .inr k₂, .inr k₂' => k₂ ≤ k₂'

List.length in Init.Prelude

instance : Membership α (Dict α ω) := ⟨Dict.is_mem⟩

def Dict.is_mem (m : Dict α ω) (x : α) : Prop := (m x).isSome

reduceDIte in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

Multiset.map in Mathlib.Data.Multiset.MapFold

def attackGameR : Scontract K₁ K₂ V C Sigma :=
  σ ++ attackGameRGo requests σ

instance [PreWithZero V] : Coe (Τc K₁ K₂ V) (Τ K₁ K₂ V) := ⟨(↑·)⟩

instance : Inhabited (S' K₁ K₂ V) := ⟨S'.initial K₁ K₂ V⟩

abbrev Τc (K₁ K₂ V : Type) [PreWithZero V] : Type := { τ : Τ K₁ K₂ V // τ.isComplete }

local macro:max (priority := high) "↪" b:term : term => `(⟨$b, by admit /- proof elided -/
⟩)

def mkDepositBlock (K₁ C Sigma : Type) (addr : K₂) (value : V₊) : Block K₁ K₂ C Sigma V :=
  deposit addr value

instance : Preorder (Kbar K₁ K₂ × Kbar K₁ K₂) := inferInstance

structure CommitT (C K Pi : Type) where
  commitment : C
  dict       : Dict K Pi

CoeFun in Init.Coe

Unit in Init.Prelude

def Kbar.isK₁ (k : Kbar K₁ K₂) := k matches key (.inl _)

Finmap in Mathlib.Data.Finmap

instance : Coe K₂ (Key K₁ K₂) := ⟨.inr⟩

instance (priority := high) : LE (Vector α n) := ⟨le⟩

def getBalanceProof (requests : List (Request K₁ K₂ C Sigma Pi V))
                    (h₀ : ∀ request ∈ requests, request.isValid)
                    (i : Fin (attackGameR requests []).length)
                    (h₁ : (attackGameR requests [])[i].isWithdrawalBlock) :
                    BalanceProof K₁ K₂ C Pi V :=
  let request := requests[i]'(by admit /- proof elided -/
  )
  have : request.getWithdrawal.isSome := by admit /- proof elided -/

Lean.Parser.Tactic.replace in Init.Tactics

private instance : IsTotal (Key K₁ K₂) (·≤·) :=
  {
    total := λ a b ↦ by
      dsimp [(·≤·), Key.le]
      aesop (add simp le_total)
  }

Preorder.toLE in Mathlib.Order.Defs.PartialOrder

def lookup (ct : CommitT C K Pi) {k : K} (h : k ∈ ct.dict) : Pi :=
  ct.dict[k]

inductive Kbar (K₁ K₂ : Type) where
  | key (k : Key K₁ K₂)
  | Source
deriving DecidableEq

Zero in Init.Prelude

Correctness : ∀ (l : List (Kₚ × Kₛ)) (_ : ∀ pair ∈ l, pair ←ᵣ KeyGen) (m : M),
                  let (kₚs, kₛs) := l.unzip
                  Verify kₚs m (Aggregate (kₚs.zip (kₛs.map (Sign · m)))) = true

instance : Preorder (Key K₁ K₂ → V₊) := discretePreorder

Unforgeability :
    ComputationallyInfeasible <|
      ∃ (k : List (Kₚ × Kₛ)) (m : M) (σ : Sigma),
        let kₚs := k.map Prod.fst
        Verify kₚs m σ = true ∧
        
        
        ∃ userIdx : Fin k.length,
          let (honestₚ, honestₛ) := k[userIdx]
          honestₚ ∈ kₚs ∧ ∃ key : Kₛ, key ≠ honestₛ ∧ Sign key m = σ

correct_keys_eq : ∀ {dict : Dict K M}, (Commit dict).keys = dict.keys

IsGreatest in Mathlib.Order.Bounds.Defs

def BalanceProof.toBalanceF (π : BalanceProof K₁ K₂ C Pi V)
                            (σ : Scontract K₁ K₂ V C Sigma) : K₁ → V₊ :=
  λ k : K₁ ↦ ⟨Bal π σ k, by admit /- proof elided -/
  ⟩

flip in Init.Core

And in Init.Prelude

Finset.univ in Mathlib.Data.Fintype.Defs

Function.RightInverse in Init.Data.Function

Set.Ici in Mathlib.Order.Interval.Set.Defs

instance : Coe (Key K₁ K₂) (Kbar K₁ K₂) := ⟨.key⟩

instance : Coe K₁ (Key K₁ K₂) := ⟨.inl⟩

class SignatureAggregation (M Kₚ Kₛ Sigma : Type) where
  KeyGen    : SimpleRandom.Seed → Kₚ × Kₛ
  Sign      : Kₛ → M → Sigma
  Aggregate : List (Kₚ × Sigma) → Sigma
  Verify    : List Kₚ → M → Sigma → Bool

private def BalFixed (bs : List (Block K₁ K₂ C Sigma V)) : BalanceProof K₁ K₂ C Pi V → S K₁ K₂ V :=
  λ π ↦ fStarFixed (s₀ := S.initial K₁ K₂ V) (TransactionsInBlocksFixed π bs)

def computeBalance' (blocks : Scontract K₁ K₂ V C Sigma) (acc : V) : V :=
  blocks.foldl Block.updateBalance acc

Multiset.filter in Mathlib.Data.Multiset.Filter

absurd in Init.Prelude

instance : Setoid' ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V) where
  isEquiv := by admit /- proof elided -/

Option in Init.Prelude

Prod in Init.Prelude

class Setoid' (X : Type) extends Preorder X where
  isEquiv : IsEquivRel (X := X)

Subtype.mk in Init.Prelude

Sigma.fst in Init.Core
</all_available_defs>

<all_available_lemmas>
@[simp]
lemma sum_fc_eq_sum : ∑ (k : Kbar K₁ K₂), fc (Tc, b) k = ∑ (k : Kbar K₁ K₂), b k

lemma proposition6 [Setoid' Y] {D₁ D₂ : Dict X Y} :
  (∃ join, IsLUB {D₁, D₂} join) ↔ ∀ x, D₁ x ≠ .none ∧ D₂ x ≠ .none → D₁ x ≅ D₂ x

@[simp]
lemma isLUB_some_none_of_some :
  IsLUB {.some x, none} y? ↔ IsLUB {.some x} y?

private lemma prop6_general_aux :
  (∀ π π' : BalanceProof K₁ K₂ C Pi V, π ∈ πs ∧ π' ∈ πs → π <≅> π') →
     IsLUB {π | π ∈ πs} (mergeR'' πs .initial)

lemma f_transfer_block_source' (h : b.isTransferBlock) :
  ((TransactionsInBlock π b).foldl f σ).1 .Source = σ .Source

lemma senderReceiver_transactionsInBlocks {s r v} {s' r' v'} {eq₁ eq₂} {i}
  (h₀ : i < (TransactionsInBlocks π bs).length)
  (h₁ : (TransactionsInBlocks π bs)[i] = ⟨(s, r, v), eq₁⟩)
  (h₂ : (TransactionsInBlocks π' bs)[i]'(by blast with π) = ⟨(s', r', v'), eq₂⟩) :
  s = s' ∧ r = r'

lemma iso_K_merge_left_of_ne_none (h : π K ≠ none) : π K ≅ (π <+> acc) K

@[simp]
lemma merge_eq_none :
  (π <+> acc) K = none ↔ π K = none ∧ acc K = none

@[simp]
lemma Block.updateBalance_withdrawal {B : K₁ → V₊} :
  (Block.withdrawal B).updateBalance (K₁ := K₁) (K₂ := K₂) (C := C) (Sigma := Sigma) v = v - ∑ (k : K₁), (B k).1

@[simp]
lemma v'_key_eq_meet {k : Key K₁ K₂} : v' v b (Kbar.key k) = ⟨v ⊓ b k, by simp⟩

lemma existsLUB_iff_compat :
  (∃ join, IsLUB {π₁, π₂} join) ↔ π₁ <≅> π₂

lemma f_transfer_source''
  (h : b.isTransferBlock) (h₁ : T ∈ TransactionsInBlock π b) : 
  (f σ T) .Source = σ .Source

@[simp]
lemma length_attackGameBlocks! :
  (attackGameBlocks! requests).length = requests.length

lemma proposition1 [Preorder X] {x y : X} {s : Set X}
  (h₁ : IsLUB s x) (h₂ : IsLUB s y) : x ≅ y

@[simp]
lemma discretePreorder_eq_equality_TransactionBatch [Finite K₁] [Finite K₂]
  {a b : TransactionBatch K₁ K₂ V} : a ≤ b ↔ a = b

lemma f_withdraw_source'
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isWithdrawalBlock},
         T ∈ TransactionsInBlock π block.1) :
  (f σ T).1 .Source = σ .Source + (↑(T.value.get (isSome_of_withdrawal h)) ⊓ σ T.sender)

@[simp]
lemma some_iso_some :
  (Option.some x ≅ .some y) ↔ x ≅ y

lemma sum_f_le_sum : ∑ (k : Kbar K₁ K₂), f b T k ≤ ∑ (k : Kbar K₁ K₂), b k

lemma f_IsGLB_of_V' {b : S K₁ K₂ V} {T : Τ K₁ K₂ V} {k : Kbar K₁ K₂} :
  IsGLB (V' b T k) (f b T k)

lemma keys_Merge_left {x : α} (h : x ∈ D₁) : Merge D₁ D₂ x = D₁ x

@[simp]
lemma aggregateDeposits_nil : aggregateDeposits ([] : Scontract K₁ K₂ V C Sigma) = 0

@[simp]
lemma length_attackGameRGo : (attackGameRGo requests σ).length = requests.length

@[simp]
lemma isLUB_some_some_some :
  IsLUB {some x, some y} (some join) ↔ ((join ≅ x) ∧ join ≅ y)

@[simp]
lemma e_def : e i = λ j ↦ if i = j then 1 else 0

lemma toBlock!_of_withdrawal (h : request matches .withdrawal ..) :
  request.toBlock! σ matches .withdrawal ..

omit [Finite K₁] [Finite K₂] in
private lemma fold_f_any_transaction_transfer {acc : S K₁ K₂ V} {l : List (Τ K₁ K₂ V)}
  (h : ∀ T ∈ l, (¬ T.1.1 matches .Source) ∧ (¬ T.1.2.1 matches .Source)) :
  (List.foldl f acc l) .Source = acc .Source

@[simp]
lemma mergeR''_cons :
  mergeR'' (π :: πs) acc = Dict.Merge acc (mergeR'' πs π)

lemma mergeR''_eq_foldl :
  mergeR'' πs acc = mergeR''' πs acc

lemma toBlock!_of_transfer (h : request matches .transfer ..) :
  request.toBlock! σ matches .transfer ..

lemma f_transfer_block_source (h : b.isTransferBlock) :
  ((TransactionsInBlock π b).foldl f σ) .Source = σ .Source

lemma ne_none_of_ne_iso [Setoid' Y] {D₁ D₂ : Dict X Y} {k : X}
  (h : D₁ k ≠ .none) (h₁ : D₁ ≅ D₂) : D₂ k ≠ .none

lemma proposition2 [Setoid' X] {x y : X} :
  (∃ join : X, IsLUB {x, y} join) ↔ x ≅ y

@[simp]
lemma withdrawal_ne_transfer : 
  (withdrawal ws).isTransferBlock (V := V) (Sigma := Sigma) (C := C) (K₂ := K₂) = False

@[simp]
lemma computeBalance'_cons : computeBalance' (hd :: σ) v =
                             computeBalance' σ (Block.updateBalance v hd)

lemma le_fc_of_ne {k : Kbar K₁ K₂} (h : τc.1.1.1 ≠ k) : b k ≤ fc (τc, b) k

private lemma delta_TransactionsInBlock_transfer
  {b : { b : Block K₁ K₂ C Sigma V // b.isTransferBlock }}
  (h : π ≤ π') : 
  ∀ i : ℕ, (hlen : i < (TransactionsInBlock_transfer π b).length) →
    (TransactionsInBlock_transfer π b)[i]'hlen =
    (TransactionsInBlock_transfer π' b)[i]'(by rwa [length_TransactionsInBlock_transfer _ π]) ∨
    ((TransactionsInBlock_transfer π b)[i]'hlen).1.2.2.isNone

private lemma sum_fStar_le_zero_aux (h : ∑ (k : Kbar K₁ K₂), b k ≤ 0) :
  ∑ (k : Kbar K₁ K₂), fStar Tstar b k ≤ 0

@[simp]
lemma transactionsInBlock_deposit {r : K₂} {v : V₊} :
  TransactionsInBlock (K₁ := K₁) (Sigma := Sigma) π (Block.deposit r v) =
  [⟨(.Source, r, v), by simp [Τ'.isValid]⟩]

lemma keys_Merge_right' (h : ∀ x : α, x ∉ D₁) : Merge D₁ D₂ = D₂

@[simp]
lemma v'_source_eq_v : v' v b .Source = v

@[simp]
lemma length_appendBlock :
  (appendBlock! σ request).length = σ.length + 1

lemma merge_K : (π <+> acc) K = Dict.First (π K) (acc K)

@[simp]
lemma BalanceProof.valid_initial :
  BalanceProof.initial.Verify (K₁ := K₁) (AD := AD) (K₂ := K₂) (V := V) (M := (C × K₁ × ExtraDataT))

lemma f_transfer_source'
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isTransferBlock},
         T ∈ TransactionsInBlock π block.1) :
  (f σ T) .Source = σ .Source

lemma f_withdrawal_block_source' (h : b.isWithdrawalBlock) :
  ((TransactionsInBlock π b).foldl f σ).1 .Source = σ .Source + ∑ k : K₁, (b.getWithdrawal h k).1 ⊓ σ k

Option.isSome_iff_ne_none in Init.Data.Option.Lemmas

omit [Finite K₂] [LinearOrder K₂] in
private lemma f_withdrawal_block_source_aux {l : List K₁}
  (h₀ : l.Nodup) (h : b.isWithdrawalBlock) :
  (List.foldl f' σ
    (List.map (λ s : K₁ ↦ ⟨(s, Kbar.Source, some (b.getWithdrawal h s)), by unfold Τ'.isValid; aesop⟩) l)).1
                            .Source = σ .Source + ∑ x : K₁, if x ∈ l then (↑(b.getWithdrawal h x) ⊓ σ x) else 0

@[simp]
lemma mergeR''_eq_some {x} :
  acc K = some x → (mergeR'' πs acc) K = acc K

lemma computeBalance_eq_sum : computeBalance σ = computeBalanceSum σ

lemma proposition2' [Setoid' X] {join x y : X} (h : IsLUB {x, y} join) :
  (x ≅ join) ∧ y ≅ join

lemma sum_fStar_le_zero : ∑ (k : Kbar K₁ K₂), fStar Tstar (S.initial K₁ K₂ V) k ≤ 0

lemma isValid_iff : isValid (s, r, v?) ↔ s ≠ r ∧ (s matches .Source → v?.isSome)

lemma merge_left_none_eq_right (h : π K = none) : (π <+> acc) K = acc K

@[simp]
lemma length_TransactionsInBlock_deposit
  {b : { b : Block K₁ K₂ C Sigma V // b.isDepositBlock }} :
  (TransactionsInBlock_deposit b).length = 1

@[simp]
lemma isLUB_some_some_none_none :
  IsLUB {some x, some y, none} .none ↔ False

lemma compat_of_iso (h : π₁ ≅ π₂) : π₁ <≅> π₂

lemma verify_merge_of_valid {π₁ π₂ : BalanceProof K₁ K₂ C Pi V}
                            (h₁ : π₁.Verify (M := (C × K₁ × ExtraDataT)))
                            (h₂ : π₂.Verify (M := (C × K₁ × ExtraDataT))) :
                            BalanceProof.Verify (M := (C × K₁ × ExtraDataT)) (Dict.Merge π₁ π₂)

@[simp]
lemma mem_list_singleton_iff : π ∈ ({acc} : List (BalanceProof K₁ K₂ C Pi V)) ↔ π = acc

lemma appendBlock!_def : σ.appendBlock! request = σ ++ [request.toBlock! σ]

lemma sender_transactionsInBlocks {bs : List (Block K₁ K₂ C Sigma V)}
                                  {π₁ π₂ : BalanceProof K₁ K₂ C Pi V} :
  (TransactionsInBlocks π₁ bs).map (λ s ↦ s.1.1) =
  (TransactionsInBlocks π₂ bs).map (λ s ↦ s.1.1)

lemma length_transactionsInBlock :
  (TransactionsInBlock π₁ b).length = (TransactionsInBlock π₂ b).length

lemma appendBlock_eq_id_of_not_isValid (h : ¬request.isValid) :
  appendBlock σ request = σ

lemma proposition1' [PartialOrder X] {x y : X} {s : Set X}
  (h₁ : IsLUB s x) (h₂ : IsLUB s y) : x = y

lemma mem_of_BalanceProof_le (h : π ≤ π') (h₁ : k ∈ π) : k ∈ π'

lemma iso_of_isLUB [Setoid' X] {x y join : X} (h : IsLUB {x, y} join) : x ≅ y

private theorem monotone_fStarFixed_aux (h : v₁ ≤ v₂) (h₂ : b₁ ≤ b₂) :
                                        v₁.1.foldl f b₁ ≤ v₂.1.foldl f b₂

@[simp]
lemma length_TransactionsInBlock_withdrawal
  {b : { b : Block K₁ K₂ C Sigma V // b.isWithdrawalBlock }} :
  (TransactionsInBlock_withdrawal b).length = Nat.card K₁

lemma aggregateWithdrawals_eq_aggregateWithdrawals' {σ : Scontract K₁ K₂ V C Sigma} :
  aggregateWithdrawals σ = aggregateWithdrawals' σ

@[simp, refl]
lemma iso_rfl : a ≅ a

private lemma valid_mergeR''_aux {π : BalanceProof K₁ K₂ C Pi V}
                                 {πs : List (BalanceProof K₁ K₂ C Pi V)}
                                 {n : ℕ}
  (hn : n < πs.length.succ)
  (h₀ : π.Verify (M := (C × K₁ × ExtraDataT)))
  (h : ∀ π ∈ πs, π.Verify (M := (C × K₁ × ExtraDataT))) :
  (mergeR'' (πs.take n) π).Verify (M := (C × K₁ × ExtraDataT))

@[simp]
lemma le_eq_iso [φ : Setoid' X] {a b : X} : a ≤ b ↔ a ≅ b

@[simp]
lemma deposit_ne_widthdrawal : 
  (deposit s v).isWithdrawalBlock (V := V) (Sigma := Sigma) (C := C) (K₁ := K₁) = False

lemma proposition4W {x y : Option ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V)}
  (h : x.isSome ∧ y.isSome → x = y) : IsLUB {x, y} (Dict.First x y)

lemma s_ne_r_of_complete {t'} (h : isComplete ⟨⟨kb₁, kb₂, v?⟩, t'⟩) : kb₁ ≠ kb₂

@[simp]
lemma isLUB_none_some_iff_False :
  IsLUB {.some x} none ↔ False

lemma receiver_transactionsInBlock :
  (TransactionsInBlock π₁ b).map (λ s ↦ s.1.2.1) =
  (TransactionsInBlock π₂ b).map (λ s ↦ s.1.2.1)

lemma first_right (h : x₁.isNone) : First x₁ x₂ = x₂

@[simp]
lemma transfer_ne_deposit :
  (transfer aggregator extradata commitment senders sigma).isDepositBlock (V := V) = False

@[simp]
lemma attackGameRGo_cons :
  attackGameRGo (request :: requests) σ =
  request.toBlock! σ :: attackGameRGo requests (σ.appendBlock! request)

lemma proposition4 [Setoid' X] {x y : Option X} :
  (∃ join : Option X, IsLUB {x, y, .none} join) ↔ (x ≠ .none ∧ y ≠ .none → x ≅ y)

@[simp]
lemma attackGameBlocks'!_cons :
  attackGameBlocks'! (hd :: requests) σ = attackGameBlocks'! requests (σ ++ [hd.toBlock! σ])

lemma v_transactionsInBlocks {s r v v'} {eq₁ eq₂} {i}
  (h : π ≤ π')
  (h₀ : i < (TransactionsInBlocks π Bstar).length)
  (h₁ : (TransactionsInBlocks π Bstar)[i] = ⟨(s, r, v), eq₁⟩)
  (h₂ : (TransactionsInBlocks π' Bstar)[i]'(by blast with π) = ⟨(s, r, v'), eq₂⟩) :
  v ≤ v'

@[simp]
lemma length_attackGameR : (attackGameR requests σ).length = σ.length + requests.length

lemma f_eq_f' : f = f' (K₁ := K₁) (K₂ := K₂) (V := V)

@[simp]
lemma isLUB_some_some_iff_iso :
  IsLUB {some x} (some y) ↔ some x ≅ some y

lemma lemma4 (h : π₁ ≤ π₂) : Bal π₁ bs ≤ Bal π₂ bs

@[simp]
lemma discretePreorder_eq_equality_Key_Map_Vplus {a b : Key K₁ K₂ → V₊} : a ≤ b ↔ a = b

lemma valid_mergeR' {πs : List (BalanceProof K₁ K₂ C Pi V)} {n : Fin πs.length.succ}
  (h : ∀ π ∈ πs, π.Verify (M := (C × K₁ × ExtraDataT))) :
  (mergeR' πs n).Verify (M := (C × K₁ × ExtraDataT))

@[simp]
lemma v'_zero : v' 0 b s = 0

lemma Merge_iso_of_iso (h : π₁ ≅ π₂) :
  π₁ <+> π₃ ≅ π₂ <+> π₃

lemma batch?_neq_of_mem {π₁k π₂k : Option ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V)}
  (h₀ : π₁k ≠ .none ∧ π₂k ≠ .none)
  (h : ¬(π₁k ≅ π₂k)) : (π₁k.get (Option.isSome_iff_ne_none.2 h₀.1)).2 ≠
                       (π₂k.get (Option.isSome_iff_ne_none.2 h₀.2)).2

@[simp]
lemma isLUB_any_any_none_of_any_any :
  IsLUB {x?, y?, none} join? ↔ IsLUB {x?, y?} join?

@[simp]
lemma discretePreorder_eq_equality_Pi_Prod_ExtraDataT {a b : (Pi × ExtraDataT)} : a ≤ b

private lemma reindex_mem :
  ∀ (a : ℕ) (ha : a ∈ Finset.range (k + 1) \ {0}), reindex a ha ∈ Finset.range k

lemma attackGameRGo_isWithdrawal_iff (σ σ' : Scontract K₁ K₂ V C Sigma)
                                     (h : i < (attackGameRGo requests σ).length) :
  (attackGameRGo requests σ)[i].isWithdrawalBlock ↔
  (attackGameRGo requests σ')[i].isWithdrawalBlock

lemma valid_mergeR'' {πs : List (BalanceProof K₁ K₂ C Pi V)} {n : ℕ}
  (hn : n < πs.length.succ)
  (h : ∀ π ∈ πs, π.Verify (M := (C × K₁ × ExtraDataT))) :
  (mergeR'' (πs.take n) .initial).Verify (M := (C × K₁ × ExtraDataT))

@[simp]
lemma computeBalance'_nil : computeBalance' ([] : Scontract K₁ K₂ V C Sigma) v = v

lemma prop6_general (h : ∀ i : Fin πs.length,
                     IsLUB {mergeR'' (πs.take i.1) .initial, πs[i]} (mergeR'' (πs.take (i.1 + 1)) .initial))
  : IsLUB {π | π ∈ πs} (mergeR'' πs .initial)

@[simp]
lemma initial_Merge {π : BalanceProof K₁ K₂ C Pi V} :
  BalanceProof.initial.Merge π = π

lemma monotone_fStarFixed :
  Monotone λ (Ts : Vector (Τ K₁ K₂ V) n) ↦ Intmax.fStarFixed Ts (S.initial K₁ K₂ V)

@[simp]
lemma some_le_some :
  Option.some x ≤ .some y ↔ x ≤ y

theorem injective {α : Type} [Finite α]
  (f : UniquelyIndexed α) : Function.Injective f

@[symm]
lemma iso_symm : (a ≅ b) ↔ b ≅ a

@[simp]
lemma length_initial : (@initial K₁ K₂ C Sigma V _).length = 0

lemma boundedBelow_sset_boundedBelow_of_le {b₁ b₂ : S K₁ K₂ V} {T₁ T₂ : Τ K₁ K₂ V}
  (h : b₁ ≤ b₂) (h₁ : T₁ ≤ T₂) : boundedBelow b₂ T₂ ⊆ boundedBelow b₁ T₁

private lemma lemma5_aux {len : ℕ} {σ : Scontract K₁ K₂ V C Sigma}
  (hlen : len = σ.length) :
  (Bal π σ) Kbar.Source =
  (∑ x ∈ (Finset.univ : Finset (Fin σ.length)) ×ˢ Finset.univ,
      if h : σ[x.1].isWithdrawalBlock then
        (σ[x.1].getWithdrawal h x.2).1 ⊓ ((Bal π (List.take (x.1.1) σ)) x.2)
      else 0) -
  ∑ i : Fin (List.length σ), if h : σ[i].isDepositBlock then (σ[↑i].getDeposit h).2 else 0

lemma isSome_of_withdrawal
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isWithdrawalBlock},
         T ∈ TransactionsInBlock π block.1) : T.value.isSome

@[simp]
lemma v'_cast_nonneg : 0 ≤ ↑(v' v b' s)

@[simp]
lemma nonneg {s : S K₁ K₂ V} {k : Key K₁ K₂} : 0 ≤ s k

lemma compat_merge_of_compat :
  (∀ π', π' ∈ πs → π <≅> π') → π <≅> (mergeR'' πs .initial)

lemma length_TransactionsInBlock_transfer
  {b : { b : Block K₁ K₂ C Sigma V // b.isTransferBlock }} :
  ∀ (π₁ π₂ : BalanceProof K₁ K₂ C Pi V),
    (TransactionsInBlock_transfer π₁ b).length =
    (TransactionsInBlock_transfer π₂ b).length

@[simp]
lemma mergeR''_nil : mergeR'' [] acc = acc

@[simp]
lemma attackGameRGo_nil :
  attackGameRGo ([] : List (Request K₁ K₂ C Sigma Pi V)) σ = []

lemma monotone_TransactionsInBlocksFixed :
  Monotone λ (π : BalanceProof K₁ K₂ C Pi V) ↦ TransactionsInBlocksFixed π Bstar

lemma merge_ne_none_of_join_ne_none_iso [Setoid' Y] {D₁ D₂ join : Dict X Y} {k}
  (hk : join k ≠ .none) (h : IsLUB {D₁, D₂} join) : Dict.Merge D₁ D₂ k ≠ .none

private lemma isWithdrawalRequest_of_isWithdrawalBlock_aux {i : ℕ}
  (h₀ : ∀ request ∈ requests, request.isValid)
  (hi₁ : σ.length ≤ i)
  (hi₂ : i < (attackGameR requests σ).length)
  (h₁ : ((attackGameR requests σ)[i]'(by simp; simp at hi₂; exact hi₂)).isWithdrawalBlock) :
  (requests[i - σ.length]'(by rcases i with _ | i <;> rcases requests with _ | ⟨hd, tl⟩
                              · simp at hi₂; omega
                              · simp
                              · simp at hi₂; omega
                              · simp at hi₂ ⊢; omega)) matches .withdrawal ..

@[simp]
lemma aggregateDeposits_cons {hd} {tl : List (Block K₁ K₂ C Sigma V)} :
  aggregateDeposits (hd :: tl) =
  (if h : hd.isDepositBlock
   then (hd.getDeposit h).2.1
   else 0) +
  aggregateDeposits tl

lemma batch_eq_iff {π₁k π₂k : (Pi × ExtraDataT) × TransactionBatch K₁ K₂ V} :
  (π₁k ≅ π₂k) ↔ π₁k.2 = π₂k.2

@[simp]
lemma BalanceProof.snd_discrete {x y : TransactionBatch K₁ K₂ V} :
  @LE.le (TransactionBatch K₁ K₂ V) Preorder.toLE x y ↔ x = y

lemma V'_sset_V'_of_le {b₁ b₂ : S K₁ K₂ V} {T₁ T₂ : Τ K₁ K₂ V} {k : Kbar K₁ K₂}
  (h : b₁ ≤ b₂) (h₁ : T₁ ≤ T₂) : 
  V' b₂ T₂ k ⊆ V' b₁ T₁ k

congr_fun in Batteries.Logic

lemma le_mergeR''_aux {π acc : BalanceProof K₁ K₂ C Pi V}
                      {πs : List (BalanceProof K₁ K₂ C Pi V)}
                      {k : C × K₂}
                      (h₀ : π k ≤ acc k)
                      (h : ∀ acc : BalanceProof K₁ K₂ C Pi V, acc ∈ πs → π k ≤ acc k) :
                      π k ≤ mergeR'' πs acc k

lemma Block.updateBalance_eq_zero :
  block.updateBalance v = v + block.updateBalance 0

@[simp]
lemma none_iso_some : (.none ≅ some x) ↔ False

lemma merge_lem :
  mergeR'' (π :: πs) BalanceProof.initial = π <+> (mergeR'' πs BalanceProof.initial)

lemma f_deposit_source
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isDepositBlock},
         T ∈ TransactionsInBlock π block.1) :
  (f σ T) .Source = σ .Source + -T.value.get (isSome_of_deposit h)

lemma isSome_of_deposit
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isDepositBlock},
         T ∈ TransactionsInBlock π block.1) : T.value.isSome

@[simp]
lemma TransactionsInBlocks_cons {π : BalanceProof K₁ K₂ C Pi V}
                                {hd}
                                {tl : List (Block K₁ K₂ C Sigma V)} :
  TransactionsInBlocks π (hd :: tl) =
  TransactionsInBlock π hd ++ (List.map (TransactionsInBlock π) tl).flatten

lemma f_withdrawal_block_source (h : b.isWithdrawalBlock) :
  ((TransactionsInBlock π b).foldl f σ) .Source = σ .Source + ∑ k : K₁, (b.getWithdrawal h k).1 ⊓ σ k

lemma Merge_comm_of_compat (h : π₁ <≅> π₂) : π₁ <+> π₂ ≅ π₂ <+> π₁

@[simp]
lemma isValid_coe {s : S K₁ K₂ V} : S'.isValid (V := V) (K₁ := K₁) (K₂ := K₂) ↑s

@[simp]
lemma isLUB_some_some_none :
  IsLUB {some x, some y} .none ↔ False

@[simp]
lemma fStar_nil : fStar [] s = s

@[mono]
lemma fc_mono {τc τc' : Τc K₁ K₂ V} {b₁ b₂ : S K₁ K₂ V}
              (h : (τc, b₁) ≤ (τc', b₂)) : fc (τc, b₁) ≤ fc (τc', b₂)

@[simp]
lemma initial_eq_zero {k : Kbar K₁ K₂} : initial K₁ K₂ V k = 0

theorem theorem1 : ¬adversaryWon (attackGame requests)

lemma proposition5' [Preorder Y] {f g h join' : X → Y}
  (h₀ : IsLUB {f, g} join')
  (h₁ : ∀ x, h x ≅ join' x) :
  join' ≅ h

@[simp]
lemma deposit_ne_transfer : 
  (deposit s v).isTransferBlock (V := V) (Sigma := Sigma) (C := C) (K₁ := K₁) = False

lemma f_deposit_source''
  (h : b.isDepositBlock) (h₁ : T ∈ TransactionsInBlock π b) : 
  (f σ T).1 .Source = σ .Source + -T.value.get (isSome_of_deposit ⟨⟨b, h⟩, h₁⟩)

@[simp]
lemma mergeR''_append :
  mergeR'' (πs ++ πs') acc = mergeR'' πs' (mergeR'' πs acc)

@[simp]
lemma bal_nil : Bal (Sigma := Sigma) π [] = S.initial K₁ K₂ V

lemma proposition3''
  (h : IsLUB {x, y} join)
  (h' : IsLUB {.some x, .some y, .none} join'?) :
  .some join ≅ join'?

lemma iso_K_merge_right_of_ne_none_compat (h : π K ≠ none) (h : π <≅> acc) :
  π K ≅ (acc <+> π) K

@[simp]
lemma bs_initial : (@initial K₁ K₂ C Sigma V _) = []

lemma toBlock!_of_deposit (h : request matches .deposit ..) :
  request.toBlock! σ matches .deposit ..

lemma toBlock_eq_id_of_not_isValid (h : ¬request.isValid) :
  (toBlock σ request) = .none

@[simp]
lemma withdrawal_ne_deposit :
  (withdrawal ws).isDepositBlock (V := V) (Sigma := Sigma) (C := C) (K₂ := K₂) = False

lemma le_of_iso (h : π₂ ≅ π₃) (h₁ : π₁ ≤ π₂) : π₁ ≤ π₃

@[simp]
lemma discretePreorder_eq_equality_Vplus {a b : V₊} : a ≤ b ↔ a = b

@[simp]
lemma length_attackGameBlocks'! :
  (attackGameBlocks'! requests σ).length = σ.length + requests.length

lemma mergeR'_succ {πs : List (BalanceProof K₁ K₂ C Pi V)} {n : ℕ} (h : n + 1 < πs.length.succ) :
  mergeR' πs ⟨n + 1, h⟩ = (mergeR' πs ⟨n, by omega⟩).Merge (πs[n])

@[simp]
lemma fStar_cons {hd : Τ K₁ K₂ V} {tl : List (Τ K₁ K₂ V)} :
  fStar (hd :: tl) s = fStar tl (f s hd)

lemma attackGameBlocks'r_eq_attackGameBlocks' :
  attackGameBlocks'! requests σ = attackGameBlocks'!r requests σ

private theorem lt_iff_le_not_le {k₁ k₂ : Key K₁ K₂} : k₁ < k₂ ↔ k₁ ≤ k₂ ∧ ¬k₂ ≤ k₁

@[simp]
lemma snd_eq_of_iso {d₁ d₂ : (Pi × ExtraDataT) × TransactionBatch K₁ K₂ V} :
  d₁.2 = d₂.2 ↔ (d₁ ≅ d₂)

private lemma BalFixed_eq_BalFixed' : BalFixed bs π = BalFixed' bs π

@[simp]
lemma BalanceProof.compat_rfl : π₁ <≅> π₁

lemma compat_lem {π π' π'': BalanceProof K₁ K₂ C Pi V} :
  π <≅> π' → π <≅> π'' → π <≅> (π' <+> π'')

lemma notin_of_BalanceProof_le_notin (h : π ≤ π') (h₁ : k ∉ π') : k ∉ π

lemma sender_transactionsInBlock :
  (TransactionsInBlock π₁ b).map (λ s ↦ s.1.1) =
  (TransactionsInBlock π₂ b).map (λ s ↦ s.1.1)

theorem Function.injective_of_CryptInjective
  {α ω : Type} [Nonempty ω] {f : α → ω} [inj : Injective f] : Function.Injective f

lemma exists_key_of_isValid (h : isValid (s, r, (none : Option V₊))) : ∃ k : Key K₁ K₂, s = k

lemma mergeR'_eq_mergeR_of_lt {n : ℕ} (h : n < πs.length.succ) :
  mergeR' πs ⟨n, h⟩ = mergeR πs n

lemma first_left (h : x₁.isSome) : First x₁ x₂ = x₁

lemma eq_of_BalanceProof_le (h : π ≤ π') (h₁ : k ∈ π) (h₂ : k ∈ π') :
  ((π k).get h₁).2 = ((π' k).get h₂).2

@[simp]
lemma getDeposit_deposit {r : K₂} {v : V₊} :
  getDeposit (.deposit r v) (by aesop) = (r, v)

lemma merge_le (h₁ : π₁ ≤ π₃) (h₂ : π₂ ≤ π₃) : π₁ <+> π₂ ≤ π₃

lemma proposition3' : 
  (∃ join : X, IsLUB {x, y} join) ↔ (∃ join : Option X, IsLUB {.some x, .some y, .none} join)

lemma isWithdrawalRequest_of_isWithdrawalBlock
  (h₀ : ∀ request ∈ requests, request.isValid)
  (i : Fin (attackGameR requests []).length)
  (h₁ : ((attackGameR requests [])[i]'(by simp; rcases i with ⟨i, hi⟩; simp at hi; exact hi)).isWithdrawalBlock) :
  (requests[i]'(by rcases i with ⟨h, hi⟩; rcases requests with _ | ⟨hd, tl⟩
                   · simp at hi
                   · simp at hi ⊢; omega)) matches .withdrawal ..

@[simp]
lemma some_le_none_eq_False : .some x ≤ none ↔ False

lemma isValid_initial : (initial K₁ K₂ V).isValid

lemma le_Merge_of_le_le
        {π π₁ π₂ : BalanceProof K₁ K₂ C Pi V}
        {k : C × K₂}
        (h : π k ≤ π₁ k)
        (h₁ : π k ≤ π₂ k) :
        π k ≤ Dict.Merge π₁ π₂ k

lemma proposition5 [Preorder Y] {f g : X → Y} {join : X → Y} :
  IsLUB {f, g} join ↔ ∀ x : X, IsLUB {f x, g x} (join x)

lemma receiver_transactionsInBlocks {bs : List (Block K₁ K₂ C Sigma V)}
                                    {π₁ π₂ : BalanceProof K₁ K₂ C Pi V} :
  (TransactionsInBlocks π₁ bs).map (λ s ↦ s.1.2.1) =
  (TransactionsInBlocks π₂ bs).map (λ s ↦ s.1.2.1)

@[simp]
lemma Block.updateBalance_transfer {a : K₁} {b : ExtraDataT} {c : C} {d : List K₂} (e : Sigma) :
  (Block.transfer a b c d e).updateBalance v = v

lemma f_transfer_source
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isTransferBlock},
         T ∈ TransactionsInBlock π block.1) :
  (f σ T) .Source = σ .Source

@[simp]
lemma v'_self {h} : v' ⟨(b s), h⟩ b s = ⟨b s, h⟩

@[simp]
lemma isLUB_some_some_none_of_some :
  IsLUB {.some x, .some y, none} y? ↔ IsLUB {.some x, .some y} y?

@[simp]
lemma Merge_initial {π : BalanceProof K₁ K₂ C Pi V} :
  π.Merge BalanceProof.initial = π

lemma compat_comm : (π₁ <≅> π₂) ↔ π₂ <≅> π₁

lemma le_of_iso' (h : π₁ ≅ π₂) (h₁ : π₂ ≤ π₃) : π₁ ≤ π₃

@[simp]
lemma BalanceProof.le_initial :
  BalanceProof.initial k ≤ π k

@[simp]
lemma transfer_ne_widthdrawal : 
  (transfer aggregator extradata commitment senders sigma).isWithdrawalBlock (V := V) = False

lemma f_deposit_source'
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isDepositBlock},
         T ∈ TransactionsInBlock π block.1) :
  (f σ T).1 .Source = σ .Source + -T.value.get (isSome_of_deposit h)

lemma length_transactionsInBlocks {bs : List (Block K₁ K₂ C Sigma V)}
                                  {π₁ π₂ : BalanceProof K₁ K₂ C Pi V} :
  (TransactionsInBlocks π₁ bs).length = (TransactionsInBlocks π₂ bs).length

lemma Merge_mergeR''_comm {πs : List (BalanceProof K₁ K₂ C Pi V)} (h : π <≅> acc) :
  acc <+> (mergeR'' πs π) ≅ π <+> (mergeR'' πs acc)

@[simp]
lemma transactionsInBlocks_nil :
  TransactionsInBlocks (Pi := Pi) (K₁ := K₁) (K₂ := K₂) (V := V) (C := C) (Sigma := Sigma) π [] = []

@[simp]
lemma transactionsInBlocks_append_singleton :
  TransactionsInBlocks π (bs ++ [b]) =
  (TransactionsInBlocks π bs) ++ (TransactionsInBlock π b)

lemma lemma5 (π : BalanceProof K₁ K₂ C Pi V) :
  Bal π σ .Source =
  (∑ (i : Fin σ.length) (k : K₁),
     if h : σ[i].isWithdrawalBlock
     then let w := σ[i].getWithdrawal h
          w k ⊓ Bal π (σ.take i.1) k
     else 0)
  -
  aggregateDeposits σ

lemma isSome_getDeposit?_of_isDepositBlock {b : Block K₁ K₂ C Sigma V}
  (h : b.isDepositBlock) : b.getDeposit?.isSome

@[symm]
lemma BalanceProof.compat_comm : π₁ <≅> π₂ ↔ π₂ <≅> π₁
</all_available_lemmas>

<local_ctx>
import Mathlib.Algebra.Order.Ring.Unbundled.Nonneg

import Mathlib.Data.Finite.Defs

import Mathlib.Data.Finmap

import Mathlib.Data.List.Intervals

import Mathlib.Data.Set.Image

import Mathlib.Logic.Embedding.Basic

import Mathlib.Tactic

import FVIntmax.Wheels.Wheels

namespace Intmax

namespace CryptoAssumptions

section Hashing

class Injective {α ω : Type} (f : α → ω) where
  h : ComputationallyInfeasible (¬ Function.Injective f)

end Hashing

end CryptoAssumptions

section UniquelyIndexed

prefix:max "!" => UniqueTokenT

namespace UniquelyIndexed

end UniquelyIndexed

end UniquelyIndexed

section NonNeg

postfix:max "₊" => NonNeg

section Nonneg

variable {α : Type} [PreWithZero α] {v : α₊}

end Nonneg

end NonNeg

section Order

section VectorPreorder

open Mathlib

variable {α : Type} [Preorder α] {n : ℕ}
         {v₁ v₂ v₃ : Vector α n}

namespace Vec

def le (v₁ v₂ : Vector α n) :=
  ∀ x ∈ (v₁.1.zip v₂.1), x.1 ≤ x.2
</local_ctx>

<target_theorem>
lemma le_trans (h₁ : v₁ ≤ v₂) (h₂ : v₂ ≤ v₃) : v₁ ≤ v₃ :=
</target_theorem>

