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>
Fin in Init.Prelude
Float in Init.Data.Float
Matrix in Mathlib.LinearAlgebra.Matrix.Defs
DecidableEq in Init.Prelude
Invertible in Mathlib.Algebra.Group.Invertible.Defs
Matrix.invertibleOfIsUnitDet in Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Fin.elim0 in Init.Data.Fin.Basic
Float.ofNat in Init.Data.OfScientific
List in Init.Prelude
List.finRange in Init.Data.List.FinRange
LinearOrder in Mathlib.Order.Defs.LinearOrder
Zero in Init.Prelude
Matrix.diagonal in Mathlib.Data.Matrix.Diagonal
Matrix.fromBlocks in Mathlib.Data.Matrix.Block
Matrix.PosSemidef in Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.det in Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Sum in Init.Core
Sum.elim in Init.Data.Sum.Basic
Sum.inr in Init.Core
Nonempty in Init.Prelude
Finset in Mathlib.Data.Finset.Defs
Sum.inl in Init.Core
Matrix.IsHermitian in Mathlib.LinearAlgebra.Matrix.Hermitian
A in examples.CircleOptimisation
Matrix.PosSemidef.sqrt in Mathlib.Analysis.Matrix.Order
RCLike in Mathlib.Analysis.RCLike.Basic
RCLike.ofReal in Mathlib.Analysis.RCLike.Basic
Fintype in Mathlib.Data.Fintype.Defs
Matrix.vecMul in Mathlib.Data.Matrix.Mul
IsUnit in Mathlib.Algebra.Group.Units.Defs
Matrix.mulVec in Mathlib.Data.Matrix.Mul
Matrix.toLin' in Mathlib.LinearAlgebra.Matrix.ToLin
Module in Mathlib.Algebra.Module.Defs
Module.End in Mathlib.Algebra.Module.LinearMap.End
Module.End.HasEigenvector in Mathlib.LinearAlgebra.Eigenspace.Basic
LT in Init.Prelude
Matrix.BlockTriangular in Mathlib.LinearAlgebra.Matrix.Block
id in Init.Prelude
</used_lib_defs>

<used_repo_defs>
def toUpperTri (A : Matrix (Fin n) (Fin n) Float) : Matrix (Fin n) (Fin n) Float :=
  fun i j => if i ≤ j then A i j else 0

noncomputable instance PosDef.Invertible [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) :
    Invertible M :=
  invertibleOfIsUnitDet M (isUnit_iff_ne_zero.2 hM.det_ne_zero)

def diag {n} {α} (M : Matrix n n α) : n → α :=
  fun i => M i i

def det {n : ℕ} (A : Matrix (Fin n) (Fin n) Float) : Float :=
  if h : 0 < n then
    if n == 1 then A ⟨0, h⟩ ⟨0, h⟩ else
      (List.finRange n).foldl (fun s i =>
        s + (-1) ^ (Float.ofNat i.val) * A i ⟨0, h⟩ * det (minor A i ⟨0, h⟩)) 0
  else 0

def minor (A : Matrix (Fin n) (Fin n) Float) (a b : Fin n) :
    Matrix (Fin n.pred) (Fin n.pred) Float :=
  match n with
  | 0 => fun _ => Fin.elim0
  | _ + 1 => minorAux A a b

private def minorAux (A : Matrix (Fin n.succ) (Fin n.succ) Float) (a b : Fin n.succ) :
    Matrix (Fin n) (Fin n) Float :=
  fun i j =>
    let i' : Fin n.succ := if i.val < a.val then i else i.succ;
    let j' : Fin n.succ := if j.val < b.val then j else j.succ;
    A i' j'

def toUpperTri {m α : Type _} [LinearOrder m] [Zero α] (A : Matrix m m α) :
    Matrix m m α :=
  fun i j => if i ≤ j then A i j else 0

noncomputable def IsHermitian.sqrt {A : Matrix n n ℝ} (hA : A.IsHermitian) : Matrix n n ℝ :=
  hA.eigenvectorMatrix * Matrix.diagonal (fun i => (hA.eigenvalues i).sqrt) * hA.eigenvectorMatrixᵀ

structure SymmMatrixVariable where
  index  : Nat
  name   : String
  I      : Nat
  J      : Nat
  primal : Option Float
  dual   : Option Float

instance : ToString SymmMatrixVariable where
  toString smv :=
    s!"{smv.index} | " ++
    s!"{smv.name} | " ++
    s!"{smv.I} | " ++
    s!"{smv.J} | " ++
    s!"{smv.primal} | " ++
    s!"{smv.dual}"

