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"):
User Prompt:
<used_lib_defs>
Array in Init.Prelude
</used_lib_defs>

<local_ctx>
import Mathlib

def fillArray (n : Nat) (v : Int) : Array Int :=
  let rec loop (i : Nat) (arr : Array Int) : Array Int :=
    if i < n then loop (i + 1) (arr.push v)
    else arr
  loop 0 #[]

@[reducible, simp]
def fillArray_postcond (n : Nat) (v : Int) (result : Array Int) : Prop :=
  result.size = n ∧ ∀ k < n, result[k]! = v
</local_ctx>

<target_theorem>
theorem fillArray_spec (n : Nat) (v : Int) :
    fillArray_postcond n v (fillArray n v) :=
</target_theorem>

Agent Response:
<reasoning>
IMPORTANT LEAN 4 SYNTAX NOTE: The postcondition uses `result[k]!` which works in 
a `def` statement. However, this syntax FAILS TO PARSE in universally quantified 
hypotheses inside theorem signatures. For example:

  -- THIS FAILS with "unexpected token '!'; expected ')'"
  theorem bad (arr : Array Int) (h : ∀ j, j < n → arr[j]! = v) : ... 

To work around this, I reformulate invariants using `arr.toList` instead:

  -- THIS WORKS
  theorem good (arr : Array Int) (h : arr.toList = List.replicate n v) : ...

Then in the final proof, I connect `toList` back to `[k]!` using:
  - Array.getElem!_eq_getElem?_getD
  - Array.getElem?_eq_toList_getElem?

This is the standard pattern when postconditions use `[i]!` but you need helper lemmas.
</reasoning>

