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>
abbrev Dict (α ω : Type) : Type := α → Option ω

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)

def isRandom (f : Seed → α) (x : α) := ∃ seed, x = f seed

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

Sum.inl in Init.Core

List.attach in Init.Data.List.Attach

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

def lookup_h [DecidableEq α] {a : α}
  (s : Finmap β) (h : a ∈ s) : β a := s.lookup a |>.get (Option.isSome_iff_exists.2 (Finmap.mem_iff.1 h))

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

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

List.NodupKeys in Mathlib.Data.List.Sigma

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

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

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

Decidable in Init.Prelude

Option.isSome in Init.Data.Option.Basic

List.concat in Init.Prelude

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

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

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

Int in Init.Data.Int.Basic

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

Lean.Parser.Tactic.replace in Init.Tactics

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

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

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

def Seed : Type := ℕ

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

IsAntisymm in Mathlib.Order.Defs.Unbundled

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

Set.image in Mathlib.Data.Set.Defs

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

Finset in Mathlib.Data.Finset.Defs

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

instance latticePreorder : Preorder V := inferInstance

Option in Init.Prelude

Nonempty in Init.Prelude

Subtype in Init.Prelude

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 keysUneq (k₂ : K₂) (k : Key K₁ K₂) : Prop :=
  match k with
  | .inl _   => True
  | .inr k₂' => k₂ ≠ k₂'

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

List.zipWith in Init.Data.List.Basic

Classical.arbitrary in Mathlib.Logic.Nonempty

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

Multiset.keys in Mathlib.Data.Finmap

Membership in Init.Prelude

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

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

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

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

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

Multiset.Nodup in Mathlib.Data.Multiset.Defs

List.foldl in Init.Prelude

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

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

abbrev ExtraDataT : Type := ℕ

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 codomainPred {α : Type} [DecidableEq α] {β : Type}
  (m : Finmap (λ _ : α ↦ β)) (P : β → Prop) : Prop :=
  ∀ key : α, (h : key ∈ m) → P (m.lookup_h h)

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

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

lowerBounds in Mathlib.Order.Bounds.Defs

Monotone in Mathlib.Order.Monotone.Defs

instance : Preorder (Option V₊) := inferInstance

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

Iff in Init.Core

Finset.univ in Mathlib.Data.Fintype.Defs

List.finRange in Init.Data.List.FinRange

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

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

Multiset in Mathlib.Data.Multiset.Defs

Finite in Mathlib.Data.Finite.Defs

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

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

LE.le in Init.Prelude

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

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

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

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

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

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 }

PartialOrder in Mathlib.Order.Defs.PartialOrder

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

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

Set.range in Mathlib.Data.Set.Operations

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

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

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

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 iso {X : Type} [Preorder X] (a b : X) := a ≤ b ∧ b ≤ a

absurd in Init.Prelude

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

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

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

flip in Init.Core

List.length in Init.Prelude

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

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

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

Function.Injective in Init.Data.Function

