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

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)

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

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

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 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 adjugate (A : Matrix (Fin n) (Fin n) Float) : Matrix (Fin n) (Fin n) Float :=
  transpose (cofactor A)

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

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

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

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

Array.push in Init.Prelude

let listListExpr ← mkAppM ``Array.toList #[arrayListExpr]

def Key.format : Key → Format
  | Key.star                   => "*"
  | Key.other                  => "◾"
  | Key.lit (Literal.natVal v) => Std.format v
  | Key.lit (Literal.strVal v) => repr v
  | Key.const k _              => Std.format k
  | Key.proj s i               => Std.format s ++ "." ++ Std.format i
  | Key.fvar k _               => Std.format k.name
  | Key.arrow                  => "→"

partial def getNumericalValue? : EggTree → Option Float
  | Tree.leaf s =>
      Option.map Float.ofInt s.toInt?
  | Tree.node "neg" #[(t : EggTree)] =>
      Option.map Float.neg t.getNumericalValue?
  | Tree.node "sqrt" #[(t : EggTree)] =>
      Option.map Float.sqrt t.getNumericalValue?
  | Tree.node "log" #[(t : EggTree)] =>
      Option.map Float.log t.getNumericalValue?
  | Tree.node "exp" #[(t : EggTree)] =>
      Option.map Float.exp t.getNumericalValue?
  | Tree.node "add" #[(t1 : EggTree), (t2 : EggTree)] =>
      Option.map₂ Float.add t1.getNumericalValue? t2.getNumericalValue?
  | Tree.node "sub" #[(t1 : EggTree), (t2 : EggTree)] =>
      Option.map₂ Float.sub t1.getNumericalValue? t2.getNumericalValue?
  | Tree.node "mul" #[(t1 : EggTree), (t2 : EggTree)] =>
      Option.map₂ Float.mul t1.getNumericalValue? t2.getNumericalValue?
  | Tree.node "div" #[(t1 : EggTree), (t2 : EggTree)] =>
      Option.map₂ Float.div t1.getNumericalValue? t2.getNumericalValue?
  | Tree.node "pow" #[(t1 : EggTree), (t2 : EggTree)] =>
      Option.map₂ Float.pow t1.getNumericalValue? t2.getNumericalValue?
  | _ => none

Mathlib.Meta.Positivity.core in Mathlib.Tactic.Positivity.Core

@[tactic reorderConstrs]
def evalReorderConstrs : Tactic := fun stx => match stx with
  | `(tactic| reorder_constrs [$ids,*]) => do
      let ids := ids.getElems.map Syntax.getId
      (reorderConstrsBuilder ids).toTactic
      saveTacticInfoForToken stx
  | _ => throwUnsupportedSyntax

AddCommMonoid in Mathlib.Algebra.Group.Defs

def setScalarConstraintsScalarVariablesCoord (p : Problem) (em : EncodedMatrix) : Problem :=
  { p with scalarConstraintsScalarVariablesCoord := em }

DecidablePred in Init.Prelude

private def mkArrayAux (ty : Expr) (as : List Expr) :
    MetaM Expr := do
  match as with
  | []    => return mkAppN (mkConst ``Array.empty [levelZero]) #[ty]
  | e::es =>
      let r ← mkArrayAux ty es
      mkAppM ``Array.push #[r, e]

def buildCargo (targetFile : FilePath) (manifestFile : FilePath) (targetDest : FilePath)
    (oFileJobs : Array (BuildJob FilePath)) (stopOnSuccess : Bool) :
    SpawnM (BuildJob FilePath) :=
  let name := targetFile.fileName.getD targetFile.toString
  buildFileAfterDepArray targetFile oFileJobs fun _ => do
    let env := if stopOnSuccess then #[("RUSTFLAGS", some "
    compileCargo name manifestFile (env := env)
    createParentDirs targetDest
    proc {
      cmd := "cp"
      args := #[targetFile.toString, targetDest.toString]
    }

def klDiv : m → ℝ := fun i => Real.klDiv (x i) (y i)

else
    let steps ← liftExcept <| outJson.getObjVal? "steps"
    let steps ← liftExcept <| Json.getObj? steps

def fromIndexAndEncodedMatrix (i : Nat) (em : EncodedMatrix) : EncodedMatrixList := Id.run <| do
  let mut eml := empty
  for eme in em.values do
    let emle := EncodedMatrixListEntry.fromIndexAndEncodedMatrixEntry i eme
    eml := eml.addEntry emle
  eml

def ReductionBuilder (α) := ReductionExpr → MVarId → TacticM α

DecidableEq in Init.Prelude

instance : ToString Sexp := ⟨Sexp.toString⟩

List.range in Init.Data.List.Basic

abbrev VCondIdx := Nat

@[rel]
def weaken_constraints (cs' : D → Prop) (hcs : ∀ x, cs x → cs' x) : ⟨f, cs⟩ ≽' ⟨f, cs'⟩ :=
  { phi := id,
    phi_feasibility := fun x h_feas_x => hcs x h_feas_x,
    phi_optimality := fun _ _ => le_refl _ }

def toTactic {α} (builder : EquivalenceBuilder α) : TacticM α := withMainContext do
  let transf ← TransformationGoal.fromExpr (← getMainTarget)

let paramsDecls ← (← getLCtx).decls.toArray.filterMapM (fun decl? => do
    if let some decl := decl? then
      if (← inferType decl.type).isType then return some decl else return none
    else return none)

Array.range in Init.Data.Array.Basic

private def decomposeBracketedBinder : Syntax → TermElabM (Array (Syntax × Syntax)) :=
  fun stx => match stx[0] with
    | `(bracketedBinderF|($ids* : $ty)) => return ids.map (·.raw, ty.raw)
    | `(ident|$id) => return #[(id.raw, (← `(_)).raw)]

