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 CommitT (C K Pi : Type) where
  commitment : C
  dict       : Dict K Pi

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

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

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

correct_consistent :
    ∀ {dict : Dict K M} {key : K} (h : key ∈ dict.keys), 
      Verify (Commit dict)[key] key dict[key] (Commit dict).commitment = true

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

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

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

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

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

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

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

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

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

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⟩

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

private def Bal' (bs : List (Block K₁ K₂ C Sigma V)) : BalanceProof K₁ K₂ C Pi V → S K₁ K₂ V :=
  fStar (s₀ := S.initial K₁ K₂ V) ∘ TransactionsInBlocks (bs := bs)

private def fStarFixed {n : ℕ}
  (Ts : Vector (Τ K₁ K₂ V) n) (s₀ : S K₁ K₂ V) : S K₁ K₂ V :=
  fStar Ts.1 s₀

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)

private def BalFixed' (bs : List (Block K₁ K₂ C Sigma V)) : BalanceProof K₁ K₂ C Pi V → S K₁ K₂ V :=
  fStarFixed (n := (length_of_TransactionsInBlocks (Pi := Pi) bs).1)
             (s₀ := S.initial K₁ K₂ V) ∘ TransactionsInBlocksFixed (Pi := Pi) (bs := bs)

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

def isValid (s : S' K₁ K₂ V) := ∀ k : Kbar K₁ K₂, k matches .Source ∨ 0 ≤ s k

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

def initial (K₁ K₂ V : Type) [PreWithZero V] : S K₁ K₂ V :=
  ⟨S'.initial K₁ K₂ V, S'.isValid_initial⟩

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

def Block.updateBalance (bal : V) (block : Block K₁ K₂ C Sigma V) : V :=
  match block with
   
  | .deposit _ v  => bal + v
   
  | .transfer ..  => bal
   
  | .withdrawal B => bal - ∑ k : K₁, (B k).1

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

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 attackGameBlocks' : Scontract K₁ K₂ V C Sigma :=
  requests.foldl Scontract.appendBlock σ

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

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

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 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 attackGameR : Scontract K₁ K₂ V C Sigma :=
  σ ++ attackGameRGo requests σ

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

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

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

def computeBalance (blocks : Scontract K₁ K₂ V C Sigma) : V :=
  computeBalance' blocks 0

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

def aggregateDeposits (σ : Scontract K₁ K₂ V C Sigma) : V :=
  ∑ i : Fin σ.length,
    if h : σ[i].isDepositBlock
    then (σ[i.1].getDeposit h).2.1
    else 0

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

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

def computeBalanceSum (σ : Scontract K₁ K₂ V C Sigma) :=
  let v_deposited : V := aggregateDeposits σ
  let v_withdrawn : V := aggregateWithdrawals σ
  v_deposited - v_withdrawn

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

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

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 σ

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

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

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 = σ

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)

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

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

abbrev Dict (α ω : Type) : Type := α → Option ω

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

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

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

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

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

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

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

abbrev keysUneq (k₂ : K₂) (k : Key K₁ K₂) : Prop :=
  match k with
  | .inl _   => True
  | .inr k₂' => k₂ ≠ k₂'

abbrev ExtraDataT : Type := ℕ

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

def isValid (τ : Τ' K₁ K₂ V) :=
  match τ with
  | (s, r, v) => s ≠ r ∧ (s matches .Source → v.isSome)

@[aesop norm (rule_sets := [Intmax.aesop_valid])]

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

def isComplete (τ : Τ K₁ K₂ V) :=
  match τ with | ⟨(_, _, v), _⟩ => v.isSome

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

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

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

inductive Request where
  | deposit (recipient : K₂) (amount : V₊)
  | transfer (aggregator : K₁) (extradata : ExtraDataT) (commitment : C) (senders : List K₂) (sigma : Sigma)
  | withdrawal (π : BalanceProof K₁ K₂ C Pi V)

def Request.isValid (request : Request K₁ K₂ C Sigma Pi V) : Bool :=
  match request 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))

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

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

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

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

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

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

abbrev TransactionBatch (K₁ : Type) [Finite K₁]
                        (K₂ : Type) [Finite K₂]
                        (V : Type) [PreWithZero V] :=
  Key K₁ K₂ → V₊

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