structure Result where
  summary        : Summary
  constraints    : List Constraint
  vars           : List Variable
  symmMatrixVars : List SymmMatrixVariable

instance : ToString Result where
  toString res :=
    (toString res.summary) ++ "\n" ++
    "CONSTRAINTS \n" ++
    "INDEX | NAME | AT | ACTIVITY | LOWER LIMIT | UPPER LIMIT | DUAL LOWER | DUAL UPPER \n" ++
    (res.constraints.foldl (fun acc s => acc ++ (toString s) ++ "\n") "") ++ "\n" ++
    "VARIABLES \n" ++
    "INDEX | NAME | AT | ACTIVITY | LOWER LIMIT | UPPER LIMIT | DUAL LOWER | DUAL UPPER | " ++
    "CONIC DUAL \n" ++
    (res.vars.foldl (fun acc s => acc ++ (toString s) ++ "\n") "") ++ "\n" ++
    "SYMMETRIC MATRIX VARIABLES \n" ++
    "INDEX | NAME | I | J | PRIMAL | DUAL \n" ++
    (res.symmMatrixVars.foldl (fun acc s => acc ++ (toString s) ++ "\n") "") ++ "\n"

private def symmMatrixVarsTitle : Parsec Unit :=
  skipString "SYMMETRIC MATRIX VARIABLES" <* endOfLine

private def symmMatrixVarsHeaders : Parsec Unit :=
  skipString "INDEX"  <* ws' <*
  skipString "NAME"   <* ws' <*
  skipString "I"      <* ws' <*
  skipString "J"      <* ws' <*
  skipString "PRIMAL" <* ws' <*
  skipString "DUAL"   <* ws' <* endOfLine

private def symmMatrixVar : Parsec SymmMatrixVariable :=
  SymmMatrixVariable.mk <$>
  constraintElem nat         <*>
  constraintElem string      <*>
  constraintElem nat         <*>
  constraintElem nat         <*>
  constraintElem optionFloat <*>
  constraintElem optionFloat <* ws' <* endOfLine

private def symmMatrixVars : Parsec (List SymmMatrixVariable) :=
  (symmMatrixVarsTitle  *>
  symmMatrixVarsHeaders *>
  Array.data <$> many symmMatrixVar) <|> pure []

def result : Parsec Result :=
  Result.mk <$>
  summary        <* ws <*>
  constraints    <* ws <*>
  vars           <* ws <*>
  symmMatrixVars <* ws

unsafe def inferDimension (ty : Expr) : MetaM (List (Nat × Nat)) :=
  match ty.consumeMData with
  | .const ``Real _ =>
      return [(1, 1)]
  | .forallE _ (.app (.const ``Fin _) nExpr) e _ =>
    match e with
    | .const ``Real _  => do
      let n : Nat ← evalExpr Nat (mkConst ``Nat) nExpr
      return [(n, 1)]
    | .forallE _ (.app (.const ``Fin _) mExpr) (.const ``Real _) _ => do
      let n : Nat ← evalExpr Nat (mkConst ``Nat) nExpr
      let m : Nat ← evalExpr Nat (mkConst ``Nat) mExpr
      return [(n, m)]
    | _ => throwSolveError "could not infer dimension of {ty}."
  | .app (.app (.app M FinN) FinM) R => do
    match (M, FinN, FinM, R) with
    | (.const ``Matrix _, .app (.const ``Fin _) nExpr, .app (.const ``Fin _) mExpr,
        .const ``Real _) =>
      let n : Nat ← evalExpr Nat (mkConst ``Nat) nExpr
      let m : Nat ← evalExpr Nat (mkConst ``Nat) mExpr
      return [(n, m)]
    | _ => throwSolveError "could not infer dimension of {ty}."
  | .app (.app (.const ``Prod _) tyl) tyr => do
    let l ← inferDimension tyl
    let r ← inferDimension tyr
    return (l ++ r)
  | _ => throwSolveError "could not infer dimension of {ty}."