Finset.sum in Mathlib.Algebra.BigOperators.Group.Finset.Defs

ToString in Init.Data.ToString.Basic

@[equiv]
def decompose_constraint (g : D → E) (cs' : D → E → Prop) (hc : ∀ x, cs x ↔ cs' x (g x)) :
    ⟨f, cs⟩ ≡ ⟨fun (x, _) => f x, fun (x, y) => y = g x ∧ cs' x y⟩ :=
  Equivalence.ofStrongEquivalence <|
  { phi := fun x => (x, g x),
    psi := fun (x, _) => x,
    phi_feasibility := fun {x} h_feas_x => by admit /- proof elided -/

@[equiv]
def epigraph_form : ⟨f, cs⟩ ≡ ⟨fun (t, _) => t, fun (t, x) => f x ≤ t ∧ cs x⟩ :=
  Equivalence.ofStrongEquivalence <|
  { phi := fun x => (f x, x),
    psi := fun (_, x) => x,
    phi_feasibility := fun {x} h_feas_x => by admit /- proof elided -/

withLocalDeclD `h (← mkAppM ``Minimization.constraints #[oldProblem, p]) fun h => do
      let (_, cprs) := Meta.composeAndWithProj constraints.toList
      let hProj := (cprs h).toArray

private def ignoreArg (a : Expr) (i : Nat) (infos : Array Meta.ParamInfo) : MetaM Bool := do
  if h : i < infos.size then
    let info := infos.get ⟨i, h⟩
    if info.isInstImplicit then
      return true
    else if info.isImplicit || info.isStrictImplicit then
      return not (← isType a)
    else
      isProof a
  else
    isProof a

instance : LT Key := ⟨fun a b => Key.lt a b⟩

Array.zipWith in Init.Data.Array.Basic

def runEggRequestRaw (requestJson : String) : MetaM String := do
  let eggProcess ← IO.Process.spawn {
      cmd    := "egg-pre-dcp/utils/egg-pre-dcp",
      stdout := IO.Process.Stdio.piped,
      stdin  := IO.Process.Stdio.piped,
      stderr := IO.Process.Stdio.null
    }

def compileCargo (name : String) (manifestFile : FilePath) (cargo : FilePath := "cargo")
    (env : Array (String × Option String)) : LogIO Unit := do
  logInfo s!"Creating {name}"
  proc {
    env := env
    cmd := cargo.toString
    args := #["build", "
  }

@[equiv]
noncomputable def map_objFun_log {f : D → ℝ} (h : ∀ x, cs x → f x > 0) :
    ⟨f, cs⟩ ≡ ⟨fun x => (Real.log (f x)), cs⟩ :=

instance : ToMessageData AtomData where
  toMessageData
  | AtomData.graph d => toMessageData d

@[equiv]
def rewrite_objFun_8 (hrw :
    ∀ x, c1 x → c2 x → c3 x → c4 x → c5 x → c6 x → c7 x → c8 x → f x = g x) :
    ⟨f, [[c1, c2, c3, c4, c5, c6, c7, c8]]⟩ ≡ ⟨g, [[c1, c2, c3, c4, c5, c6, c7, c8]]⟩ :=
  rewrite_objFun (fun x _ => by admit /- proof elided -/
  )

private def constraints : Parsec (List Constraint) :=
  constraintsTitle   *>
  constraintsHeaders *>
  Array.data <$> many constraint

let ds := pat.newConstrVarsArray.map (mkFVar ·.fvarId)
              mkLambdaFVars (xs ++ bs ++ vs ++ zs ++ cs ++ ds) optCondAdjusted

def nonnegOrthCone (x : ℝ) : Prop :=
  0 ≤ x

def Sexp.fromList : List Sexp → Sexp
  | xs => Sexp.list xs

def elabReductionProof (lhs : Expr) (rhsName : Name) (stx : Syntax) : TermElabM (Expr × Expr) :=
  elabTransformationProof TransformationGoal.Reduction lhs rhsName stx

check adjustedOptimality
        trace[CvxLean.debug] "adjustedOptimality: {adjustedOptimality}"

LE.le in Init.Prelude

Lean.Syntax.getId in Init.Prelude

let objFunBackwardBody := objFunBackwardBody.replaceFVars
        (newConstrVars.map (mkFVar ·.fvarId))
        (hProj.drop (hProj.length - newConstrVars.size)).toArray

abbrev FeasibilityProof := Expr

Neg.neg in Init.Prelude

def isTransitive : TransformationGoal → Bool
  | TransformationGoal.Solution => false
  | _ => true

modify in Init.Prelude

Lean.Syntax.ident in Init.Prelude

def map (f : α → β) (oc : OC α) : OC β :=
  OC.mk (f oc.objFun) (oc.constrs.map f)

def withCopyOfMonoXs {α} [Inhabited α] (xs : Array Expr) (argKinds : Array ArgKind)
    (f : Array Expr → Array Expr → Array ArgKind → TermElabM α) : TermElabM α := do
  
  let mut argDeclInfo : Array (Name × (Array Expr → TermElabM Expr)) := #[]
  let mut monoXs := #[]
  let mut monoArgKind := #[]
  for i in [:xs.size] do
    if argKinds[i]! != ArgKind.Constant ∧ argKinds[i]! != ArgKind.Neither then
      let ty := ← inferType xs[i]!
      let name := (← FVarId.getDecl xs[i]!.fvarId!).userName
      argDeclInfo := argDeclInfo.push (name, fun _ => pure ty)
      monoXs := monoXs.push xs[i]!
      monoArgKind := monoArgKind.push argKinds[i]!

Lean.getMaxHeight in Lean.Environment

Lean.Elab.Term.commitIfNoErrors? in Lean.Elab.Term.TermElabM

return res

@[tactic renameVars]
partial def evalRenameVars : Tactic := fun stx => match stx with
| `(tactic| rename_vars [$ids,*]) => do
    let names := (ids.elemsAndSeps.map Syntax.getId).filter (· != Lean.Name.anonymous)
    (renameVarsBuilder names).toTactic
    saveTacticInfoForToken stx
| _ => throwUnsupportedSyntax

def SexpM.pushSexp (sexp: Sexp): SexpM Unit := do
  let state ← get
  if state.stack.length == 0 then
    set { state with stack := [], sexps := sexp :: state.sexps }
  else
    set { state with stack := (SexpTok.sexp sexp) :: state.stack }

def setObjSense (p : Problem) (os : ObjSense) : Problem :=
  { p with objSense := os }

def decomposeDomain (domain : Expr) : m (List (Name × Expr)) := do
  match domain with
  | .app (.app (.const `Prod _) ty1) ty2 => do
      return (← decomposeLabel ty1) :: (← decomposeDomain ty2)
  | _ => do return [← decomposeLabel domain]

List.toString in Init.Data.ToString.Basic

@[positivity (log (_ : ℝ))]
def evalLog : PositivityExt where eval {_ _α} zα pα e := do
  let (.app _log (x : Q(ℝ))) ←
    withReducible (whnf e) | throwError "not (Real.log x)"
  
  match ← core zα pα (q($x - (1 : ℝ)) : Q(ℝ)) with
  | .nonnegative pa =>
      let pa' ← mkAppM ``Real.log_nonneg_of_ge_one #[pa]
      pure (.nonnegative pa')
  | .positive pa =>
      let pa' ← mkAppM ``Real.log_pos_of_gt_one #[pa]
      pure (.positive pa')
  | _ =>
      pure .none

IO.FS.Mode.write in Init.System.IO

def maximizeNeg := @Neg.neg

Real.instPow in Mathlib.Analysis.SpecialFunctions.Pow.Real

let backwardMap ← makeBackwardMap originalVars mkDomain

Set in Mathlib.Data.Set.Defs

Lean.Parser.ppSpace in Lean.Parser.Extra

def AtomExtension : Type :=
  PersistentEnvExtension
    (Array Key × AtomData) (Array Key × AtomData) (DiscrTree AtomData)
deriving Inhabited

def findIdx' (p : α → Prop) [DecidablePred p] : List α → Option ℕ
  | []     => none
  | (a::l) => if p a then some 0 else (findIdx' p l).map Nat.succ

Preorder in Mathlib.Order.Defs.PartialOrder

def setScalarVariables (p : Problem) (cp : ConeProduct) : Problem :=
  { p with scalarVariables := cp }

private def varsHeaders : Parsec Unit :=
  skipString "INDEX"       <* ws' <*
  skipString "NAME"        <* ws' <*
  skipString "AT"          <* ws' <*
  skipString "ACTIVITY"    <* ws' <*
  skipString "LOWER LIMIT" <* ws' <*
  skipString "UPPER LIMIT" <* ws' <*
  skipString "DUAL LOWER"  <* ws' <*
  skipString "DUAL UPPER"  <* ws' <*
  (skipString "CONIC DUAL" <|> pure ()) <* ws' <* endOfLine

instance : ToString ScalarAffine where
  toString sa := s!"ScalarAffine [{sa.n}, {sa.m}, {sa.A}, {sa.a}, {sa.b}]"

instance : ToExpr (Array (Array Float)) :=

private def tmpMVarId : MVarId := { name := `_discr_tree_tmp }

Monad in Init.Prelude

let constrBackward ← makeConstrBackward pat.vcondElimMap E canonProblemExpr originalVars
            newVars (pat.optimality.constrs.map (·.val)) canonConstrs pat.newConstrs
            pat.newConstrVarsArray

def Key.arity : Key → Nat
  | Key.const _ a => a
  | Key.fvar _ a  => a
  | Key.arrow     => 2
  | Key.proj ..   => 1
  | _             => 0

let newConstrProofs := pat.feasibility.fold #[] fun acc fs => fs.fold acc Array.append
        let newFeasibility ← newConstrProofs.mapM (fun e =>
          withLocalDeclsDNondep vconds fun cs => do
            withLocalDeclsDNondep bconds fun bs => do
              mkLambdaFVars (xs ++ cs ++ bs) (e.replaceFVars vs vsSol))

liftTermElabM do
      trace[CvxLean.debug] "Addding atom {atomData}"
      addAtom <| AtomData.graph atomData
  | _ => throwUnsupportedSyntax

let objFunBackwardBody := objFunBackwardBody.replaceFVars
        (xs ++ ys) prs.toArray

private abbrev getUnifyKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
  getKeyArgs e (isMatch := false) (_root := root)

def delabVar (e : Expr) : DelabM (Lean.Name × Term) := do
  match e with
  | Expr.mdata m e =>
      match m.get? `CvxLeanLabel with
      | some (name : Lean.Name) => return (name, ← descend e 0 do delab)
      | none => Alternative.failure
  | _ => return (`_, ← delab)

abbrev VCondElimMap := Std.HashMap Nat Expr

def empty : DimensionList := DimensionList.mk 0 []

def cleanUpCompAux (e : Expr) (name : String) : MetaM Expr := do
  match e with
  | .app (.app (.app (.app (.app (.const ``Function.comp lvls) ty₁) ty₂) ty₃) f₁) f₂ => do
      let f₂ ← instantiateMVars <| ← whnf f₂
      let f₁ ← instantiateMVars f₁
      return mkApp5 (mkConst ``Function.comp lvls) ty₁ ty₂ ty₃ f₁ f₂
  | _ => throwError "{name} not of the form '... ∘ ...'"

Fin.val in Init.Prelude

Lean.mkLambda in Lean.Expr

structure CanonExprWithSolution where
  canonExpr : CanonExpr
  solution : Solution
deriving Inhabited

Lean.mkLet in Lean.Expr

Invertible in Mathlib.Algebra.Group.Invertible.Defs

def finRange' (d n : Nat) : List (Fin n) :=
  if hn : 0 < n then (List.range d).map (Fin.ofNat' · hn) else []

def setObjectiveOnlyMatrix (data : ProblemData) (A : Array (Array Float)) (b : Float) :
    ProblemData :=
  data.setObjective A #[] b

def empty : EncodedMatrixList := EncodedMatrixList.mk 0 []

instance {dl} : Decidable (isEmpty dl) := Nat.decEq _ _

@[equiv]
def eq_to_le_left {S} [Preorder S] (e : D ≃ S × E) (g : E → S) (cs' : D → Prop)
    (hcs : ∀ {x}, cs x ↔ ((e x).1 = g (e x).2 ∧ cs' x))
    (hf : ∀ y r s, f (e.symm (r, y)) = f (e.symm (s, y)))
    (h_mono: ∀ y r s, r ≤ s → cs' (e.symm (r, y)) → cs' (e.symm (s, y))) :
    ⟨f, cs⟩ ≡ ⟨f, fun x => (e x).1 ≤ g (e x).2 ∧ cs' x⟩ :=
  Equivalence.ofStrongEquivalence <|
  { phi := fun x => x,
    psi := fun x => e.symm (g (e x).2, (e x).2),
    phi_feasibility := fun {x} h_feas_x => ⟨le_of_eq (hcs.1 h_feas_x).1, (hcs.1 h_feas_x).2⟩,
    psi_feasibility := fun {x} h_feas_x => by admit /- proof elided -/

structure StrongEquivalence where
  phi : D → E
  psi : E → D
  phi_feasibility : ∀ x, p.feasible x → q.feasible (phi x)
  psi_feasibility : ∀ y, q.feasible y → p.feasible (psi y)
  phi_optimality : ∀ x, p.feasible x → q.objFun (phi x) ≤ p.objFun x
  psi_optimality : ∀ y, q.feasible y → p.objFun (psi y) ≤ q.objFun y

Lean.Meta.mkAppOptM in Lean.Meta.AppBuilder

let rhsName := probIdStx.getId
      let (rhs, proof) ← elabRelaxationProof lhs rhsName proofStx.raw

let zsSolInTermsOfXs ← pat.forwardImagesNewVars.mapM (fun e => mkLambdaFVars xs
          (e.replaceFVars vs vsSol))

Float.ofScientific in Init.Data.OfScientific

Lean.Parser.ppGroup in Lean.Parser.Extra

def ofStrongEquivalence (E : p ≡' q) : p ≽' q :=
  { phi := E.phi,
    phi_feasibility := E.phi_feasibility,
    phi_optimality := E.phi_optimality }

partial def runEquivalenceTactic (mvarId : MVarId) (stx : Syntax) : TermElabM Unit := do
  runTransformationTactic TransformationGoal.Equivalence mvarId stx

if isMap then
    
    if let gs@(_ :: _) ← evalTacticAt tacStx g then
      trace[CvxLean.debug] "`pre_dcp` failed to close goals: {gs}."
      throwPreDCPError "failed to apply {step.rewriteName}."
  else
    
    
    let fvars := Array.mk <| vars.map (fun v => mkFVar (FVarId.mk v))
    let paramsFvars := Array.mk <| params.map (fun v => mkFVar (FVarId.mk v))
    let paramsDeclsIds := Array.mk <| paramsDecls.map (fun decl => mkFVar decl.fvarId)
    let D ← instantiateMVars eqvExpr.domainLHS

def EggOCTreeExtended := EggOCTree × Array EggDomainIdentified

Task in Init.Core

Except.ok in Init.Prelude

@[red]
def rewrite_constraint_2 (hrw : ∀ x, c1 x → cs x → (c2 x ↔ c2' x)) :
    ⟨f, [[c1, c2, cs]]⟩ ≼ ⟨f, [[c1, c2', cs]]⟩ :=
  ofEquivalence <| Equivalence.rewrite_constraint_2 hrw

EuclideanSpace.single in Mathlib.Analysis.InnerProductSpace.PiL2

Matrix.toLin' in Mathlib.LinearAlgebra.Matrix.ToLin

abbrev AtomDataTrees := GraphAtomDataTree × ArgumentsTree × CurvatureTree × BCondsTree

partial def realToFloat (e : Expr) : MetaM Expr := do
  let e ← e.removeMData
  let discrTree ← getRealToFloatDiscrTree
  let translations ← discrTree.getMatch e
  for translation in translations do
    let (mvars, _, pattern) ← lambdaMetaTelescope translation.real
    if ← isDefEq pattern e then
      \n{pattern} \n{e}"
  match e with
  | Expr.app a b => return mkApp (← realToFloat a) (← realToFloat b)
  | Expr.lam n ty b d => do
      withLocalDecl n d (← realToFloat ty) fun fvar => do
        let b := b.instantiate1 fvar
        let bF ← realToFloat b
        mkLambdaFVars #[fvar] bF
  | Expr.forallE n ty b d => do
      withLocalDecl n d (← realToFloat ty) fun fvar => do
        let b := b.instantiate1 fvar
        let bF ← realToFloat b
        mkForallFVars #[fvar] bF
  | Expr.mdata m e => return mkMData m (← realToFloat e)
  | Expr.letE n ty t b _ => return mkLet n (← realToFloat ty) (← realToFloat t) (← realToFloat b)
  | Expr.proj typeName idx struct => return mkProj typeName idx (← realToFloat struct)
  | e@(Expr.const n _) => do
      if ← isOptimizationParam n then
        let paramExpr ← getOptimizationParamExpr n e
        let paramExprF ← realToFloat paramExpr
        \n{e.toMessageData}"
        return paramExprF
      else
        return e
  | _ => return e

def mkExistsIntro (xs : Array Expr) (e : Expr) : MetaM Expr := do
  let mut res := e
  for i in [:xs.size] do
    let x := xs[xs.size - i - 1]!
    res ← mkAppOptM ``Exists.intro
      #[none, some <| ← mkLambdaFVars #[x] (← inferType res), some x, some res]
  return res

@[command_elab atomWithBCondsCommand] unsafe def elabAtomWithBCondsCommand : CommandElab
  | `(declare_atom $id [ $curv ] $args* : $expr :=
      bconditions $bconds*
      vconditions $vconds*
      implementationVars $impVars*
      implementationObjective $impObj
      implementationConstraints $impConstrs*
      solution $sols*
      solutionEqualsAtom $solEqAtom
      feasibility $feas*
      optimality $opt
      vconditionElimination $vcondElim*) => do
    let atomData ← liftTermElabM do
      let curv ← elabCurvature curv.raw
      let (argDecls, argKinds) ← elabArgKinds args.rawImpl
      let (expr, bodyTy) ← elabExpr expr.raw argDecls
      let (bconds, _) ← elabBConds argDecls bconds.rawImpl
      let (vconds, vcondMap) ← elabVConditions argDecls vconds.rawImpl
      let (impVars, impVarMap) ← elabImpVars argDecls impVars.rawImpl
      let impObj ← elabImpObj argDecls impVars impObj.raw bodyTy
      let impConstrs ← elabImpConstrs argDecls impVars bconds impConstrs.rawImpl
      let sols ← elabSols argDecls impVars impVarMap sols.rawImpl
      let solEqAtom ← elabSolEqAtom argDecls vconds impObj sols expr solEqAtom.raw
      let feas ← elabFeas argDecls vconds bconds impConstrs sols feas.rawImpl
      let opt ← elabOpt curv argDecls expr bconds impVars impObj impConstrs argKinds opt.raw
      let vcondElim ← elabVCondElim curv argDecls bconds vconds vcondMap impVars impConstrs argKinds
        vcondElim.rawImpl

def replaceProjections (e : Expr) (p : FVarId) (rs : Array Expr) : MetaM Expr := do
  let pre (e : Expr) : MetaM TransformStep := do
    match ← decomposeProj e p rs.data with
    | some r => return TransformStep.done r
    | none => return TransformStep.continue
  transform e (pre := pre)
where
  decomposeProj (e : Expr) (p : FVarId) (rs : List Expr) (first : Option Bool := none) :
      MetaM (Option Expr) := do
    
    
    
    
    match first, e, rs with
    | _, .fvar fVarId, [r] =>
        if fVarId == p then return r else return none
    | some true, .fvar fVarId, r :: _ :: _ =>
        if fVarId == p then return r else return none
    | none, .app (.app (.app (.const ``Prod.fst _) _) _) e, r :: rs => do
        decomposeProj e p (r :: rs) (first := true)
    | _, .app (.app (.app (.const ``Prod.snd _) _) _) e, _ :: rs => do
        decomposeProj e p rs (first := first == some true)
    | _, _, [] => return none
    | _, _, _ :: _ => return none

HMul.hMul in Init.Prelude

@[rel]
def remove_constraint {c cs' : D → Prop} (hcs : ∀ x, cs x ↔ c x ∧ cs' x) : ⟨f, cs⟩ ≽' ⟨f, cs'⟩ :=
  { phi := id,
    phi_feasibility := fun x h_feas_x => ((hcs x).mp h_feas_x).2,
    phi_optimality := fun _ _ => le_refl _ }

def additivity := leading_parser withPosition <|
  nonReservedSymbol "additivity" >>
  checkColGt "indented term" >> termParser

noncomputable instance instDivReal : Div ℝ :=

@[positivity (1 - ((_ : ℝ) ^ (2 : ℝ)))]
def evalOneSubSq : PositivityExt where eval {_ _α} zα pα e := do
  let (.app (.app _sub _one) (.app (.app _pow (x : Q(ℝ))) _two)) ←
    withReducible (whnf e) | throwError "not (1 - x ^ 2)"
  
  let h1 := ← do
    match ← core zα pα x with
    | .nonnegative pa => return some pa
    | .positive pa =>
        let pa ← mkAppM ``le_of_lt #[pa]
        return some pa
    | _ => return none
  
  let h2 := ← do
    match ← core zα pα (q((1 : ℝ) - $x) : Q(ℝ)) with
    | .nonnegative pa => return some pa
    | .positive pa =>
        let pa ← mkAppM ``le_of_lt #[pa]
        return some pa
    | _ => return none
  
  match h1, h2 with
  | some h1', some h2' =>
      let pa' ← mkAppM ``Real.one_sub_sq_nonneg_of_le_one #[h1', h2']
      pure (.nonnegative pa')
  | _, _ =>
      pure .none

@[strong_equiv]
def symm (E : p ≡' q) : q ≡' p :=
  { phi := E.psi,
    psi := E.phi,
    phi_feasibility := E.psi_feasibility,
    psi_feasibility := E.phi_feasibility,
    phi_optimality := E.psi_optimality,
    psi_optimality := E.phi_optimality }

@[inline]
def fold (initialKeys : Array Key) (f : σ → Array Key → α → σ) (init : σ)
    (t : Trie α) : σ :=
  Id.run $ t.foldM initialKeys (init := init) λ s k a => return f s k a

abbrev VCondsIdxsTree := Tree VCondsIdxs Unit

Lean.withRef in Init.Prelude

MonadReaderOf in Init.Prelude

Lean.Elab.Tactic.evalTacticAt in Lean.Elab.Tactic.Basic

structure Minimization (D R : Type) where
  objFun : D → R
  constraints : D → Prop

@[equiv]
def graph_expansion_least {S} [Preorder S] (g : D → S) (c d : S → D → Prop) (h : S → D → R)
    (hg : ∀ x v, c v x → IsLeast {y | d y x} (g x))
    (hf : ∀ x, f x = h (g x) x)
    (hcs : ∀ x, cs x = c (g x) x)
    (h_mono_f : ∀ x r s, r ≤ s → h r x ≤ h s x)
    (h_mono_cs : ∀ x r s, r ≤ s → c s x → c r x) :
    ⟨f, cs⟩ ≡ ⟨fun (s, y) => h s y, fun (s, y) => d s y ∧ c s y⟩ :=
  Equivalence.ofStrongEquivalence <|
  { phi := fun x => (g x, x),
    psi := fun (_, y) => y,
    phi_feasibility := fun {x} h_feas_x => by admit /- proof elided -/

def mkAndProj (e : Expr) (i : Nat) (total : Nat) : MetaM Expr := do
  match total, i with
    | 1, 0 => return e
    | 0, _ => throwError "total too small"
    | _, 0 => return ← mkAppM ``And.left #[e]
    | total + 1, i + 1 => mkAndProj (← mkAppM ``And.right #[e]) i total

instance ChangeOfVariables.prod_right {D E F} (c : E → D) [cov : ChangeOfVariables c] :
    ChangeOfVariables (fun x : F × E => (x.1, c x.2)) :=
  { inv := fun ⟨x₁, x₂⟩ => (x₁, cov.inv x₂)
    condition := fun ⟨_, x₂⟩ => cov.condition x₂
    property := fun ⟨x₁, x₂⟩ hx => by admit /- proof elided -/

@[equiv]
def rewrite_constraint_7_last
    (hrw : ∀ x, c1 x → c2 x → c3 x → c4 x → c5 x → c6 x → (c7 x ↔ c7' x)) :
    ⟨f, [[c1, c2, c3, c4, c5, c6, c7]]⟩ ≡ ⟨f, [[c1, c2, c3, c4, c5, c6, c7']]⟩ :=
  equivalence_of_rw_constr hrw

@[command_elab affineAtomCommand] unsafe def elabAffineAtomCommand : CommandElab
  | `(declare_atom $id [ affine ] $args* : $expr :=
      bconditions $bconds*
      homogenity $hom
      additivity $add
      optimality $opt) => do
    let atomData ← liftTermElabM do
      let (argDecls, argKinds) ← elabArgKinds args.rawImpl
      let (expr, _bodyTy) ← elabExpr expr.raw argDecls
      let vconds := #[]
      let impVars := #[]
      let impObj := expr
      let impConstrs := #[]
      let sols := #[]
      let solEqAtom ← lambdaTelescope expr fun xs body => do
        return ← mkLambdaFVars xs <| ← mkEqRefl body
      let feas := #[]
      let (bconds, _) ← elabBConds argDecls bconds.rawImpl
      let hom ← elabHom argDecls expr argKinds hom.raw
      check hom 
      let add ← elabAdd argDecls expr argKinds add.raw
      check add 
      let optConcave ← elabOpt Curvature.Concave argDecls expr bconds impVars impObj impConstrs
        argKinds opt.raw
      let optConvex ←
        withExistingLocalDecls argDecls.toList do
          let xs := argDecls.map (mkFVar ·.fvarId)
          let bconds := bconds.map fun (n,c) => (n, mkAppNBeta c xs)
          withLocalDeclsDNondep bconds fun as => do
            withCopyOfMonoXs xs argKinds fun _monoXs ys _monoArgKind => do
              let mut optInverted := optConcave
              let mut i' := 0
              for i in [:xs.size] do
                if argKinds[i]! != ArgKind.Constant ∧ argKinds[i]! != ArgKind.Neither then
                  optInverted := mkApp optInverted ys[i']!
                  i' := i' + 1
                else
                  optInverted := mkApp optInverted xs[i]!
              optInverted := mkAppN optInverted as
              for i in [:xs.size] do
                if argKinds[i]! != ArgKind.Constant ∧ argKinds[i]! != ArgKind.Neither then
                  optInverted := mkApp optInverted xs[i]!
              return ← mkLambdaFVars (xs ++ as ++ ys) optInverted
      let opt ← mkAppM ``And.intro #[optConcave, optConvex]
      let vcondElim := #[]

Fintype.card in Mathlib.Data.Fintype.Card

List.cons in Init.Prelude

Float in Init.Data.Float

def mkSolEqAtomOC (originalVarsDecls : Array LocalDecl) (atoms : OC GraphAtomDataTree)
    (canonWithSolution : OC CanonExprsWithSolutionTree) (vcondVars : OC VCondsTree)
    (originalConstrVars : Array LocalDecl) : MetaM (OC SolEqAtomProofsTree) :=
  withExistingLocalDecls originalVarsDecls.toList do
    withExistingLocalDecls originalConstrVars.toList do
      let solEqAtom ← OC.map3M mkSolEqAtom atoms canonWithSolution vcondVars
      trace[CvxLean.debug] "`solEqAtom`: {solEqAtom}."
      return solEqAtom

instance : ToMessageData ArgKind where
  toMessageData
  | ArgKind.Increasing => "increasing"
  | ArgKind.Decreasing => "decreasing"
  | ArgKind.Neither => "neither"
  | ArgKind.Constant => "constant"

liftTermElabM do
      trace[CvxLean.debug] "Adding atom data {atomData}"
      addAtom <| AtomData.graph atomData
  | _ => throwUnsupportedSyntax

let currNamespace ← getCurrNamespace
      let probId := currNamespace ++ probIdStx.getId
      let relId := currNamespace ++ relIdStx.getId

Matrix.toBlock in Mathlib.Data.Matrix.Block

abbrev OptimalityProofsTree := Tree OptimalityProof OptimalityProof

@[command_elab «reductionAndBwdMap»]
def evalReductionAndBwdMap : CommandElab := fun stx => match stx with
  | `(reduction* $eqvId / $probId $declSig := $proofStx) => do
      liftTermElabM do
        let (binders, lhsStx) := expandDeclSig declSig.raw
        elabBindersEx binders.getArgs fun xs =>
          evalReductionAux probId eqvId xs lhsStx proofStx true
  | _ => throwUnsupportedSyntax

inductive Curvature where
  | Constant | Affine | Concave | Convex | AffineSet | ConvexSet
deriving BEq, Inhabited

HPow.hPow in Init.Prelude

abbrev PreVCondsTree := Tree PreVConds Unit

@[red]
def rewrite_constraint_7_last
    (hrw : ∀ x, c1 x → c2 x → c3 x → c4 x → c5 x → c6 x → (c7 x ↔ c7' x)) :
    ⟨f, [[c1, c2, c3, c4, c5, c6, c7]]⟩ ≼ ⟨f, [[c1, c2, c3, c4, c5, c6, c7']]⟩ :=
  ofEquivalence <| Equivalence.rewrite_constraint_7_last hrw

partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) := do
  Core.checkMaxHeartbeats "getUnify"
  let (k, args) ← getUnifyKeyArgs e (root := true)
  match k with
  | Key.star => d.root.foldlM (init := #[]) fun result k c => process k.arity #[] c result
  | _ =>
    let result := getStarResult d
    match d.root.find? k with
    | none   => return result
    | some c => process 0 args c result
where
  process (skip : Nat) (todo : Array Expr) (c : Trie α) (result : Array α) : MetaM (Array α) := do
    match skip, c with
    | skip + 1, Trie.node _vs cs =>
      if cs.isEmpty then
        return result
      else
        cs.foldlM (init := result) fun result ⟨k, c⟩ => process (skip + k.arity) todo c result
    | 0, Trie.node vs cs => do
      if todo.isEmpty then
        return result ++ vs
      else if cs.isEmpty then
        return result
      else
        let e     := todo.back
        let todo  := todo.pop
        let (k, args) ← getUnifyKeyArgs e (root := false)
        let visitStar (result : Array α) : MetaM (Array α) :=
          let first := cs[0]!
          if first.1 == Key.star then
            process 0 todo first.2 result
          else
            return result
        let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
          match findKey cs k with
          | none   => pure result
          | some c => process 0 (todo ++ args) c.2 result
        match k with
        | Key.star  => cs.foldlM (init := result) fun result ⟨k, c⟩ => process k.arity todo c result
        
        | Key.arrow => visitNonStar Key.other #[] (← visitNonStar k args (← visitStar result))
        | _         => visitNonStar k args (← visitStar result)

abbrev VConds := Array VCond

private def tmpStar := mkMVar tmpMVarId

\n{e.toMessageData}"

Lean.Elab.Term.elabTerm in Lean.Elab.Term.TermElabM

abbrev OptimalityAndVCondElimProofs := OptimalityProof × VCondElimProofs

Decidable in Init.Prelude

return res
</all_available_defs>

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

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

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

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 PosDef.PosDef_sqrt {A : Matrix n n ℝ} (hA : A.PosDef) : hA.1.sqrt.PosDef

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

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 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 PosSemidef.det_nonneg {M : Matrix n n ℝ} (hM : M.PosSemidef) [DecidableEq n] : 0 ≤ det M

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

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

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

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

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

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

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

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

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

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

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

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

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

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.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 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 log_eq_log {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : x = y ↔ log x = log y

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

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

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

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

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

lemma rpow_eq_mul_rpow_pred {x y : ℝ} (hx : x ≠ 0) :
    x ^ y = x * (x ^ (y - 1))

theorem vecCons_zero_zero {n} [Zero α] : vecCons (0 : α) (0 : Fin n → α) = 0
</all_available_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>