noncomputable def univFinmap (K : Type) [Fintype K] [DecidableEq K]
                             (V : Type) [DecidableEq V] :
  { m : Finmap (λ _ : K ↦ V) // ∀ k, k ∈ m } ≃ (K → V) :=
  {
    toFun := λ m k ↦ m.1.lookup_h (a := k) (m.2 k)
    invFun := λ f ↦
      let keys : Finset K := Finset.univ
      ⟨⟨
        Multiset.ofList <| keys.toList.zipWith (f := Sigma.mk) (keys.toList.map f),
        by admit /- proof elided -/
       ⟩,
        by admit /- proof elided -/
           ⟩
    left_inv := by admit /- proof elided -/

instance : PreWithZero α₊ :=

Function.eval in Mathlib.Logic.Function.Basic

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

Set in Mathlib.Data.Set.Defs

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

instance [Finite α] : Finite α₊ :=

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

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

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

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 IsEquivRel {X : Type} [Preorder X] := ∀ a b : X, a ≤ b ↔ a ≅ b

Finset.range in Mathlib.Data.Finset.Range

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

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

Multiset.map in Mathlib.Data.Multiset.MapFold

Finmap in Mathlib.Data.Finmap

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

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

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

DecidableEq in Init.Prelude

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

Subtype.val in Init.Prelude

Multiset.ofList in Mathlib.Data.Multiset.Defs

And in Init.Prelude

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

CoeFun in Init.Coe

Preorder.toLE in Mathlib.Order.Defs.PartialOrder

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

Lattice in Mathlib.Order.Lattice

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

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)

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

Prod.fst in Init.Prelude

Vector in Init.Data.Vector.Basic

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

Option.isNone in Init.Data.Option.Basic

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

IsGLB in Mathlib.Order.Bounds.Defs

Finset.sort in Mathlib.Data.Finset.Sort

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

IsLUB in Mathlib.Order.Bounds.Defs

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

upperBounds in Mathlib.Order.Bounds.Defs

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

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

IsLeast in Mathlib.Order.Bounds.Defs

IsBot in Mathlib.Order.Max

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

List.flatten in Init.Prelude

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

abbrev KₚT : Type := ℕ

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

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

instance : Preorder (Τ K₁ K₂ V × S 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 : Preorder (Pi × ExtraDataT) := trivialPreorder

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

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

IsTotal in Mathlib.Order.Defs.Unbundled

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

Coe in Init.Coe

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

instance : LT (Key K₁ K₂) := ⟨Key.lt⟩

Nat in Init.Prelude

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

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

LinearOrder in Mathlib.Order.Defs.LinearOrder

Multiset.dedup in Mathlib.Data.Multiset.Dedup

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

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

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

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 e (i : Kbar K₁ K₂) : Kbar K₁ K₂ → ℤ := λ j ↦ if i = j then 1 else 0

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₂ × Option V₊) := inferInstance

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

LT in Init.Prelude

Nat.card in Mathlib.SetTheory.Cardinal.Finite

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

Finset.toList in Mathlib.Data.Finset.Dedup

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

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

List.lookup in Init.Data.List.Basic

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

List.take in Init.Data.List.Basic

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

def Kbar.getK₁ (k : Kbar K₁ K₂) (_h : k.isK₁) : K₁ :=
  match h : k with
  | .key (.inl k₁) => k₁
  | .key (.inr _) | .Source => by admit /- proof elided -/

LE 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 [Finite K₁] [Finite K₂] : Preorder ((Pi × ExtraDataT) × TransactionBatch K₁ K₂ V) := inferInstance

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

iInf in Mathlib.Order.SetNotation

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

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

List.Ico in Mathlib.Data.List.Intervals

List in Init.Prelude

List.map in Init.Prelude

Prod in Init.Prelude

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

Std.Associative in Init.Core

Prod.snd in Init.Prelude

Sigma.mk in Init.Core
</all_available_defs>

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

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

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

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

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

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

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 monotone_TransactionsInBlocksFixed :
  Monotone λ (π : BalanceProof K₁ K₂ C Pi V) ↦ TransactionsInBlocksFixed π Bstar

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

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

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

theorem theorem1 : ¬adversaryWon (attackGame requests)

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

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

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

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

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

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 attackGame_eq_attackGameBlocks!_normalise :
  attackGame requests = attackGameBlocks! (normalise requests)

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

lemma le_of_iso' (h : π₁ ≅ π₂) (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)

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

@[simp]
lemma v'_source_eq_v : v' v b .Source = 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 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 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 attackGameRGo_cons :
  attackGameRGo (request :: requests) σ =
  request.toBlock! σ :: attackGameRGo requests (σ.appendBlock! request)

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

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

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

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

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

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

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

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

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

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

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

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

Option.isSome_iff_ne_none in Init.Data.Option.Lemmas

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

private lemma merge_lem_aux :
  mergeR'' (π :: πs) acc = acc <+> π <+> (mergeR'' πs BalanceProof.initial)

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

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

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

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

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

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

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

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

lemma isSome_of_complete {t'} (h : isComplete ⟨⟨kb₁, kb₂, v?⟩, t'⟩) : v?.isSome

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

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

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)

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

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 f_transfer_source
  (h : ∃ block : {b : Block K₁ K₂ C Sigma V // b.isTransferBlock},
         T ∈ TransactionsInBlock π block.1) :
  (f σ T) .Source = σ .Source

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

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

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

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

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

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)

@[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 le_of_ext_le {α : Type} [Preorder α] {v₁ v₂ : Vector α n}
  (h : ∀ i : Fin n, v₁.1[i] ≤ v₂.1[i]) : v₁ ≤ v₂

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

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

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

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

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)