unsafe def ofProblemData (minExpr : MinimizationExpr) (data : ProblemData)
    (sections : ScalarAffineSections) : MetaM CBF.Problem := do
  let totalDim ← getTotalDim minExpr

  let mut cbf := CBF.Problem.empty
  cbf := cbf.addScalarVariable (CBF.Cone.mk CBF.ConeType.F totalDim)

  if h : data.objective.isSome then
    let sa := data.objective.get h
    let AEnc := CBF.EncodedMatrixList.fromArray #[sa.A]
    let aEnc := CBF.EncodedVector.fromArray sa.a
    let bEnc := CBF.EncodedValue.mk (some sa.b)
    cbf := cbf.setObjectivePSDVariablesCoord AEnc
    cbf := cbf.setObjectiveScalarVariablesCoord aEnc
    cbf := cbf.setObjectiveShiftCoord bEnc

  for (sa, sct) in data.scalarAffineConstraints do
    let coneType := translateCone sct
    let cone := CBF.Cone.mk coneType 1
    let AEnc := CBF.EncodedMatrixList.fromArray #[sa.A]
    let aEnc := CBF.EncodedVector.fromArray sa.a
    let bEnc := sa.b
    cbf := cbf.addScalarValuedAffineConstraint cone AEnc aEnc bEnc

  for ma in data.matrixAffineConstraints do
    let HEnc := CBF.EncodedMatrixList.fromArray ma.H
    let DEnc := CBF.EncodedMatrix.fromArray ma.D
    cbf := cbf.addMatrixValuedAffineConstraint ma.n HEnc DEnc

  
  let n := cbf.scalarConstraints.n
  let cones := cbf.scalarConstraints.cones
  let groupedCones ← groupCones sections cones
  cbf := cbf.setScalarConstraints (CBF.ConeProduct.mk n groupedCones.length groupedCones)

  return cbf

structure SimpleMatrixVarSol where
  name  : String
  I     : Nat
  J     : Nat
  value : Option Float

instance : ToString SimpleMatrixVarSol where
  toString v :=
    match v.value with
    | some x => v.name ++ "[" ++ toString v.I ++ ", " ++ toString v.J ++ "]* = " ++ toString x
    | none   => "none"

structure SolutionData where
  status         : String
  varsSols       : List SimpleVarSol
  matrixVarsSols : List SimpleMatrixVarSol

instance : ToString SolutionData where
  toString s :=
    "Status: " ++ s.status ++ "\n" ++
    "Variables: (" ++ ", ".intercalate (s.varsSols.map toString) ++ ")\n" ++
    "Matrix variables: (" ++ ", ".intercalate (s.matrixVarsSols.map toString) ++ ")"

def p :=
  optimization (x y : ℝ)
    minimize -2 * x
    subject to
      c₁ : 0 ≤ x
      c₂ : 1 < y
      c₃ : log (y - 1) ≤ 2 * sqrt x + 1
      c₄ : 3 * x + 5 * y ≤ 10

-- Transform (proving `p ≡ q`).

equivalence* eqv/q : p :=

def const (k : α) : Matrix m n α :=
  fun _ _ => k

instance [Preorder α] : Preorder (Matrix m n α) where
  le := fun A B => ∀ i j, A i j ≤ B i j
  le_refl := fun _ _ _ => le_refl _
  le_trans := fun _ _ _ hAB hBC i j => le_trans (hAB i j) (hBC i j)
  lt_iff_le_not_le := fun _ _ => refl _

def abs (A : Matrix m n ℝ) : Matrix m n ℝ :=
  fun i j => |A i j|

def sum [Fintype m] [AddCommMonoid α] (X : Matrix m m α) : α :=
  ∑ i, (∑ j, X i j)

def toArray (A : Matrix (Fin n) (Fin n) Float) : Array (Array Float) :=
  (Array.range n).map <| fun i =>
    if h : i < n then Vec.Computable.toArray (A ⟨i, h⟩) else Array.mk <| List.replicate n 0

def dotProduct (v w : Fin n → Float) : Float :=
  (Array.zipWith (Vec.Computable.toArray v) (Vec.Computable.toArray w) Float.mul).foldl Float.add 0

def mulVec (M : Matrix (Fin n) (Fin m) Float) (v : (Fin m) → Float) : Fin n → Float :=
  fun i => (fun j => M i j) ⬝ᵥᶜ v

def vecMul (x : Fin n → Float) (M : Matrix (Fin n) (Fin m) Float) : Fin m → Float :=
  fun j => x ⬝ᵥᶜ fun i => M i j

def transpose {m n} {α} (M : Matrix m n α) : Matrix n m α :=
  fun i j => M j i

def diag {n} {α} (M : Matrix n n α) : n → α :=
  fun i => M i i

def mul (M : Matrix (Fin l) (Fin m) Float) (N : Matrix (Fin m) (Fin n) Float) :
    Matrix (Fin l) (Fin n) Float :=
  fun i k => (fun j => M i j) ⬝ᵥᶜ (fun j => N j k)