<lean4_invented_lemmas>
-- NOTE: Invariant uses toList instead of [i]! to avoid parse errors
theorem fillArray_loop_inv (n : Nat) (v : Int) (i : Nat) (arr : Array Int)
    (hsize : arr.size = i) 
    (hvals : arr.toList = List.replicate i v)  -- NOT: ∀ j < i, arr[j]! = v
    (hi : i ≤ n) :
    let result := fillArray.loop n v i arr
    result.size = n ∧ result.toList = List.replicate n v := by
  induction i, arr using fillArray.loop.induct n v with
  | case1 i arr hi' ih =>
    simp only [fillArray.loop, hi', ↓reduceIte]
    apply ih
    · simp [Array.size_push, hsize]
    · simp [Array.toList_push, hvals, List.replicate_succ']
    · omega
  | case2 i arr hi' =>
    simp only [fillArray.loop, hi', ↓reduceIte]
    have : i = n := by omega
    subst this
    exact ⟨hsize, hvals⟩
</lean4_invented_lemmas>

<lean4_proof>
by
  unfold fillArray_postcond fillArray
  obtain ⟨hsize, hlist⟩ := fillArray_loop_inv n v 0 #[] (by simp) (by simp) (by omega)
  refine ⟨hsize, ?_⟩
  intro k hk
  -- Connect toList back to [k]!
  simp only [Array.getElem!_eq_getElem?_getD, Array.getElem?_eq_toList_getElem?]
  rw [hlist]
  simp [List.getElem?_replicate, hk]
</lean4_proof>

### Your task:
<used_lib_defs>
Nat.succ in Init.Prelude
Nat.succPNat in Mathlib.Data.PNat.Defs
Nat.pred in Init.Prelude
Nat.add in Init.Prelude
Nat.sub in Init.Prelude
Nat.subDigitChar in Init.Data.Repr
Nat.mul in Init.Prelude
Nat.multichoose in Mathlib.Data.Nat.Choose.Basic
Nat.div in Init.Prelude
Nat.div.go in Init.Prelude
Nat.mod in Init.Prelude
Nat.mod.inductionOn in Init.Data.Nat.Div.Basic
Nat.min in Init.Data.Nat.Basic
Nat.minFac in Mathlib.Data.Nat.Prime.Defs
Nat.max in Init.Data.Nat.Basic
Nat.maxPowDiv in Mathlib.Data.Nat.MaxPowDiv
Nat.pow in Init.Prelude
Nat.lt in Init.Prelude
Nat.lt_iff_le_and_not_ge in Init.Data.Nat.Basic
Nat.le in Init.Prelude
Int.add in Init.Data.Int.Basic
Int.add_of_le in Init.Data.Int.Cooper
Int.sub in Init.Data.Int.Basic
Int.subNatNat in Init.Data.Int.Basic
Int.mul in Init.Data.Int.Basic
Int.multichoose in Mathlib.RingTheory.Binomial
Int.div2 in Mathlib.Data.Int.Bitwise
Int.divExact in Init.Data.Int.DivMod.Basic
Int.neg in Init.Data.Int.Basic
Int.negInduction in Mathlib.Data.Int.Init
Int.toNat in Init.Data.Int.Basic
Int.toNat? in Init.Data.Int.Basic
Int.ofNat in Init.Data.Int.Basic
Int.ofNatHom in Mathlib.Data.Int.Cast.Lemmas
Int.natAbs in Init.Data.Int.Basic
Int.natAbsHom in Mathlib.Data.Int.NatAbs
Array.size in Init.Prelude
Array.get!Internal in Init.Prelude
Array.get!InternalBorrowed in Init.Prelude
Array.set in Init.Data.Array.Set
Array.set! in Init.Data.Array.Set
Array.push in Init.Prelude
Array.pop in Init.Data.Array.Basic
Array.popWhile in Init.Data.Array.Basic
Array.toList in Init.Prelude
Array.toListAppend in Init.Data.Array.Basic
Array.empty in Init.Prelude
Array.emptyWithCapacity in Init.Prelude
Array.mkEmpty in Init.Prelude
Array.foldl in Init.Data.Array.Basic
Array.foldlM in Init.Data.Array.Basic
Array.map in Init.Data.Array.Basic
Array.mapFinIdx in Init.Data.Array.Basic
Array.filter in Init.Data.Array.Basic
Array.filterM in Init.Data.Array.Basic
Array.back in Init.Data.Array.Basic
</used_lib_defs>

<lib_lemmas>
Nat.add_comm in Init.Data.Nat.Basic
Nat.add_assoc in Init.Data.Nat.Basic
Nat.add_zero in Init.Core
Nat.zero_add in Init.Data.Nat.Basic
Nat.sub_self in Init.Data.Nat.Basic
Nat.sub_self_add in Init.Data.Nat.Basic
Nat.sub_zero in Init.Data.Nat.Basic
Nat.mul_comm in Init.Data.Nat.Basic
Nat.div_self in Init.Data.Nat.Div.Basic
Nat.mod_self in Init.Data.Nat.Div.Basic
Nat.lt_succ in Init.Data.Nat.Basic
Nat.lt_succ_floor in Mathlib.Algebra.Order.Floor.Semiring
Nat.lt_succ_iff in Init.Data.Nat.Basic
Nat.succ_lt_of_lt_pred in Init.Data.Nat.Basic
Nat.succ_lt_succ in Init.Data.Nat.Basic
Nat.le_succ in Init.Prelude
Nat.le_succ_iff in Init.Data.Nat.Lemmas
Nat.lt_of_lt_floor in Mathlib.Algebra.Order.Floor.Semiring
Nat.lt_of_lt_of_eq in Init.Data.Nat.Basic
Nat.lt_of_le_of_lt in Init.Prelude
Nat.lt_of_le_of_ne in Init.Prelude
Nat.le_of_lt in Init.Data.Nat.Basic
Nat.le_of_lt_add_of_dvd in Init.Data.Nat.Lemmas
Nat.le_trans in Init.Prelude
Nat.lt_trans in Init.Prelude
Nat.not_lt in Init.Data.Nat.Basic
Nat.not_lt_eq in Init.Data.Nat.Basic
Nat.lt_irrefl in Init.Prelude
Nat.le_refl in Init.Prelude
Int.add_comm in Init.Data.Int.Lemmas
Int.add_assoc in Init.Data.Int.Lemmas
Int.sub_self in Init.Data.Int.Lemmas
Int.neg_neg in Init.Data.Int.Lemmas
Int.neg_negSucc in Init.Data.Int.Lemmas
Int.toNat_of_nonneg in Init.Data.Int.Order
Int.toNat_of_nonpos in Init.Data.Int.Lemmas
Int.ofNat_lt in Init.Data.Int.Order
Int.ofNat_lt_ofNat_of_lt in Mathlib.Data.Int.Order.Basic
Int.ofNat_le in Init.Data.Int.Order
Int.ofNat_le_ofNat_of_le in Mathlib.Data.Int.Order.Basic
Int.lt_of_add_lt_add_left in Init.Data.Int.Order
Int.lt_of_add_lt_add_right in Init.Data.Int.Order
Int.le_of_add_le_add_left in Init.Data.Int.Order
Int.le_of_add_le_add_right in Init.Data.Int.Order
Array.size_set in Init.Data.Array.Basic
Array.size_set! in Batteries.Data.Array.Lemmas
Array.size_setIfInBounds in Init.Data.Array.Lemmas
Array.size_push in Init.Data.Array.Basic
Array.size_pop in Init.Data.Array.Basic
Array.size_append in Init.Data.Array.Lemmas
Array.size_empty in Init.Data.Array.Lemmas
Array.getElem_set in Init.Data.Array.Lemmas
Array.getElem_setIfInBounds in Init.Data.Array.Lemmas
Array.getElem_setIfInBounds_ne in Init.Data.Array.Lemmas
Array.getElem_push in Init.Data.Array.Lemmas
Array.getElem_push_eq in Init.Data.Array.Lemmas
Array.getElem_push_lt in Init.Data.Array.Lemmas
Array.toList_eq_nil_iff in Init.Data.Array.Lemmas
Array.length_toList in Init.Data.Array.Lemmas
Array.mem_iff_append in Init.Data.Array.Lemmas
Array.mem_iff_getElem in Init.Data.Array.Lemmas
decide_eq_true in Init.Prelude
decide_eq_false in Init.Prelude
of_decide_eq_true in Init.Prelude
of_decide_eq_false in Init.Prelude
eq_comm in Init.Core
ne_comm in Init.Core
Iff.intro in Init.Core
Iff.mp in Init.Core
Iff.mpr in Init.Core
And.intro in Init.Prelude
And.left in Init.Prelude
And.right in Init.Prelude
Or.inl in Init.Prelude
Or.inr in Init.Prelude
Classical.em in Init.Classical
</lib_lemmas>

<local_ctx>
import Mathlib

@[reducible, simp]
def concat_precond (a : Array Int) (b : Array Int) : Prop :=
  True

def concat (a : Array Int) (b : Array Int) (h_precond : concat_precond (a) (b)) : Array Int :=
  let n := a.size + b.size
  let rec loop (i : Nat) (c : Array Int) : Array Int :=
    if i < n then
      let value := if i < a.size then a[i]! else b[i - a.size]!
      loop (i + 1) (c.set! i value)
    else
      c
  loop 0 (Array.mkArray n 0)

@[reducible, simp]
-- Note: Use a[i]'(by omega) instead of a[i]! in theorem signatures
def concat_postcond (a : Array Int) (b : Array Int) (result: Array Int) (h_precond : concat_precond (a) (b)) :=
  result.size = a.size + b.size
    ∧ (∀ k, k < a.size → result[k]! = a[k]!)
    ∧ (∀ k, k < b.size → result[k + a.size]! = b[k]!)
</local_ctx>

<target_theorem>
theorem concat_spec_satisfied (a: Array Int) (b: Array Int) (h_precond : concat_precond (a) (b)) :
    concat_postcond (a) (b) (concat (a) (b) h_precond) h_precond
</target_theorem>