abbrev UniqueTokenT (α : Type) [Finite α] : Type := Fin (Finite.exists_equiv_fin α |>.choose)

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

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

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

def trivialPreorder {α : Type} : Preorder α :=
  {
    lt := λ _ _ ↦ False
    le := λ _ _ ↦ True
    le_refl := by admit /- proof elided -/

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

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

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

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

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

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

def TransactionsInBlocks
  (π : BalanceProof K₁ K₂ C Pi V) (bs : List (Block K₁ K₂ C Sigma V)) : List (Τ K₁ K₂ V) :=
  (bs.map (TransactionsInBlock π)).flatten

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

def v' (v : V₊) (b : S K₁ K₂ V) (s : Kbar K₁ K₂) : V₊ :=
  match h : s with
  | .Source => v
  | .key _  => ⟨v ⊓ b s, by admit /- proof elided -/
  ⟩

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

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 V' (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) (k : Kbar K₁ K₂) : Set V :=
  { v : V | v ∈ (fc · k) '' boundedBelow b T }

def f' (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) : S K₁ K₂ V := 
  ⟨
    λ k ↦
      match h : T with
      | ⟨(_, _, .some _), hT⟩ => fc (⟨T, by admit /- proof elided -/
      ⟩, b) k
      | ⟨(s, _, .none), _⟩ => if k = s then 0 else b k,
    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 -/
  ⟩

def infV (b : S K₁ K₂ V) (T : Τ K₁ K₂ V) (k : Kbar K₁ K₂) :
  InfSet V where
    sInf := λ s ↦ if s = V' b T k
                  then (exists_inf b T).1 k
                  else 0

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

def fStar (Ts : List (Τ K₁ K₂ V)) (s₀ : S K₁ K₂ V) : S K₁ K₂ V :=
  Ts.foldl f s₀

def Bal (π : BalanceProof K₁ K₂ C Pi V) (bs : List (Block K₁ K₂ C Sigma V)) : S K₁ K₂ V :=
  fStar (TransactionsInBlocks π bs) (.initial K₁ K₂ V)

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

Finset in Mathlib.Data.Finset.Defs

IsBot in Mathlib.Order.Max

Sigma.fst in Init.Core

Nat.card in Mathlib.SetTheory.Cardinal.Finite

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

upperBounds in Mathlib.Order.Bounds.Defs

Bool in Init.Prelude

Option in Init.Prelude

OfNat in Init.Prelude

LT in Init.Prelude

Set in Mathlib.Data.Set.Defs

Multiset.filter in Mathlib.Data.Multiset.Filter

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

Fintype in Mathlib.Data.Fintype.Defs

Multiset.dedup in Mathlib.Data.Multiset.Dedup

instance : Preorder (Pi × ExtraDataT) := trivialPreorder

Std.Associative in Init.Core

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

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

Subtype in Init.Prelude

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

Multiset.ofList in Mathlib.Data.Multiset.Defs

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

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

List.lookup in Init.Data.List.Basic

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

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

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

Function.eval in Mathlib.Logic.Function.Basic

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

List in Init.Prelude

List.attach in Init.Data.List.Attach

Coe in Init.Coe

instance latticePreorder : Preorder V := inferInstance

Finset.univ in Mathlib.Data.Fintype.Defs

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

Zero in Init.Prelude

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

Unit in Init.Prelude

Multiset.Nodup in Mathlib.Data.Multiset.Defs

Multiset in Mathlib.Data.Multiset.Defs

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

flip in Init.Core

List.map in Init.Prelude

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

Lean.Parser.Tactic.replace in Init.Tactics

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

def initial (K₁ K₂ V : Type) [Zero V] : S' K₁ K₂ V := λ _ ↦ 0

Sigma.mk in Init.Core

absurd in Init.Prelude

instance [PreWithZero V] : Inhabited (S K₁ K₂ V) := ⟨S.initial K₁ K₂ V⟩

Lattice in Mathlib.Order.Lattice

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

List.finRange in Init.Data.List.FinRange

List.concat in Init.Prelude

Finset.range in Mathlib.Data.Finset.Range

IsTotal in Mathlib.Order.Defs.Unbundled

iInf in Mathlib.Order.SetNotation

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 univKbar : Kbar K₁ K₂ ≃ Key K₁ K₂ ⊕ Unit :=
  {
    toFun := λ kbar ↦ match kbar with | .key k => k | .Source => ()
    invFun := λ sum ↦ match sum with | .inl k => .key k | .inr _ => .Source
    left_inv := by admit /- proof elided -/

Function.RightInverse in Init.Data.Function

Subtype.val in Init.Prelude

inferInstanceAs in Init.Prelude

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₂'

IsLUB in Mathlib.Order.Bounds.Defs

IsGreatest in Mathlib.Order.Bounds.Defs

Finset.toList in Mathlib.Data.Finset.Dedup

Prod.fst in Init.Prelude

instance : Nonempty ExtraDataT := inferInstanceAs (Nonempty ℕ)

Preorder in Mathlib.Order.Defs.PartialOrder

instance : PreWithZero α₊ :=

Set.range in Mathlib.Data.Set.Operations

IsGLB in Mathlib.Order.Bounds.Defs

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

IsTrans in Mathlib.Order.Defs.Unbundled

Inhabited in Init.Prelude

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

Membership in Init.Prelude

Prod.snd in Init.Prelude

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

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

noncomputable instance {α : Type} [Lattice α] [Zero α] : PreWithZero α := inferInstance

def getDeposit? (b : Block K₁ K₂ C Sigma V) : Option (K₂ × V₊) :=
  match b with
  | deposit r v => .some (r, v)
  | transfer .. | withdrawal .. => .none

DecidableEq in Init.Prelude

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

Prod in Init.Prelude

List.zipWith in Init.Data.List.Basic

LinearOrder in Mathlib.Order.Defs.LinearOrder

Sigma in Init.Core

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

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

LE in Init.Prelude

CoeFun in Init.Coe

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

Eq in Init.Prelude

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

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

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

Multiset.map in Mathlib.Data.Multiset.MapFold

def mergeR (πs : List (BalanceProof K₁ K₂ C Pi V)) (n : ℕ) : BalanceProof K₁ K₂ C Pi V :=
  if _ : n < πs.length.succ
  then match n with
       | 0 => .initial
       | k + 1 => Dict.Merge (mergeR πs k) πs[k]
  else .initial

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

Function.LeftInverse in Init.Data.Function

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

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

Preorder.toLE in Mathlib.Order.Defs.PartialOrder

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

List.NodupKeys in Mathlib.Data.List.Sigma

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

abbrev KₚT : Type := ℕ

List.take in Init.Data.List.Basic

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

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

Decidable in Init.Prelude

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₂'

IsAntisymm in Mathlib.Order.Defs.Unbundled

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

Finset.sort in Mathlib.Data.Finset.Sort

instance (priority := high) : LE (Kbar K₁ K₂) := ⟨(·=·)⟩

Option.isSome in Init.Data.Option.Basic
</all_available_defs>

<all_available_lemmas>
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 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 σ

private lemma Bal'_eq_Bal : Bal' bs π = Bal π bs

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

lemma TransactionsInBlocksFixed_le_of_TransactionsInBlocks
  (h : ∀ i : Fin (length_of_TransactionsInBlocks bs).1,
    (TransactionsInBlocks π bs)[i]'(by blast with π i) ≤
    (TransactionsInBlocks π' bs)[i]'(by blast with π' i)) :
  TransactionsInBlocksFixed π bs ≤ TransactionsInBlocksFixed π' bs

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'

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

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'

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

lemma monotone_f (h₁ : b₁ ≤ b₂) (h₂ : T₁ ≤ T₂) : f b₁ T₁ k ≤ f b₂ T₂ k

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

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

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

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

lemma appendBlock_eq_appendBlock!_of_isValid (h : request.isValid) :
  appendBlock σ request = appendBlock! σ request

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

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

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

private lemma reindex_inj :
  ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ Finset.range (k + 1) \ {0})
    (a₂ : ℕ) (ha₂ : a₂ ∈ Finset.range (k + 1) \ {0}),
  reindex a₁ ha₁ = reindex a₂ ha₂ → a₁ = a₂

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

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

lemma computeBalance'_eq_zero : computeBalance' σ v = v + computeBalance' σ 0

private lemma computeBalance_eq_sum_aux : computeBalance' σ v = v + computeBalanceSum σ

lemma computeBalance_eq_sum : computeBalance σ = computeBalanceSum σ

lemma attackGameR_eq_attackGameBlocks' :
  attackGameR requests σ = attackGameBlocks'!r requests σ

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

lemma attackGameBlocks_eq_attackGameR :
  attackGameBlocks! requests = attackGameR requests []

lemma attackGameBlocks'_eq_attackGameBlocks'!_normalise :
  attackGameBlocks' requests σ = attackGameBlocks'! (normalise requests) σ

lemma attackGame_eq_attackGameBlocks!_normalise :
  attackGame requests = attackGameBlocks! (normalise requests)

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

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

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

lemma lemma3 : Bal π bs .Source ≤ 0

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

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

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

@[trans]
lemma iso_trans : (a ≅ b) → (b ≅ c) → a ≅ c

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

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

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

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

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

lemma proposition4' [Setoid' X] {join x y : Option X} (h : IsLUB {x, y, .none} join) :
  join ≅ Dict.First x y

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 proposition5' [Preorder Y] {f g h join' : X → Y}
  (h₀ : IsLUB {f, g} join')
  (h₁ : ∀ x, h x ≅ join' x) :
  join' ≅ h

lemma proposition6_aux [Setoid' Y] {D₁ D₂ : Dict X Y}
  (h : ∀ k, D₁ k ≠ .none ∧ D₂ k ≠ .none → D₁ k ≅ D₂ k) : IsLUB {D₁, D₂} (Dict.Merge D₁ D₂)

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

lemma proposition6' [Setoid' Y] {D₁ D₂ join : Dict X Y} (h : IsLUB {D₁, D₂} join) :
  join ≅ Dict.Merge D₁ D₂

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

lemma getElem_Ico_of_lt {m n : ℕ} (h : n < m) : (List.Ico 0 m)[n]'(by simp [h]) = n

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

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

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

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 v'_cast_nonneg : 0 ≤ ↑(v' v b' s)

@[simp]
lemma none_le : Option.none ≤ .some x

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

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

theorem nodup_filter_of_nodup [DecidableEq α] [DecidablePred P]
  (h : m.Nodup) : (Multiset.filter P m).Nodup

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

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 some_le_none_eq_False : .some x ≤ none ↔ False

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

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)

@[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 toBlock!_of_deposit (h : request matches .deposit ..) :
  request.toBlock! σ matches .deposit ..

private lemma V'_eq_range {b : S K₁ K₂ V} {T : Τ K₁ K₂ V} {k : Kbar K₁ K₂} :
  V' b T k =
  Set.range λ (x : { x : (Τc K₁ K₂ V × S K₁ K₂ V) // (T, b) ≤ (↑x.1, x.2) }) ↦ fc ↑x k

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

lemma keys_Merge_left' (h : ∀ x, x ∈ D₁) : Merge D₁ D₂ = D₁

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

@[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 isSome_of_complete {t'} (h : isComplete ⟨⟨kb₁, kb₂, v?⟩, t'⟩) : v?.isSome

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

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

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

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

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

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

Option.isSome_iff_ne_none in Init.Data.Option.Lemmas

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

lemma map_eq_project_triple {β γ δ : Type}
                            {s : β} {r : γ} {v : δ}
                            {i : ℕ}
                            {P : (β × γ × δ) → Prop}
                            {l : List (Subtype P)}
                            {h₀}
                            {h : i < l.length} : 
  l[i]'h = ⟨(s, r, v), h₀⟩ → (l[i]'h).1.2.2 = v

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

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)

@[simp]
lemma isComplete_none {t'} : ¬isComplete ⟨⟨kb₁, kb₂, (.none : Option V₊)⟩, t'⟩

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

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

@[simp]
lemma Block.updateBalance_deposit {r : K₂} {v : V} {vplus : V₊} :
  (Block.deposit r vplus).updateBalance (K₁ := K₁) (C := C) (Sigma := Sigma) v = v + vplus

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 mergeR'_eq_mergeR_of_lt {n : ℕ} (h : n < πs.length.succ) :
  mergeR' πs ⟨n, h⟩ = mergeR πs n

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

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

lemma isLUB_of_isLUB_iso (h : IsLUB A π₁) (h₁ : π₁ ≅ π₂) : IsLUB A π₂

lemma toBlock_σ_isWithdrawalBlock (σ σ' : Scontract K₁ K₂ V C Sigma) :
  (request.toBlock! σ).isWithdrawalBlock ↔
  (request.toBlock! σ').isWithdrawalBlock

lemma setoid_rewrite_LUB {X : Type} {s : Set X} [Setoid' X] {x y : X} (h₁ : IsLUB s x) (h₂ : x ≅ y) :
  IsLUB s y

lemma le_cons
  (eq₁ : v₁ = ⟨hd₁ :: tl₁, len₁⟩) (eq₂ : v₂ = ⟨hd₂ :: tl₂, len₂⟩)
  (h : v₁ ≤ v₂) : hd₁ ≤ hd₂ ∧
  @LE.le (Vector α n) vectorPreorder.toLE ⟨tl₁, by simp at len₁; assumption⟩ ⟨tl₂, by simp at len₂; assumption⟩

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

lemma f_withdraw_source''
  (h : b.isWithdrawalBlock) (h₁ : T ∈ TransactionsInBlock π b) : 
  (f σ T).1 .Source = σ .Source + (↑(T.value.get (isSome_of_withdrawal ⟨⟨b, h⟩, h₁⟩)) ⊓ σ T.sender)

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

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

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

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

@[simp]
lemma attackGameR_cons :
  attackGameR (request :: requests) σ =
  σ ++ attackGameRGo (request :: requests) σ

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 toBlock_σ_matches_withdrawal (σ σ' : Scontract K₁ K₂ V C Sigma) :
  request.toBlock! σ matches .withdrawal .. ↔
  request.toBlock! σ' matches .withdrawal ..

@[simp]
lemma fc_key : 0 ≤ fc (τc, b) (.key k)

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

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 notin_of_BalanceProof_le_notin (h : π ≤ π') (h₁ : k ∉ π') : k ∉ π

@[simp]
lemma isComplete_some {t'} : isComplete ⟨⟨kb₁, kb₂, .some v⟩, t'⟩

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

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 mem_list_singleton_iff : π ∈ ({acc} : List (BalanceProof K₁ K₂ C Pi V)) ↔ π = acc

@[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 toBlock!_of_transfer (h : request matches .transfer ..) :
  request.toBlock! σ matches .transfer ..

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

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)

theorem nodup_map_of_pres_keys_nodup
  (h : ∀ x, Sigma.fst (f x) = x) (h₁ : m.Nodup) : (Multiset.map f m).Nodup

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

lemma isValid_some_of_ne {v : V₊} (h : s ≠ r) : Τ'.isValid (s, r, some v)

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

lemma zip_eq_iff {α β : Type}
  {l₁ l₃ : List α} {l₂ l₄ : List β}
  (h : l₁.length = l₂.length)
  (h₁ : l₂.length = l₃.length)
  (h₂ : l₃.length = l₄.length) :
  List.zip l₁ l₂ = List.zip l₃ l₄ ↔ l₁ = l₃ ∧ l₂ = l₄

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

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

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

theorem keys_map_eq (h : ∀ x, Sigma.fst (f x) = x) : (List.map f m).keys = m

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

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

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

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

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

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

congr_fun in Batteries.Logic

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

@[simp]
lemma getWithdrawal_isSome :
  request.getWithdrawal.isSome ↔ request matches .withdrawal ..

@[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 isLUB_none_some_iff_False :
  IsLUB {.some x} none ↔ False

@[simp]
lemma discretePreorder_eq_equality_Kbar {a b : Kbar K₁ K₂} : a ≤ b ↔ a = b

theorem keys_map_eq (h : ∀ x, Sigma.fst (f x) = x) : (Multiset.map f m).keys = m

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

lemma Block.updateBalance_of_transfer (h : block.isTransferBlock) :
  block.updateBalance v = v

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

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

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

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

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

theorem nodup_map_of_pres_keys_nodup
  (h : ∀ x, Sigma.fst (f x) = x) (h₁ : m.Nodup) : (List.map f m).Nodup

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 BalanceProof.le_initial :
  BalanceProof.initial k ≤ π k

@[simp]
lemma nonneg_coe {s : S K₁ K₂ V} {k : Key K₁ K₂} : 0 ≤ (↑s : S' K₁ K₂ V) k

lemma s_ne_r_of_isValid (h : isValid ⟨s, r, v?⟩) : s ≠ r

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

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

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

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 deposit_ne_widthdrawal : 
  (deposit s v).isWithdrawalBlock (V := V) (Sigma := Sigma) (C := C) (K₁ := K₁) = False

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

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

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

@[simp]
lemma appendBlock!_nil : Scontract.appendBlock! [] request = [request.toBlock! []]

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

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

lemma le_of_iso (h : π₂ ≅ π₃) (h₁ : π₁ ≤ π₂) : π₁ ≤ π₃
</all_available_lemmas>

<local_ctx>
import FVIntmax.AttackGame

import FVIntmax.Lemma3

import FVIntmax.Lemma4

import FVIntmax.Lemma5

import FVIntmax.Propositions

import FVIntmax.Request

import FVIntmax.Wheels

import FVIntmax.Wheels.AuthenticatedDictionary

import FVIntmax.Wheels.SignatureAggregation

import Mathlib

namespace Intmax

open Classical

noncomputable section Intmax

noncomputable section theorem1

section AttackGame

variable {Sigma Pi M : Type}
         {C : Type} [Nonempty C]
         {V : Type}
         [Lattice V] [AddCommGroup V]
         [CovariantClass V V (· + ·) (· ≤ ·)]
         [CovariantClass V V (Function.swap (· + ·)) (· ≤ ·)]
         {K₁ : Type} [Nonempty K₁] [Finite K₁] [LinearOrder K₁]
         {K₂ : Type} [Finite K₂] [LinearOrder K₂]
         {Kₚ : Type} [Nonempty Kₚ]
         {Kₛ : Type} [Nonempty Kₛ]

def mergeR'' (πs : List (BalanceProof K₁ K₂ C Pi V)) (acc : BalanceProof K₁ K₂ C Pi V) : BalanceProof K₁ K₂ C Pi V :=
  match πs with
  | [] => acc
  | π :: πs => Dict.Merge acc (mergeR'' πs π)

section MergeLemmas

variable {acc π : BalanceProof K₁ K₂ C Pi V} {πs πs : List (BalanceProof K₁ K₂ C Pi V)}

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

end MergeLemmas

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

notation:51 π₁:52 " <≅> " π₂:52 => BalanceProof.compat π₁ π₂

notation:65 π₁:65 " <+> " π₂:66 => Dict.Merge π₁ π₂

section Compat

variable {π₁ π₂ π₃ : BalanceProof K₁ K₂ C Pi V}

end Compat

section MergeLemmas

variable {π acc : BalanceProof K₁ K₂ C Pi V}
         {πs : List (BalanceProof K₁ K₂ C Pi V)}

end MergeLemmas

variable [AD : ADScheme K₂ (C × K₁ × ExtraDataT) C Pi]

section MergeLemmas

variable {π acc : BalanceProof K₁ K₂ C Pi V}
         {πs : List (BalanceProof K₁ K₂ C Pi V)}

end MergeLemmas

variable [SA : SignatureAggregation (C × K₁ × ExtraDataT) K₂ KₛT Sigma]
         [Hinj : CryptoAssumptions.Injective (H (α := TransactionBatch K₁ K₂ V × ExtraDataT) (ω := (C × K₁ × ExtraDataT)))]
         {requests : List (Request K₁ K₂ C Sigma Pi V)}
         (isπ : isπ (normalise requests))

open Lean.Elab.Tactic Lean.Parser.Tactic in
</local_ctx>

<target_theorem>
theorem theorem1 : ¬adversaryWon (attackGame requests) :=
</target_theorem>