def sum (A : Matrix (Fin n) (Fin n) Float) : Float :=
  Vec.Computable.sum (fun i => Vec.Computable.sum (A i))

def trace (A : Matrix (Fin n) (Fin n) Float) : Float :=
  (Vec.Computable.toArray (fun i => A i i)).foldl (· + ·) 0

def covarianceMatrix {N n : ℕ} (Y : Matrix (Fin N) (Fin n) Float) (i j : Fin n) : Float :=
  Vec.Computable.sum (fun k => (Y k i) * (Y k j)) / (OfNat.ofNat N)

def diagonal (x : Fin n → Float) : Matrix (Fin n) (Fin n) Float :=
  fun i j => (if i = j then x i else 0)

def fromBlocks {l : Type} {m : Type} {n : Type} {o : Type} {α : Type} :
    Matrix n l α → Matrix n m α → Matrix o l α → Matrix o m α → Matrix (n ⊕ o) (l ⊕ m) α :=
  fun A B C D i j =>
    match i with
    | Sum.inl i =>
      match j with
      | Sum.inl j => A i j
      | Sum.inr j => B i j
    | Sum.inr i =>
      match j with
      | Sum.inl j => C i j
      | Sum.inr j => D i j

private def minorAux (A : Matrix (Fin n.succ) (Fin n.succ) Float) (a b : Fin n.succ) :
    Matrix (Fin n) (Fin n) Float :=
  fun i j =>
    let i' : Fin n.succ := if i.val < a.val then i else i.succ;
    let j' : Fin n.succ := if j.val < b.val then j else j.succ;
    A i' j'

def minor (A : Matrix (Fin n) (Fin n) Float) (a b : Fin n) :
    Matrix (Fin n.pred) (Fin n.pred) Float :=
  match n with
  | 0 => fun _ => Fin.elim0
  | _ + 1 => minorAux A a b

def det {n : ℕ} (A : Matrix (Fin n) (Fin n) Float) : Float :=
  if h : 0 < n then
    if n == 1 then A ⟨0, h⟩ ⟨0, h⟩ else
      (List.finRange n).foldl (fun s i =>
        s + (-1) ^ (Float.ofNat i.val) * A i ⟨0, h⟩ * det (minor A i ⟨0, h⟩)) 0
  else 0

def inv (A : Matrix (Fin n) (Fin n) Float) : Matrix (Fin n) (Fin n) Float :=
  (1 / det A) • adjugate A

def adjugate (A : Matrix (Fin n) (Fin n) Float) : Matrix (Fin n) (Fin n) Float :=
  transpose (cofactor A)

def cofactor (A : Matrix (Fin n) (Fin n) Float) : Matrix (Fin n) (Fin n) Float :=
  fun i j => (-1) ^ (Float.ofNat (i.val + j.val)) * (A i j)

def transpose {m n} {α} (M : Matrix m n α) : Matrix n m α :=
  fun i j => M j i

def upperTriangular [LT m] (M : Matrix m m R) :=
  M.BlockTriangular id

def zeroCone (x : ℝ) : Prop :=
  x = 0

def Vec.zeroCone {n} [Fintype n] (x : n → ℝ) : Prop :=
  ∀ i, Real.zeroCone (x i)

def Matrix.zeroCone {n m} [Fintype n] [Fintype m] (M : Matrix n m ℝ) : Prop :=
  ∀ i j, Real.zeroCone (M i j)

def addMatrixAffineConstraint (data : ProblemData) (H : Array (Array (Array Float)))
    (D : Array (Array Float)) : ProblemData :=
  let constraint := MatrixAffine.mk D.size H D
  { data with matrixAffineConstraints := data.matrixAffineConstraints.push constraint }

def upperTriangular [LT m] (M : Matrix m m R) :=
  M.BlockTriangular id

def lowerTriangular [LT m] (M : Matrix m m R) :=
  M.BlockTriangular OrderDual.toDual

def Matrix.PSDCone {n} [Fintype n] (A : Matrix n n ℝ) : Prop :=
  Matrix.PosSemidef A
</used_repo_defs>

