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:
* <used_lib_defs>...</used_lib_defs>: Imported library definitions directly used by the theorem.
* <used_repo_defs>...</used_repo_defs>: Definitions from the local project (but outside the current file), directly or transitively used by the theorem.
* <lib_lemmas>...</lib_lemmas>: Imported library lemmas/theorems that may assist the proof.
* <repo_lemmas>...</repo_lemmas>: Lemmas/theorems defined in the local project outside this file.
* <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 used definitions and helpful lemmas (used_lib_defs, used_repo_defs, lib_lemmas, repo_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:
<used_lib_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)
</used_lib_defs>

<repo_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) :\n(l₁ ++ l₂)[i] = l₁[i]
</repo_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:
<used_lib_defs>
Preorder in Mathlib.Order.Defs.PartialOrder
Zero in Init.Prelude
Finite in Mathlib.Data.Finite.Defs
Option in Init.Prelude
List in Init.Prelude
Fin in Init.Prelude
IsLUB in Mathlib.Order.Bounds.Defs
List.length in Init.Prelude
List.take in Init.Data.List.Basic
Finset in Mathlib.Data.Finset.Defs
Lean.Parser.Tactic.replace in Init.Tactics
Nat in Init.Prelude
Prod in Init.Prelude
Set in Mathlib.Data.Set.Defs
absurd in Init.Prelude
List.foldl in Init.Prelude
IsLeast in Mathlib.Order.Bounds.Defs
LE in Init.Prelude
LE.le in Init.Prelude
lowerBounds in Mathlib.Order.Bounds.Defs
upperBounds in Mathlib.Order.Bounds.Defs
Vector in Init.Data.Vector.Basic
Preorder.toLE in Mathlib.Order.Defs.PartialOrder
List.concat in Init.Prelude
</used_lib_defs>

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

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

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

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) 

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

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

class abbrev PreWithZero (α : Type) := Preorder α, Zero α

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

abbrev ExtraDataT : Type := ℕ

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

def Merge (D₁ D₂ : Dict α ω) : Dict α ω := D
  where D := λ x ↦ First (D₁ x) (D₂ 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 BalanceProof.initial : BalanceProof K₁ K₂ C Pi V := λ _ ↦ .none

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

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

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

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

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

postfix:max "₊" => NonNeg
</used_repo_defs>

<lib_lemmas>
List.foldl_assoc in Init.Data.List.Lemmas
List.foldl_append in Init.Data.List.Lemmas
Set.mem_insert_iff in Mathlib.Data.Set.Insert
Set.mem_setOf_eq in Mathlib.Data.Set.Operations
Set.mem_singleton_iff in Mathlib.Data.Set.Insert
Set.mem_union in Mathlib.Data.Set.Basic
and_imp in Init.SimpLemmas
forall_eq in Init.PropLemmas
forall_eq_or_imp in Init.PropLemmas
List.concat_cons in Init.Data.List.Lemmas
Classical.not_forall in Init.Classical
Classical.not_imp in Init.Classical
Fin.getElem_fin in Init.GetElem
Fin.is_le' in Init.Data.Fin.Lemmas
Fin.lt_def in Init.Data.Fin.Lemmas
Fin.lt_of_le_of_lt in Init.Data.Fin.Lemmas
Fin.lt_of_lt_of_le in Init.Data.Fin.Lemmas
Finset.exists_minimal in Mathlib.Order.Preorder.Finite
Finset.filter_nonempty_iff in Mathlib.Data.Finset.Filter
Finset.mem_filter in Mathlib.Data.Finset.Filter
Finset.mem_univ in Mathlib.Data.Fintype.Defs
List.getElem_mem in Init.GetElem
List.getElem_of_mem in Init.Data.List.Lemmas
List.mem_take_iff_getElem in Init.Data.List.Nat.TakeDrop
List.take_add in Init.Data.List.Nat.TakeDrop
List.take_concat_get in Init.Data.List.TakeDrop
Nat.exists_eq_add_of_le in Init.Data.Nat.Lemmas
Option.ne_none_iff_exists in Init.Data.Option.Lemmas
Set.toFinset_setOf in Mathlib.Data.Fintype.Sets
and_true in Init.SimpLemmas
eq_or_lt_of_le in Mathlib.Order.Basic
gt_iff_lt in Init.Core
inf_of_le_left in Mathlib.Order.Lattice
lt_add_iff_pos_right in Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_irrefl in Mathlib.Order.Defs.PartialOrder
lt_trans in Mathlib.Order.Defs.PartialOrder
ne_eq in Init.SimpLemmas
not_and in Init.SimpLemmas
not_false_eq_true in Init.SimpLemmas
not_lt in Mathlib.Order.Defs.LinearOrder
true_and in Init.SimpLemmas
zero_lt_one in Mathlib.Algebra.Order.ZeroLEOne
</lib_lemmas>

<repo_lemmas>
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 proposition4 [Setoid' X] {x y : Option X} :
  (∃ join : Option X, IsLUB {x, y, .none} join) ↔ (x ≠ .none ∧ y ≠ .none → x ≅ y)

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

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

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

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

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₂ join : Dict X Y} (h : IsLUB {D₁, D₂} join) :
  join ≅ Dict.Merge D₁ D₂

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

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

@[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 Merge_assoc {D₃ : Dict α ω} :
  Merge (Merge D₁ D₂) D₃ = Merge D₁ (Merge D₂ D₃)

@[simp]
lemma none_iso_some : (.none ≅ some x) ↔ False
</repo_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)}
</local_ctx>

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