omit Hinj in
private theorem not_adversaryWon_attackGame_of_exists_LUB
  (eqrequests : requests! = normalise requests)
  (hValid     : ∀ request ∈ requests!, request.isValid)
  (eqI        : I = (List.finRange (attackGameR requests! []).length).filter ((attackGameR requests! [])[·].isWithdrawalBlock))
  (hI         : ∀ {i : Fin (attackGameR requests! []).length}, i ∈ I ↔ (attackGameR requests! [])[i].isWithdrawalBlock)
  (hgetπ      : getπ =
                λ i : {i : Fin (attackGameR requests! []).length // i ∈ I} ↦
                  (i, getBalanceProof requests! hValid ⟨i.1.1, i.1.2⟩ (hI.1 i.2)))
  (eqπs       : πs = I.attach.map getπ)
  (hlen       : πs.length ≤ n)
  (hπs        : ∀ (i : {i // i ∈ I}), (List.lookup i πs).isSome)
  (eqπproofs  : πproofs = πs.map Prod.snd)
  (πproofslen : πproofs.length = πs.length)
  (isπ        : ∀ (i : Fin (List.length (attackGameR requests! [])))
                  (h : (attackGameR requests! [])[i.1].isWithdrawalBlock),
                  (attackGameR requests! [])[i.1].getWithdrawal h =
                  (getBalanceProof requests! hValid i h).toBalanceF ((attackGameR requests! []).take i.1))
  (contra     : ¬0 ≤ computeBalanceSum (attackGameR requests! []))
  (existsLUB  : ∃ join, IsLUB {π | π ∈ πproofs} join) : False

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

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

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

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

@[simp]
lemma isLUB_some_none_iff_False :
  IsLUB {none} (.some x) ↔ False

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

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

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

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

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

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

private lemma le_cons_aux 
  (eq₁ : v₁ = ⟨hd₁ :: tl₁, len₁⟩) (eq₂ : v₂ = ⟨hd₂ :: tl₂, len₂⟩)
  (h : v₁ ≤ v₂) : hd₁ ≤ hd₂ ∧
  le ⟨tl₁, by simp at len₁; assumption⟩ ⟨tl₂, by simp at len₂; assumption⟩

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

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

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

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

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

lemma toBlock_σ_matches_withdrawal (σ σ' : Scontract K₁ K₂ V C Sigma) :
  request.toBlock! σ matches .withdrawal .. ↔
  request.toBlock! σ' matches .withdrawal ..

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

lemma lemma3 : Bal π bs .Source ≤ 0

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

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

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

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

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

@[simp]
lemma mergeR''_concat {π} {πs : List (BalanceProof K₁ K₂ C Pi V)} {acc} :
  mergeR'' (πs.concat π) acc = ((mergeR'' πs acc) <+> π)

@[aesop safe apply]
lemma nonneg_key_of_isValid {b : S' K₁ K₂ V} {k} (h : b.isValid) : 0 ≤ b (.key k)

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

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

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

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 iso_K_merge_right_of_ne_none_compat (h : π K ≠ none) (h : π <≅> acc) :
  π K ≅ (acc <+> π) K

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₁

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

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

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

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

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

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 computeBalance'_nil : computeBalance' ([] : Scontract K₁ K₂ V C Sigma) v = v

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

@[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 isValid_coe {s : S K₁ K₂ V} : S'.isValid (V := V) (K₁ := K₁) (K₂ := K₂) ↑s

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

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

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

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

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

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

@[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 finRange_eq_Ico : List.finRange n = (List.Ico 0 n).attach.map λ ⟨i, hi⟩ ↦ ⟨i, by aesop⟩

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

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

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

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

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

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 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 nonneg_coe {s : S K₁ K₂ V} {k : Key K₁ K₂} : 0 ≤ (↑s : S' K₁ K₂ V) 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 getElem_Ico_of_lt {m n : ℕ} (h : n < m) : (List.Ico 0 m)[n]'(by simp [h]) = n

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

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

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

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

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

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 discretePreorder_eq_equality_Key_Map_Vplus {a b : Key K₁ K₂ → V₊} : a ≤ b ↔ a = b

lemma toBlock_eq_toBlock!_of_isValid (h : request.isValid) :
  (toBlock σ request) = toBlock! σ request

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

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

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

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

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

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 fStar_cons {hd : Τ K₁ K₂ V} {tl : List (Τ K₁ K₂ V)} :
  fStar (hd :: tl) s = fStar tl (f s hd)

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

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

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

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 Merge_mergeR''_comm {πs : List (BalanceProof K₁ K₂ C Pi V)} (h : π <≅> acc) :
  acc <+> (mergeR'' πs π) ≅ π <+> (mergeR'' πs acc)

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)

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 keys_dedup_map_pres_univ
  (h : m.Nodup) [DecidableEq (Sigma β)] (h₁ : ∀ x, Sigma.fst (f x) = x) :
  (Multiset.map f m).dedup.keys = m

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

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

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

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

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

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

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 iso_of_isLUB [Setoid' X] {x y join : X} (h : IsLUB {x, y} join) : x ≅ y

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

lemma Merge_split (h₀ : 0 < i) (h₁ : i ≤ πs.length) :
  mergeR'' (πs.take i) acc =
  mergeR'' (πs.take (i - 1)) acc <+> πs[i - 1]

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 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_withdrawal {B : K₁ → V₊} :
  (Block.withdrawal B).updateBalance (K₁ := K₁) (K₂ := K₂) (C := C) (Sigma := Sigma) v = v - ∑ (k : K₁), (B k).1

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

@[simp]
lemma v'_self {h} : v' ⟨(b s), h⟩ b s = ⟨b s, 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 first_left (h : x₁.isSome) : First x₁ x₂ = x₁

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

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

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

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

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

<local_ctx>
import Mathlib.Order.Bounds.Basic

import Mathlib.Order.Bounds.Defs

import Mathlib.Order.Defs

import Aesop

import FVIntmax.Wheels.Dictionary

namespace Intmax

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

notation:51 (priority := high) a:52 " ≅ " b:52 => iso a b

section iso

variable {X : Type} [Preorder X]
         {a b c : X}

end iso

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)

section Automation

variable {α : Type} [Preorder α]
         {x y : α}

end Automation

section Propositions

variable {X Y : Type}

section proposition3

variable [Preorder X]
         {x? y? join? join'? : Option X}
         {x y join join' : X}

end proposition3

section Automation

variable {X : Type} [Setoid' X]
         {x y : X}
         {x? y? : Option X}

end Automation
</local_ctx>

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