<lib_lemmas>
congr_fun in Batteries.Logic
Matrix.fromBlocks_mulVec in Mathlib.Data.Matrix.Block
Finset.prod_ne_zero_iff in Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Matrix.det_diagonal in Mathlib.LinearAlgebra.Matrix.Determinant.Basic
lt_of_lt_of_le in Mathlib.Order.Defs.PartialOrder
ne_of_gt in Mathlib.Order.Defs.PartialOrder
Matrix.det_isEmpty in Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_of_upperTriangular in Mathlib.LinearAlgebra.Matrix.Block
le_of_add_le_of_nonneg_left in Mathlib.Algebra.Order.Monoid.Unbundled.Basic
not_nonempty_iff in Mathlib.Logic.IsEmpty
</lib_lemmas>

<repo_lemmas>
lemma Real.one_sub_div_exp_pos_of_pos {x : ℝ} : 0 < x → 0 < 1 - 1 / Real.exp x

@[positivity (1 - (1 / (Real.exp (_ : ℝ))))]
def evalOneSubDivExp : PositivityExt where eval {_ _α} zα pα e := do
  let (.app (.app _sub _one) (.app (.app _div _one') (.app _exp (x : Q(ℝ))))) ←
    withReducible (whnf e) | throwError "not (1 - 1 / Real.exp x)"
  match ← core zα pα x with
  | .positive pa =>
      let pa' ← mkAppM ``Real.one_sub_div_exp_pos_of_pos #[pa]
      pure (.positive pa')
  | _ =>
      pure .none

lemma PosSemidef.PosDef_iff_det_ne_zero [DecidableEq n] {M : Matrix n n ℝ} (hM : M.PosSemidef) :
    M.PosDef ↔ M.det ≠ 0

lemma PosSemidef.PosSemidef_sqrt {A : Matrix n n ℝ} (hA : A.PosSemidef) :
    hA.1.sqrt.PosSemidef

lemma PosSemidef.add {M N : Matrix n n 𝕜} (hM : M.PosSemidef) (hN : N.PosSemidef) :
    (M + N).PosSemidef

@[simp]
lemma PosSemidef.sqrt_mul_sqrt {A : Matrix n n ℝ} (hA : A.PosSemidef) :
    hA.1.sqrt * hA.1.sqrt = A

lemma PosSemidef.conjTranspose_mul_mul (M N : Matrix n n 𝕜) (hM : M.PosSemidef) :
    (Nᴴ * M * N).PosSemidef

lemma eigenvectorMatrix_inv_mul : hA.eigenvectorMatrixInv * hA.eigenvectorMatrix = 1

theorem spectral_theorem'' :
    hA.eigenvectorMatrix * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * hA.eigenvectorMatrixᴴ =
    A

lemma conjTranspose_eq_transpose {m n : Type _} {A : Matrix m n ℝ} : Aᴴ = Aᵀ

lemma IsHermitian.fromBlocks₁₁ [Fintype m] [DecidableEq m] {A : Matrix m m 𝕜} (B : Matrix m n 𝕜)
    (D : Matrix n n 𝕜) (hA : A.IsHermitian) :
    (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian

lemma IsHermitian.fromBlocks₂₂ [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜) (B : Matrix m n 𝕜)
    {D : Matrix n n 𝕜} (hD : D.IsHermitian) :
    (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian

lemma PosSemidef.fromBlocks₁₁ [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m m 𝕜}
    (B : Matrix m n 𝕜) (D : Matrix n n 𝕜) (hA : A.PosDef) [Invertible A] :
    (fromBlocks A B Bᴴ D).PosSemidef ↔ (D - Bᴴ * A⁻¹ * B).PosSemidef

lemma PosSemidef.fromBlocks₂₂ [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜)
    (B : Matrix m n 𝕜) {D : Matrix n n 𝕜} (hD : D.PosDef) [Invertible D] :
    (fromBlocks A B Bᴴ D).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef

lemma schur_complement_eq₁₁ [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m m 𝕜}
    (B : Matrix m n 𝕜) (D : Matrix n n 𝕜) (x : m → 𝕜) (y : n → 𝕜) [Invertible A]
    (hA : A.IsHermitian) :
    vecMul (star (x ⊕ᵥ y)) (fromBlocks A B Bᴴ D) ⬝ᵥ (x ⊕ᵥ y) =
      vecMul (star (x + (A⁻¹ * B).mulVec y)) A ⬝ᵥ (x + (A⁻¹ * B).mulVec y) +
        vecMul (star y) (D - Bᴴ * A⁻¹ * B) ⬝ᵥ y

lemma schur_complement_eq₂₂ [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜)
    (B : Matrix m n 𝕜) {D : Matrix n n 𝕜} (x : m → 𝕜) (y : n → 𝕜) [Invertible D]
    (hD : D.IsHermitian) :
    vecMul (star (x ⊕ᵥ y)) (fromBlocks A B Bᴴ D) ⬝ᵥ (x ⊕ᵥ y) =
      vecMul (star ((D⁻¹ * Bᴴ).mulVec x + y)) D ⬝ᵥ ((D⁻¹ * Bᴴ).mulVec x + y) +
        vecMul (star x) (A - B * D⁻¹ * Bᴴ) ⬝ᵥ x

lemma IsHermitian.nonsingular_inv [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.IsHermitian)
    (hMdet : IsUnit M.det) : M⁻¹.IsHermitian

lemma PosDef.isUnit_det [DecidableEq n] {M : Matrix n n ℝ} (hM : M.PosDef) : IsUnit M.det

lemma PosDef.nonsingular_inv [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : M⁻¹.PosDef

lemma PosDef.det_ne_zero [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : M.det ≠ 0

lemma PosDef.PosDef_sqrt {A : Matrix n n ℝ} (hA : A.PosDef) : hA.1.sqrt.PosDef

lemma PosDef.conjTranspose_mul_mul [DecidableEq n] (M N : Matrix n n 𝕜) (hM : M.PosDef)
    (hN : N.det ≠ 0) : (Nᴴ * M * N).PosDef

lemma PosSemiDef.IsSymm {n} {A : Matrix (Fin n) (Fin n) ℝ} (hA : PosSemidef A) : IsSymm A

lemma PosSemidef.det_nonneg {M : Matrix n n ℝ} (hM : M.PosSemidef) [DecidableEq n] : 0 ≤ det M

lemma isUnit_det_of_PosDef_inv [DecidableEq n] {M : Matrix n n ℝ} (h : M⁻¹.PosDef) :
    IsUnit M.det

lemma PosDef_inv_iff_PosDef [DecidableEq n] (M : Matrix n n ℝ) : M⁻¹.PosDef ↔ M.PosDef
    
lemma conj_symm {x : n → 𝕜} {M : Matrix n n 𝕜} (hM : M.IsHermitian) :
    star (star x ⬝ᵥ mulVec M x) = star x ⬝ᵥ mulVec M x

lemma det_add_det_le_det_add [Nonempty n] (A B : Matrix n n ℝ) (hA : A.PosSemidef)
    (hB : B.PosSemidef) : A.det + B.det ≤ (A + B).det

lemma det_add_det_le_det_add' [Nonempty n] (A B : Matrix n n ℝ) (hA : A.PosDef)
    (hB : B.PosSemidef) : A.det + B.det ≤ (A + B).det

lemma sum_exp_eq_sum_div {n} (x : Fin n → ℝ) (t : ℝ) :
    Vec.sum (Vec.exp (x - Vec.const n t)) = (Vec.sum (Vec.exp x)) / (Real.exp t)

lemma sum_exp_pos {n} (hn : 0 < n) (x : Fin n → ℝ) :
    0 < Vec.sum (Vec.exp x)

lemma eigenspace_add {f g : End R M} {a b : R} :
    eigenspace f a ⊓ eigenspace g b ≤ eigenspace (f + g) (a + b)

lemma eigenspace_one : eigenspace (1 : End R M) 1 = ⊤

lemma has_eigenvector_add {f g : End R M} {a b : R} {x : M} (hf : HasEigenvector f a x)
    (hg : HasEigenvector g b x) : HasEigenvector (f + g) (a + b) x

lemma has_eigenvector_one {x : M} (hx : x ≠ 0) : HasEigenvector (1 : End R M) 1 x

lemma IsHermitian.has_eigenvector_one_add {A : Matrix n n ℝ} (hA : A.IsHermitian) (i : n) :
    Module.End.HasEigenvector
      (1 + Matrix.toLin' A) (1 + (hA.eigenvalues i)) ((hA.eigenvectorBasis) i)

lemma det_add_det_le_det_add' [Nonempty n] (A B : Matrix n n ℝ) (hA : A.PosDef)
    (hB : B.PosSemidef) : A.det + B.det ≤ (A + B).det

lemma one_add_prod_le_prod_one_add {n : Type _} [Fintype n] [Nonempty n]
    (f : n → ℝ) (hf : ∀ i, 0 ≤ f i) : 1 + (∏ i, f i) ≤ ∏ i, (1 + f i)

lemma BlockTriangular.zero : BlockTriangular (0 : Matrix m m R) b

lemma BlockTriangular_diagonal [DecidableEq m] (d : m → R) :
    BlockTriangular (diagonal d) b

lemma BlockTriangular_blockDiagonal' [DecidableEq α]
    (d : ∀ (i : α), Matrix (m' i) (m' i) R) :
    BlockTriangular (blockDiagonal'  d) Sigma.fst

lemma BlockTriangular_blockDiagonal [DecidableEq α] (d : α → Matrix m m R) :
    BlockTriangular (blockDiagonal d) Prod.snd

lemma toBlock_inverse_mul_toBlock_eq_one_of_BlockTriangular [LinearOrder α]
    [Invertible M] (hM : BlockTriangular M b) (k : α) :
    M⁻¹.toBlock (fun i => b i < k) (fun i => b i < k) *
  M.toBlock (fun i => b i < k) (fun i => b i < k) = 1

lemma inv_toBlock_of_BlockTriangular [LinearOrder α]
    [Invertible M] (hM : BlockTriangular M b) (k : α) :
    (M.toBlock (fun i => b i < k) (fun i => b i < k))⁻¹ =
    M⁻¹.toBlock (fun i => b i < k) (fun i => b i < k)

lemma toSquareBlock_inv_mul_toSquareBlock_eq_one [LinearOrder α]
    [Invertible M] (hM : BlockTriangular M b) (k : α) :
    M⁻¹.toSquareBlock b k * M.toSquareBlock b k = 1

theorem toUpperTri_zero {m : Type _} [LinearOrder m] :
    Matrix.toUpperTri (0 : Matrix m m ℝ) = 0

theorem toUpperTri_smul {m : Type _} [LinearOrder m]
    (A : Matrix m m ℝ) (κ : ℝ) :
    κ • Matrix.toUpperTri A = Matrix.toUpperTri (κ • A)

theorem toUpperTri_add {m : Type _} [LinearOrder m]
    (A B : Matrix m m ℝ) :
    Matrix.toUpperTri (A + B) = Matrix.toUpperTri A + Matrix.toUpperTri B

lemma upperTriangular_toUpperTri {m : Type _} [LinearOrder m]
    (A : Matrix m m ℝ) : A.toUpperTri.upperTriangular

lemma upperTriangular.toUpperTri_eq {A : Matrix n n ℝ}
    (hA : upperTriangular A) : A.toUpperTri = A

lemma Real.log_nonneg_of_ge_one {x : ℝ} : 0 ≤ x - 1 → 0 ≤ log x

lemma Real.log_pos_of_gt_one {x : ℝ} : 0 < x - 1 → 0 < log x

lemma Real.one_sub_one_div_sq_nonneg_of_le_one {x : ℝ} :
    0 < x → 0 ≤ 1 - x → 0 ≤ (1 / x ^ (2 : ℝ)) - 1

lemma Real.one_sub_sq_nonneg_of_le_one {x : ℝ} : 0 ≤ x → 0 ≤ 1 - x → 0 ≤ 1 - x ^ (2 : ℝ)

lemma Real.exp_sub_one_pos_of_pos {x : ℝ} : 0 < x → 0 < Real.exp x - 1

lemma Real.one_sub_div_exp_pos_of_pos {x : ℝ} : 0 < x → 0 < 1 - 1 / Real.exp x

lemma Real.scaled_sq_diff_pos_of_pos {a x : ℝ} :
    0 < a - 1 → 0 < x → 0 < (a * x) ^ (2 : ℝ) - x ^ (2 : ℝ)
  
lemma det_eq_prod_eigenvalues (xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)) (as : n → ℝ)
    (hxs : ∀ j, Module.End.HasEigenvector (Matrix.toLin' A) (as j) (xs j)) : det A = ∏ i, as i

lemma IsHermitian.hasEigenvector_eigenvectorBasis (hA : A.IsHermitian) (i : n) :
    Module.End.HasEigenvector (Matrix.toLin' A) (hA.eigenvalues i) (hA.eigenvectorBasis i)

lemma log_eq_log {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : x = y ↔ log x = log y

theorem exp_iff_expCone (t x : ℝ) : exp x ≤ t ↔ expCone x 1 t

@[simp]
lemma PosSemidef_zero : PosSemidef (0 : Matrix n n 𝕜)

lemma LogDetAtom.feasibility_PosDef {D Z : Matrix n n ℝ} (hD : D = LDL.diag hA)
    (hZ : Z = LDL.diag hA * (LDL.lower hA)ᵀ) : (fromBlocks D Z Zᵀ A).PosSemidef

lemma LogDetAtom.feasibility_PosDef' {D Z Y : Matrix n n ℝ} (hY : Y = LDL.diag hA * (LDL.lower hA)ᵀ)
    (hD : D = diagonal Y.diag) (hZ : Z = Y.toUpperTri) : (fromBlocks D Z Zᵀ A).PosSemidef

lemma LDL.diagEntries_pos {A : Matrix n n ℝ} (hA: A.PosDef) (i : n) :
    0 < LDL.diagEntries hA i

lemma LogDetAtom.solution_eq_atom {A : Matrix n n ℝ} (hA: A.PosDef) :
    ∑ i, Real.log (LDL.diagEntries hA i) = Real.log (A.det)

lemma LogDetAtom.feasibility_exp {A : Matrix n n ℝ} (hA: A.PosDef) (i : n) :
    LDL.diagEntries hA i ≤ ((LDL.diag hA) * ((LDL.lower hA)ᵀ)).diag i

lemma Real.inverse_eq_inv (a : ℝ) : Ring.inverse a = a⁻¹

lemma PosSemidef_diagonal [DecidableEq n] {f : n → ℝ} (hf : ∀ i, 0 ≤ f i) :
    (diagonal f).PosSemidef
lemma PosDef_diagonal [DecidableEq n] {f : n → ℝ} (hf : ∀ i, 0 < f i) : (diagonal f).PosDef


lemma upperTriangular_inv_of_upperTriangular [Fintype m] [LinearOrder m]
    [Invertible M] (hM : upperTriangular M) : upperTriangular M⁻¹

lemma lowerTriangular_inv_of_lowerTriangular [Fintype m] [LinearOrder m]
    [Invertible M] (hM : lowerTriangular M) : lowerTriangular M⁻¹

lemma upperTriangular.mul [Fintype m] [LinearOrder m] (hM : upperTriangular M)
    (hN : upperTriangular N) : upperTriangular (M * N)

lemma lowerTriangular.mul [Fintype m] [LinearOrder m] (hM : lowerTriangular M)
    (hN : lowerTriangular N) : lowerTriangular (M * N)

lemma lowerTriangular.transpose [Fintype m] [LinearOrder m]
    (hM : lowerTriangular M) : upperTriangular Mᵀ

lemma upperTriangular.transpose [Fintype m] [LinearOrder m]
    (hM : upperTriangular M) : lowerTriangular Mᵀ

lemma diag_inv_mul_diag_eq_one_of_upperTriangular [Fintype m] [LinearOrder m]
    [Invertible M] (hM : upperTriangular M) (k : m) :
    M⁻¹ k k * M k k = 1

lemma diag_inv_mul_diag_eq_one_of_lowerTriangular [Fintype m] [LinearOrder m]
    [Invertible M] (hM : lowerTriangular M) (k : m) : M⁻¹ k k * M k k = 1

@[simp]
lemma det_lowerInv : (lowerInv hS).det = 1

@[simp]
lemma det_lower : (lower hS).det = 1

lemma lower_eq_to_matrix :
    lower hS =
      ((@gramSchmidtBasis 𝕜 (n → 𝕜) _
        (NormedAddCommGroup.ofMatrix hS.transpose)
        (InnerProductSpace.ofMatrix hS.transpose)
  n _ _ _ (Pi.basisFun 𝕜 n)).toMatrix (Pi.basisFun 𝕜 n))ᵀ
</repo_lemmas>

<local_ctx>
import Mathlib.LinearAlgebra.Matrix.LDL

import CvxLean.Lib.Math.SchurComplement

import CvxLean.Lib.Math.Subadditivity

import CvxLean.Lib.Math.LinearAlgebra.Matrix.Triangular

import CvxLean.Lib.Math.LinearAlgebra.Matrix.ToUpperTri

import CvxLean.Lib.Math.LinearAlgebra.Matrix.LDL

namespace Matrix

open Matrix BigOperators

variable {n : Type} [Fintype n] [LinearOrder n] [LocallyFiniteOrderBot n]

variable {𝕜 : Type} [RCLike 𝕜]

variable {A : Matrix n n ℝ} (hA : A.PosDef)

open scoped Matrix ComplexOrder
</local_ctx>

<target_theorem>
lemma LogDetAtom.cond_elim {t : n → ℝ} {Y Z D : Matrix n n ℝ} (ht : ∀ i, (t i).exp ≤ Y.diag i)
    (hD : D = Matrix.diagonal (Y.diag)) (hZ : Z = Y.toUpperTri)
    (hPSD : (fromBlocks D Z Zᵀ A).PosSemidef) : A.PosDef :=
</target_theorem>

