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

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

@[command_elab «time_cmd»]
def evalTimeCmd : CommandElab := fun stx => match stx with
  | `(time_cmd $cmd) => do
      let before ← BaseIO.toIO IO.monoMsNow
      elabCommand cmd
      let after ← BaseIO.toIO IO.monoMsNow
      let diff := after - before
      dbg_trace s!"Command time: {diff} ms"
  | _ => throwUnsupportedSyntax

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

if responseType == "Error" then
    match (outJson.getObjValD "error").getStr? with
    | Except.error _ => throwError "error calling `egg`."
    | Except.ok errorMessage => throwError "from `egg` (\"{errorMessage}\")."

Lean.mkIdent in Init.Meta.Defs

abbrev FeasibilityProof := Expr

Empty in Init.Prelude

abbrev NewVarsTree := Tree (Array LocalDecl) Unit

@[default_instance]
noncomputable instance (priority := high) : HPow ℝ ℝ ℝ :=

noncomputable def huber (x : Real) :=
  if abs x ≤ 1 then x ^ 2 else 2 * abs x - 1

Lean.LocalDecl.cdecl in Lean.LocalContext

def fromArray (a : Array Float) : EncodedVector := Id.run <| do
  let mut ev := empty
  for (i, ai) in a.data.enum do
    if ai > 0 || ai < 0 then
      ev := ev.addEntry (EncodedVectorEntry.mk i ai)
  return ev

Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg in Lean.PrettyPrinter.Delaborator.SubExpr

match remainingGoals with
    | [] => pure ()
    | _ => reportUnsolvedGoals remainingGoals

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

Lean.Expr.mdata in Lean.Expr

instance : ToString EggRewriteDirection where
  toString := EggRewriteDirection.toString

private def char : Parsec Char :=
  asciiLetter <|> hexDigit <|> pchar '_' <|> fail "Invalid character."

Lean.MData in Lean.Expr

Sub.sub in Init.Prelude

def RealToFloatExtension :=
  PersistentEnvExtension
    (Array Key × RealToFloatData) (Array Key × RealToFloatData) (DiscrTree RealToFloatData)
deriving Inhabited

def preElabLetVars (letVars : Array (TSyntax `CvxLean.Parser.letVar)) :
    TermElabM (Array (Lean.Name × TSyntax `Lean.Parser.Term.letDecl)) := do
  letVars.mapM fun stx =>
    match stx with
      | `(CvxLean.Parser.letVar| with $letD:letDecl) =>
          match letD with
          | `(letDecl| $id:ident := $_) => return (id.getId, letD)
          | _ => throwParserError "expected identified let declaration got {letD}."
      | _ => throwParserError "expected let declaration got {stx}."

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

structure RelaxationExpr where
  domainP : Expr
  domainQ : Expr
  codomain : Expr
  codomainPreorder : Expr
  p : Expr
  q : Expr

Lean.levelOne in Lean.Level

HMul in Init.Prelude

H in examples.HarmonicOscillator

Lean.Expr.headBeta in Lean.Expr

structure EncodedMatrixEntry where
  i : Nat
  j : Nat
  value : Float

Lean.PrettyPrinter.Delaborator.delab in Lean.PrettyPrinter.Delaborator.Basic

def toMinimizationExprRHS (redExpr : ReductionExpr) : MetaM MinimizationExpr :=
  MinimizationExpr.fromExpr redExpr.rhs

Module in Mathlib.Algebra.Module.Defs

Except in Init.Prelude

Lean.FVarId in Lean.Expr

instance : Trans (@Relaxation D E R _) (@StrongEquivalence E F R _) (@Relaxation D F R _) :=
  { trans := fun R E => Relaxation.trans R (ofStrongEquivalence E) }

Lean.Parser.Term.ident in Lean.Parser.Term

def val : Tree α α → α
  | node val _ => val
  | leaf val => val

def addEntry (emll : EncodedMatrixListList) (emlle : EncodedMatrixListListEntry) :
    EncodedMatrixListList :=
  if emlle.value > 0 || emlle.value < 0 then
    EncodedMatrixListList.mk (emll.n + 1) (emll.values.concat emlle)
  else emll

let atomData ← addAtomDataDecls id.getId atomData

let renamedVars ← manipulateVars vars names.data
  let newDomain := composeDomain renamedVars

@[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 rewrite_objFun (hrw : ∀ x, cs x → f x = g x) : ⟨f, cs⟩ ≡ ⟨g, cs⟩ :=
  Equivalence.ofStrongEquivalence <|
  { phi := id,
    psi := id,
    phi_feasibility := fun _ hx => hx
    psi_feasibility := fun _ hx => hx
    phi_optimality := fun {x} hx => le_of_eq (hrw x hx).symm
    psi_optimality := fun {x} hx => le_of_eq (hrw x hx) }

instance (a b : Key) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))

IO.rand in Init.Data.Random

private def statusKey : Parsec StatusKey :=
  (skipString "UN" *> pure StatusKey.UN) <|>
  (skipString "BS" *> pure StatusKey.BS) <|>
  (skipString "SB" *> pure StatusKey.SB) <|>
  (skipString "LL" *> pure StatusKey.LL) <|>
  (skipString "UL" *> pure StatusKey.UL) <|>
  (skipString "EQ" *> pure StatusKey.EQ) <|>
  (skipString "**" *> pure StatusKey.IN) <|>
  (fail "Invalid status key.")

def p₁ :=
  optimization (x y : ℝ)
    maximize sqrt (x - y)
    subject to
      c1 : y = 2 * x - 3
      c2 : x ^ (2 : ℝ) ≤ 2
      c3 : 0 ≤ x - y

let constrsOptimalityProofs := pat.optimality.constrs.map Tree.val
        let objFunOptimalityProof := pat.optimality.objFun.val
        let adjustedOptimality ←
          withLocalDeclsDNondep bconds fun bs => do
            
            
            let optimalityXsBConds := mkAppN atomData.optimality (xs ++ bs ++ vs)
            withLocalDeclsDNondep (canonConstrs.map (fun rc => (`_, rc))) fun cs => do
              
              let mut optimalityAfterCanon := optimalityXsBConds
              for i in [:canonConstrs.size] do
                let c := mkApp constrsOptimalityProofs[i]! cs[i]!
                optimalityAfterCanon := mkApp optimalityAfterCanon c
              
              
              
              
              let monoArgsCount := getMonoArgsCount objCurv atomData.argKinds
              let optCondAdjusted ←
                lambdaTelescope (← whnf optimalityAfterCanon) <| fun optArgs e => do
                
                let monoArgs := optArgs[:2 * monoArgsCount]
                let optCondition ← mkLambdaFVars optArgs[2 * monoArgsCount:] e
                let atomRange ← inferType (mkAppNBeta atomData.expr xs)
                
                let newCond ←
                  if atomData.curvature == Curvature.Convex then
                    mkAppOptM ``le_trans #[
                      atomRange, none, none, none, none,
                      optCondition, objFunOptimalityProof]
                  else
                    mkAppOptM ``le_trans #[
                      atomRange, none, none, none, none,
                      objFunOptimalityProof, optCondition]
                mkLambdaFVars monoArgs newCond

instHPow in Init.Prelude

def p₂ :=
  optimization (x : ℝ)
    minimize (x)
    subject to
      c1 : 1 / 1000 ≤ x
      c2 : 1 / sqrt x ≤ exp x

let vsSol := atomData.solution.map fun s => mkAppNBeta s xs

Sum in Init.Core

def stack (ev1 ev2 : EncodedVector) : EncodedVector :=
  EncodedVector.mk (ev1.n + ev2.n) (ev1.values ++ ev2.values)

partial def mkSolEqAtom : GraphAtomDataTree → CanonExprsWithSolutionTree → VCondsTree →
    MetaM SolEqAtomProofsTree
  | Tree.node atom childAtoms,
    Tree.node _canonWithSolution childCanonWithSolution,
    Tree.node vcondVars childVCondVars => do
      
      let mut childSolEqAtom := #[]
      for i in [:childAtoms.size] do
        childSolEqAtom := childSolEqAtom.push <|
          ← mkSolEqAtom childAtoms[i]! childCanonWithSolution[i]! childVCondVars[i]!
      
      let mut solEqAtomR ← mkEqRefl atom.expr
      for c in childSolEqAtom do
        solEqAtomR ← mkCongr solEqAtomR c.val
      
      let mut vconds := #[]
      for i in [:vcondVars.size] do
        let mut vcondEqCanonVCond ← mkEqRefl atom.vconds[i]!.2
        for c in childSolEqAtom do
          vcondEqCanonVCond ← mkCongr vcondEqCanonVCond c.val
        vconds := vconds.push <| ← mkEqMPR vcondEqCanonVCond vcondVars[i]!
      
      let solEqAtomL := atom.solEqAtom
      let solEqAtomL := mkAppN solEqAtomL (childCanonWithSolution.map (·.val.1))
      let solEqAtomL := mkAppN solEqAtomL vconds
      let solEqAtom ← mkEqTrans solEqAtomL solEqAtomR
      return Tree.node solEqAtom childSolEqAtom
  | Tree.leaf e, Tree.leaf _, Tree.leaf _ => do return Tree.leaf (← mkEqRefl e)
  | _, _, _ => throwDCPError "solution-equals-atom tree mismatch."

def getVariableNameSet (domain : Expr) : m (HashSet Name) := do
  let mut res : HashSet Name := {}
  for (name, _) in ← decomposeDomain domain do
    res := res.insert name
  return res

String.Pos in Init.Data.String.Defs

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

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

instance : ToString Summary where
  toString s :=
    s!"NAME             : {s.name} \n" ++
    s!"PROBLEM STATUS   : {s.problemStatus} \n" ++
    s!"SOLUTION STATUS  : {s.solutionStatus} \n" ++
    s!"OBJECTIVE NAME   : {s.objectiveName} \n" ++
    s!"PRIMAL OBJECTIVE : {s.primalObjective} \n" ++
    s!"DUAL OBJECTIVE   : {s.dualObjective} \n"

def mkOCWithNames (objFun : Expr) (constraints : List (Name × Expr))
    (originalVarsDecls : Array LocalDecl) : MetaM (OC (Name × Expr)) := do
  withExistingLocalDecls originalVarsDecls.toList do
    let oc := OC.mk (`_, objFun) constraints.toArray
    return oc

Lean.Meta.mkFreshTypeMVar in Lean.Meta.Basic

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

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

Real.instInv in Mathlib.Data.Real.Basic

let mut lhsSubExpr ← EggString.toExpr vars params step.subexprFrom
    let mut rhsSubExpr ← EggString.toExpr vars params step.subexprTo
    lhsSubExpr ← withLocalDeclD `p D fun p => do
      Meta.withDomainLocalDecls D p fun xs prs => do
        let lhsSubExpr := Expr.replaceFVars lhsSubExpr paramsFvars paramsDeclsIds
        let lhsSubExpr := Expr.replaceFVars lhsSubExpr fvars xs
        let lhsSubExpr := Expr.replaceFVars lhsSubExpr xs prs
        mkLambdaFVars #[p] lhsSubExpr
    rhsSubExpr ← withLocalDeclD `p D fun p => do
      Meta.withDomainLocalDecls D p fun xs prs => do
        let rhsSubExpr := Expr.replaceFVars rhsSubExpr paramsFvars paramsDeclsIds
        let rhsSubExpr := Expr.replaceFVars rhsSubExpr fvars xs
        let rhsSubExpr := Expr.replaceFVars rhsSubExpr xs prs
        mkLambdaFVars #[p] rhsSubExpr

abbrev NewConstrsTree := Tree (Array Expr) Unit

Real.instNeg in Mathlib.Data.Real.Basic

mkLambdaFVars (xs ++ cs ++ bs) adjustedFeas
          oldFeasibilityAdjusted := oldFeasibilityAdjusted.push adjustedFeas

@[rel]
def trans (Rx₁ : p ≽' q) (Rx₂ : q ≽' r) : p ≽' r :=
  { phi := Rx₂.phi ∘ Rx₁.phi,
    phi_feasibility := fun x h => Rx₂.phi_feasibility (Rx₁.phi x) (Rx₁.phi_feasibility x h),
    phi_optimality := fun x hx =>
      
      have h₁ := Rx₂.phi_optimality (Rx₁.phi x) (Rx₁.phi_feasibility x hx)
      
      have h₂ := Rx₁.phi_optimality x hx
      le_trans h₁ h₂ }

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

let goalExpr ← mvarId.getType
    let mut mvarId := mvarId
    let le_lemmas := [``le_of_sub_nonneg, ``nonpos_of_neg_nonneg]
    let lt_lemmas := [``lt_of_sub_pos, ``neg_of_neg_pos]
    for (le_or_lt, lemmas) in [(``LE.le, le_lemmas), (``LT.lt, lt_lemmas)] do
      match goalExpr.app4? le_or_lt with
        | some (R, _, lhs, rhs) =>
            if !(← isDefEq R q(ℝ)) then
              continue
            if ← isDefEq lhs q(0 : ℝ) then
              continue
            let le_or_lt_lemma :=
              if ← isDefEq rhs q(0 : ℝ) then lemmas[1]! else lemmas[0]!
            if let [g] ← mvarId.applyConst le_or_lt_lemma then
              mvarId := g
              break
            else
              throwError "`prepare_positivity` failed."
        | none => continue

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

@[tactic normNumOpt]
def evalNormNumOpt : Tactic := fun stx => match stx with
  | `(tactic| norm_num_opt) => withMainContext do
      normNumOptBuilder.toTactic
      saveTacticInfoForToken stx
  | _ => throwUnsupportedSyntax

Lean.PrettyPrinter.Delaborator.DelabM in Lean.PrettyPrinter.Delaborator.Basic

inductive EggTreeOpArgTag
  | arg
  | val (s : String)

inductive ObjSense
| MAX | MIN

Fin in Init.Prelude

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

private def insertVal [BEq α] (vs : Array α) (v : α) : Array α :=
  if vs.contains v then vs else vs.push v

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

private def summaryLine (id : String) (p : Parsec α) : Parsec α :=
  summaryIdentifier id *> p <* ws' <* endOfLine

instance : Norm (m → ℝ) := PiLp.instNorm 2 _

Lean.LocalDecl in Lean.LocalContext

def SexpM.advance: SexpM Unit := do
  modify (fun state => { state with it := state.it.next })

Min.min in Init.Prelude

Prod in Init.Prelude

Matrix.IsHermitian.eigenvectorBasis in Mathlib.Analysis.Matrix.Spectrum

instance : ToMessageData Curvature where
  toMessageData
  | Curvature.Constant => "constant"
  | Curvature.Affine => "affine"
  | Curvature.Concave => "concave"
  | Curvature.Convex => "convex"
  | Curvature.AffineSet => "affine_set"
  | Curvature.ConvexSet => "convex_set"

instance [i : Fact (0 < n)] : OfNat (Fin n) 0 := ⟨⟨0, i.out⟩⟩

def toExpr (solExpr : SolutionExpr) : Expr :=
  mkApp4 (mkConst ``Minimization.Solution)
    solExpr.domain solExpr.codomain solExpr.codomainPreorder solExpr.p

let forwardMap ← makeForwardMap D originalVars pat.forwardImagesNewVars

BaseIO in Init.System.IO

let stdout ← IO.asTask eggProcess.stdout.readToEnd Task.Priority.dedicated
  let stdout : String ← IO.ofExcept stdout.get
  let exitCode ← eggProcess.wait
  dbg_trace s!"Egg exit code: {exitCode}"

def fold (oc : OC α) (init : β) (f : β → α → β) : β := Id.run do
  let b ← f init oc.objFun
  let b ← oc.constrs.foldl f b
  return b

List in Init.Prelude

Matrix.diagonal in Mathlib.Data.Matrix.Diagonal

def mkForwardImagesNewVars (canonWithSolution : OC CanonExprsWithSolutionTree) :
    MetaM Solution := do
  let canonWithSolutionTrees := #[canonWithSolution.objFun] ++ canonWithSolution.constrs
  let mut fm := #[]
  for t in canonWithSolutionTrees do
    fm := t.fold fm (fun acc a => Array.append acc a.solution)
  return fm

PiLp in Mathlib.Analysis.Normed.Lp.PiLp

MonadControlT in Init.Control.Basic

Ring in Mathlib.Algebra.Ring.Defs

def convertOpt (fullProb changeObjFun : Bool := false) (convTac : TacticM Unit) :
    EquivalenceBuilder Unit :=
  fun _ g => g.withContext do
    
    if let [gEq] ← g.apply (mkConst ``Minimization.Equivalence.ofEq) then
      
      let gToConv ← do
        if fullProb then
          markAsConvGoal gEq
        else
          
          let gs := List.filterMap id <| ← Conv.congr gEq
          if let [objFunGoal, constrsGoal] := gs then
            let gToIgnore := if changeObjFun then constrsGoal else objFunGoal
            let gToChange := if changeObjFun then objFunGoal else constrsGoal
            if let _ :: _ ← evalTacticAt (← `(tactic| rfl)) gToIgnore then
              let failureLocation := if changeObjFun then "constraints" else "objective function"
              throwConvOptError "failed to close {failureLocation} subgoals."
            else
            
            if let [gToConv] ← evalTacticAt (← `(conv| ext $(mkIdent `p))) gToChange then
              if let [gToConv] ← evalTacticAt (← `(conv| show_vars $(mkIdent `p))) gToConv then
                pure gToConv
              else
                throwConvOptError "failed to show optimization variables."
            else
              throwConvOptError "failed to introduce optimization variables."
          else
            throwConvOptError "unexpected goal type."

Lean.ToMessageData in Lean.Message

let _ ← adjustedImpConstrs.mapM check
        trace[CvxLean.debug] "adjustedImpConstrs: {adjustedImpConstrs}"

let atoms := atomsAndArgs.map (·.snd.snd.fst)
      let args := atomsAndArgs.map (·.snd.snd.snd.fst)
      let curvature := atomsAndArgs.map (·.snd.snd.snd.snd.fst)
      let bconds := atomsAndArgs.map (·.snd.snd.snd.snd.snd)

Lean.Parser.Term.bracketedBinder in Lean.Parser.Term.Basic

instance : Trans (@Equivalence D E R _) (@StrongEquivalence E F R _) (@Equivalence D F R _) :=
  { trans := fun E S => Equivalence.trans E (ofStrongEquivalence S) }

def convertFullProb (shouldEval : Bool) (stx : Syntax) : EquivalenceBuilder Unit :=
  convertOpt (fullProb := true) (changeObjFun := false) do
    if shouldEval then evalTactic stx else saveTacticInfoForToken stx

def mkProcessedAtomTree (objCurv : Curvature) (objFun : Expr) (constraints : List (Name × Expr))
    (originalVarsDecls : Array LocalDecl) (extraDecls : Array LocalDecl := #[])
    (extraVars : Array FVarId := #[]) : MetaM ProcessedAtomTree := do
  let oc ← mkOC objFun constraints originalVarsDecls
  let (failedAtom, failedAtomMsgs, atoms, args, curvature, bconds) ← mkAtomTree objCurv
    originalVarsDecls (extraDecls := extraDecls) (extraVars := extraVars) oc
  let originalConstrVars ← mkOriginalConstrVars originalVarsDecls constraints.toArray
  let (vcondIdx, isVCond, vcondVars) ← mkVConditions originalVarsDecls oc constraints atoms args
    failedAtom failedAtomMsgs originalConstrVars
  let newVars ← withExistingLocalDecls originalVarsDecls.toList do
    OC.map2MwithCounter mkNewVars atoms args
  let newVarDecls ← mkNewVarDeclList newVars
  let canonWithSolution ← withExistingLocalDecls originalVarsDecls.toList do
    OC.mapM mkCanonWithSolution atoms
  let forwardImagesNewVars ← withExistingLocalDecls originalVarsDecls.toList do
    mkForwardImagesNewVars canonWithSolution
  let solEqAtom ← mkSolEqAtomOC originalVarsDecls atoms canonWithSolution vcondVars
    originalConstrVars
  let feasibility ← mkFeasibilityOC originalVarsDecls atoms canonWithSolution bconds vcondVars
    originalConstrVars solEqAtom
  let canonExprs ← mkCanonExprsOC originalVarsDecls newVarDecls atoms newVars
  let (newConstrs, newConstrVars, newConstrVarsArray) ←
    mkNewConstrsOC originalVarsDecls newVarDecls bconds atoms newVars canonExprs
  let (optimality, vcondElimMap) ← mkOptimalityAndVCondElimOC originalVarsDecls newVarDecls
    newConstrVarsArray atoms args canonExprs newVars newConstrVars curvature bconds vcondIdx

Set in Mathlib.Data.Set.Defs

unsafe def foldMUnsafe [Monad m] (initialKeys : Array Key)
    (f : σ → Array Key → α → m σ) (init : σ) : Trie α → m σ
  | Trie.node vs children => do
    let s ← vs.foldlM (init := init) λ s v => f s initialKeys v
    children.foldlM (init := s) λ s (k, t) =>
      t.foldMUnsafe (initialKeys.push k) f s

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

structure EggDomain where
  hi : String
  lo : String
  hi_open : String
  lo_open : String

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

abbrev GraphAtomDataTree := Tree GraphAtomData Expr

HDiv in Init.Prelude

Lean.addDecl in Lean.AddDecl

structure ProcessedAtomTree where
  originalVarsDecls : Array LocalDecl
  originalConstrVars : Array LocalDecl
  newVarDecls : List LocalDecl
  newConstrs : Array Expr
  newConstrVarsArray : Array LocalDecl
  forwardImagesNewVars : Array Expr
  constraints : List (Name × Expr)
  isVCond : Array Bool
  vcondElimMap : VCondElimMap
  solEqAtom : OC SolEqAtomProofsTree
  feasibility : OC FeasibilityProofsTree
  canonExprs : OC CanonExprsTree
  optimality : OC OptimalityProofsTree
deriving Inhabited

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

def addPSDConstraintsScalarVariablesCoord (p : Problem) (i : Nat) (eml : EncodedMatrixList) :
    Problem :=
  let emll := EncodedMatrixListList.fromIndexAndEncodedMatrixList i eml
  { p with PSDConstraintsScalarVariablesCoord :=
      p.PSDConstraintsScalarVariablesCoord.stack emll }

@[command_elab «solve»]
unsafe def evalSolve : CommandElab := fun stx =>
  match stx with
  | `(solve $probInstance) =>
    liftTermElabM <| do
      let probTerm ← elabTerm probInstance.raw none
      let probTerm ← whnf probTerm
      let probTerm ← instantiateMVars probTerm

return (pd, sections)

let ocTree : OC (String × EggTree) := {
    objFun := (objFun.1, ← EggTree.adjustOps objFun.2)
    constrs := ← constr.mapIdxM <|
      
      fun i (h, c) => return (s!"{i}:" ++ h, ← EggTree.adjustOps c) }
  return (ocTree, domainConstrs)

partial def findVConditions (originalConstrVars : Array LocalDecl) (constraints : Array Expr) :
    GraphAtomDataTree → ArgumentsTree → MetaM PreVCondsTree
  | Tree.node atom childAtoms, Tree.node args childArgs => do
      let mut childrenVCondData := #[]
      for i in [:childAtoms.size] do
        let childVCondData ←
          findVConditions originalConstrVars constraints childAtoms[i]! childArgs[i]!
        childrenVCondData := childrenVCondData.push childVCondData
      let mut vcondData := #[]
      for (_, vcond) in atom.vconds do
        let vcond := mkAppNBeta vcond args

def fromIndexAndEncodedVectorEntry (i : Nat) (eve : EncodedVectorEntry) : EncodedMatrixEntry :=
  EncodedMatrixEntry.mk i eve.i eve.value

return res

structure DimensionList where
  n : Nat
  dimensions : List Nat

Matrix.PosSemidef in Mathlib.LinearAlgebra.Matrix.PosDef

OfNat in Init.Prelude

Lean.Parser.Term.binderIdent in Lean.Parser.Term.Basic

invertibleOfLeftInverse in Mathlib.Algebra.Group.Invertible.Defs

@[tactic convObj]
partial def evalConvObj : Tactic := fun stx => match stx with
  | `(tactic| conv_obj => $code) => (convertObj true code).toTactic
  
  | `(tactic| conv_obj =>) => (convertObj false stx).toTactic
  | _ => throwUnsupportedSyntax

structure RealToFloatData where
  real : Expr
  float : Expr
deriving BEq, Inhabited

abbrev VCondsIdxsTree := Tree VCondsIdxs Unit

Task.Priority in Init.Core

NNRatCast.toOfScientific in Mathlib.Algebra.Order.Ring.Unbundled.Rat

Lean.MVarId.assign in Lean.MetavarContext

let r ← IO.rand 0 (2 ^ 32 - 1)
  let outputPath := s!"solver/problem{r}.sol"
  let inputPath := s!"solver/problem{r}.cbf"
  IO.FS.writeFile inputPath ""
  IO.FS.writeFile outputPath ""
  let res : Except String SolutionData ←
    IO.FS.withFile outputPath IO.FS.Mode.read fun outHandle => do
      IO.FS.withFile inputPath IO.FS.Mode.write fun inHandle => do
        
        inHandle.putStr (ToString.toString cbf)

def addRuleToTacticEntry (rwName : String) (tac : TSyntax `tactic) (mapObjFun : Bool) :
    MetaM Unit := do
  setEnv <| ruleToTacticExt.addEntry (← getEnv) (rwName, (tac, mapObjFun))

instance [ToMessageData α] : ToMessageData (DiscrTree α) := ⟨fun dt => format dt⟩

Lean.logInfo in Lean.Log

def addEntry (ev : EncodedVector) (eve : EncodedVectorEntry) : EncodedVector :=
  if eve.value < 0 || eve.value > 0 then
    EncodedVector.mk (ev.n + 1) (ev.values.concat eve)
  else
    ev

def elabTransformationProof (transf : TransformationGoal) (lhs : Expr) (rhsName : Name)
    (stx : Syntax) : TermElabM (Expr × Expr) := do
  withRef stx do
    let syntheticMVarsSaved := (← get).syntheticMVars
    modify fun s => { s with syntheticMVars := {} }
    try
      
      let lhs := ← do
        let (n, _) := lhs.getAppFnArgs
        if n != ``Minimization.mk then
          let r ← unfold lhs n
          return r.expr
        else
          return lhs

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

for mvarId in ← getMVars lhs do
        try {
          let mvarVal ← synthInstance (← mvarId.getDecl).type
          mvarId.assign mvarVal }
        catch _ => pure ()

script EggClean := do
  let targetDir : FilePath := "." / "egg-pre-dcp" / "target"
  let utilsDir : FilePath  := "." / "egg-pre-dcp" / "utils"
  let out ←
  IO.Process.output {
    cmd := "rm"
    args := #["-rf", targetDir.toString]
  } *>
  IO.Process.output {
    cmd := "rm"
    args := #["-rf", utilsDir.toString]
  }
  pure out.exitCode

let constrBackward ← mkLambdaFVars #[p, h] constrBackwardBody
      trace[CvxLean.debug] "ψ feasibility proof: {constrBackward}."
      trace[CvxLean.debug] "ψ feasibility proof type: {← inferType constrBackward}."
      check constrBackward

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

def opMap : HashMap String (String × Array EggTreeOpArgTag) :=
  HashMap.ofList [
    ("prob",        ("prob",    #[.arg, .arg])),
    ("objFun",      ("objFun",  #[.arg])),
    ("constr",      ("constr",  #[.arg, .arg])),
    ("constrs",     ("constrs", #[])),
    ("maximizeNeg", ("neg",     #[.arg])),
    ("var",         ("var",     #[.arg])),
    ("param",       ("param",   #[.arg])),
    ("eq",          ("eq",      #[.arg, .arg])),
    ("le",          ("le",      #[.arg, .arg])),
    ("lt",          ("lt",      #[.arg, .arg])),
    ("neg",         ("neg",     #[.arg])),
    ("inv",         ("inv",     #[.arg])),
    ("oneDiv",      ("div",     #[.val "1", .arg])),
    ("abs",         ("abs",     #[.arg])),
    ("sqrt",        ("sqrt",    #[.arg])),
    ("powOne",      ("pow",     #[.arg, .val "1"])),
    ("sq",          ("pow",     #[.arg, .val "2"])),
    ("powNegOne",   ("pow",     #[.arg, .val "-1"])),
    ("powNegTwo",   ("pow",     #[.arg, .val "-2"])),
    ("log",         ("log",     #[.arg])),
    ("exp",         ("exp",     #[.arg])),
    ("xexp",        ("xexp",    #[.arg])),
    ("entr",        ("entr",    #[.arg])),
    ("min",         ("min",     #[.arg, .arg])),
    ("max",         ("max",     #[.arg, .arg])),
    ("add",         ("add",     #[.arg, .arg])),
    ("sub",         ("sub",     #[.arg, .arg])),
    ("mul",         ("mul",     #[.arg, .arg])),
    ("mul1",        ("mul",     #[.arg, .arg])),
    ("mul2",        ("mul",     #[.arg, .arg])),
    ("mul3",        ("mul",     #[.arg, .arg])),
    ("mul4",        ("mul",     #[.arg, .arg])),
    ("div",         ("div",     #[.arg, .arg])),
    ("div1",        ("div",     #[.arg, .arg])),
    ("div2",        ("div",     #[.arg, .arg])),
    ("quadOverLin", ("qol",     #[.arg, .arg])),
    ("geoMean",     ("geo",     #[.arg, .arg])),
    ("logSumExp₂",  ("lse",     #[.arg, .arg])),
    ("norm2₂",      ("norm2",   #[.arg, .arg]))
  ]

DecidablePred in Init.Prelude

Lean.mkApp in Lean.Expr

def map4M (f : α → β → γ → δ → MetaM ε) (a : OC α) (b : OC β) (c : OC γ) (d : OC δ) :
    MetaM (OC ε) := do
  let objFun ← f a.objFun b.objFun c.objFun d.objFun
  if a.constrs.size != b.constrs.size || b.constrs.size != c.constrs.size
    || c.constrs.size != d.constrs.size then
    throwError "`OC` error: could not map (4), different number of constraints."
  let mut constrs := #[]
  for i in [:a.constrs.size] do
    constrs := constrs.push <| ← f a.constrs[i]! b.constrs[i]! c.constrs[i]! d.constrs[i]!
  return OC.mk objFun constrs

instance : Inhabited ProblemData where
  default := empty

Lean.mkAppN in Lean.Expr

def toArray (t : DiscrTree α) : Array (Array Key × α) :=
  t.fold (init := #[]) λ as keys a => as.push (keys, a)

def uncheckedTreeFromMinimizationExpr (goalExprs : MinimizationExpr) : MetaM EggOCTree := do
  let (objFun, constraints, originalVarsDecls) ← withLambdaBody goalExprs.constraints
    fun p constraints => do
      let pr := (← Meta.mkProjections goalExprs.domain p).toArray
      let originalVarsDecls ←
        withLocalDeclsD (pr.map fun (n, ty, _) => (n, fun _ => return ty))
          fun xs => xs.mapM fun x => x.fvarId!.getDecl
      withExistingLocalDecls originalVarsDecls.toList do
        let xs := originalVarsDecls.map fun decl => mkFVar decl.fvarId
        let constraints ← Meta.replaceProjections constraints p.fvarId! xs
        let constraints : List (Lean.Name × Expr) ←
          Meta.decomposeConstraints constraints
        let constraints ←
          constraints.mapM (fun ((n : Lean.Name), e) => do
            return (n, ← Expr.removeMData e))
        let objFunP := goalExprs.objFun.bindingBody!.instantiate1 p
        let objFun ← Meta.replaceProjections objFunP p.fvarId! xs
        return (objFun, constraints, originalVarsDecls)

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

Lean.Meta.isDefEq in Lean.Meta.Basic

let gsFinal ← evalTacticAt (← `(tactic| equivalence_rfl)) g
  if gsFinal.length != 0 then
    throwError "`remove_trivial_constrs` error: could not close last goal."

Lean.Syntax in Init.Prelude

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

Min in Init.Prelude

structure Solution where
  point : D
  isOptimal : p.optimal point

Eq.mp in Init.Core

PiLp.instNorm in Mathlib.Analysis.Normed.Lp.PiLp

def addPSDConstraintsShiftCoord (p : Problem) (i : Nat) (em : EncodedMatrix) : Problem :=
  let eml := EncodedMatrixList.fromIndexAndEncodedMatrix i em
  { p with PSDConstraintsShiftCoord :=
      p.PSDConstraintsShiftCoord.stack eml }

def applyTransitivity (transf : TransformationGoal) (g : MVarId) : TacticM (MVarId × MVarId) :=
  g.withContext do
    if transf.isTransitive then
      let gsTrans ←
        match transf with
          | TransformationGoal.Relaxation => evalTacticAt (← `(tactic| relaxation_trans)) g
          | TransformationGoal.Reduction => evalTacticAt (← `(tactic| reduction_trans)) g
          | TransformationGoal.Equivalence => evalTacticAt (← `(tactic| equivalence_trans)) g
          | _ => pure []
      if gsTrans.length != 4 then
        throwTacticBuilderError "transitivity failed."
      let mut gToChange := gsTrans[0]!
      gToChange.setTag Name.anonymous
      let gNext := gsTrans[1]!
      gNext.setTag Name.anonymous
      return (gToChange, gNext)
    else
      return (g, g)

abbrev Arguments := Array Argument

Lean.mkApp2 in Lean.Expr

abbrev CanonExpr := Expr

def empty : Problem := {
  version := 3,
  objSense := ObjSense.MIN,
  scalarVariables := ConeProduct.empty,
  PSDVariables := DimensionList.empty,
  scalarConstraints := ConeProduct.empty,
  PSDConstraints := DimensionList.empty,
  objectivePSDVariablesCoord := EncodedMatrixList.empty,
  objectiveScalarVariablesCoord := EncodedVector.empty,
  objectiveShiftCoord := EncodedValue.empty,
  scalarConstraintsPSDVariablesCoord := EncodedMatrixListList.empty,
  scalarConstraintsScalarVariablesCoord := EncodedMatrix.empty,
  scalarConstraintsShiftCoord := EncodedVector.empty,
  PSDConstraintsScalarVariablesCoord := EncodedMatrixListList.empty,
  PSDConstraintsShiftCoord := EncodedMatrixList.empty
}

Lean.Json.str in Lean.Data.Json.Basic

Option.map in Init.Prelude

def withExpr (e : Expr) (x : m α) : m α := do
  withTheReader SubExpr (fun cfg => { cfg with expr := e, pos := cfg.pos }) x

def fromExpr (e : Expr) : MetaM RelaxationExpr := do
  match e with
  | .app (.app (.app (.app (.app (.app (.const ``Minimization.Relaxation _)
      domainP) domainQ) codomain) codomainPreorder) p) q => do
      return RelaxationExpr.mk domainP domainQ codomain codomainPreorder p q
  | _ => throwError "Expression not of the form `Minimization.Relaxation ...`."

return forwardMap

def rewriteObjBuilderWithoutTarget (shouldEval : Bool) (tacStx : Syntax) :
    EquivalenceBuilder Unit :=
  rewriteObjBuilder shouldEval tacStx none

Trans in Init.Prelude

Lean.PrettyPrinter.Delaborator.Delab in Lean.PrettyPrinter.Delaborator.Basic

Lean.Syntax.ident in Init.Prelude

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)

instance : ChangeOfVariables exp :=
  { inv := log
    condition := fun x => 0 < x
    property := fun _ hx => exp_log hx }

def Matrix.quadForm {n : ℕ} (R : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) : ℝ :=
  x ⬝ᵥ R.mulVec x

Prod.fst in Init.Prelude

Lean.Parser.Category.stx in Init.Notation

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

Zero in Init.Prelude

partial def size : EggTree → Nat
  | Tree.node "var" _ => 1
  | Tree.node _ children => 1 + (children.map size).foldl Nat.add 0
  | Tree.leaf _ => 1

let currNamespace ← getCurrNamespace
  return currNamespace ++ idStx.getId

A in examples.CircleOptimisation

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

Ring.inverse in Mathlib.Algebra.GroupWithZero.Units.Basic

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

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

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

instance : ToString EggRewrite where
  toString := EggRewrite.toString

LDL.lowerInv in Mathlib.Analysis.Matrix.LDL

Lean.Name.mkNum in Init.Prelude

Lean.mkAnd in Lean.Expr

Nonempty in Init.Prelude

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ᵀ

def makeBackwardMap (xs : Array Expr) (mkDomainFunc : Expr → MetaM Expr) : MetaM Expr := do
  let backwardBody ← foldProdMk xs
  let backwardMap ← mkDomainFunc backwardBody
  trace[CvxLean.debug] "Backward map: {backwardMap}."
  check backwardMap
  trace[CvxLean.debug] "Backward map checked."

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

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

def Sexp.toAtom! : Sexp → String
  | .atom s  => s
  | .list xs => panic! s!"expected atom, found list at {List.toString xs}"

Std.HashMap in Std.Data.HashMap.Basic

instance : ToString Constraint where
  toString c :=
    s!"{c.index} | " ++
    s!"{c.name} | " ++
    s!"{c.status} | " ++
    s!"{c.activity} | " ++
    s!"{c.lowerLimit} | " ++
    s!"{c.upperLimit} | " ++
    s!"{c.dualLower} | " ++
    s!"{c.dualUpper}"

@[inline]
def merge [BEq α] (t u : DiscrTree α) : DiscrTree α :=
  if t.root.size < u.root.size then loop t u else loop u t
  where

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

instance {ev} : Decidable (isEmpty ev) := decEq _ _

def _root_.MetaM.ofExcept [ToString ε]: Except ε α → MetaM α :=
  fun e =>
    match e with
    | Except.error msg => throwError (toString msg)
    | Except.ok x => return x

abbrev SolEqAtomProofsTree := Tree SolEqAtomProof SolEqAtomProof

Lean.mkMVar in Lean.Expr

def convertLambdasToLets (e : Expr) (args : Array Expr) : Expr := Id.run do
  let mut e := e
  let mut names := #[]
  let mut tys := #[]
  for _ in args do
    tys := tys.push e.bindingDomain!
    names := names.push e.bindingName!
    e := e.bindingBody!
  for i in [:args.size] do
    e := mkLet names[args.size - 1 - i]! tys[args.size - 1 - i]! args[args.size - 1 - i]! e
  return e

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

Lean.Elab.throwUnsupportedSyntax in Lean.Elab.Exception

def addScalarConstraintsScalarVariablesCoord (p : Problem) (i : Nat) (ev : EncodedVector) :
    Problem :=
  let em := EncodedMatrix.fromIndexAndEncodedVector i ev
  { p with scalarConstraintsScalarVariablesCoord :=
      p.scalarConstraintsScalarVariablesCoord.stack em }

Pi.basisFun in Mathlib.LinearAlgebra.StdBasis

instance : Hashable Key := ⟨Key.hash⟩

Float.mul in Init.Data.Float

private def constraintsTitle : Parsec Unit :=
  skipString "CONSTRAINTS" <* ws' <* endOfLine

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

instance : ToString ScalarConeType where
  toString
  | Zero => "Zero"
  | PosOrth => "PosOrth"
  | Exp => "Exp"
  | Q => "Q"
  | QR => "QR"

Norm.norm in Mathlib.Analysis.Normed.Group.Basic

Real.exp in Mathlib.Analysis.Complex.Exponential

PiLp.innerProductSpace in Mathlib.Analysis.InnerProductSpace.PiL2

def w := p₃.solution.2.1

instance : Trans (@Relaxation D E R _) (@Relaxation E F R _) (@Relaxation D F R _) :=
  { trans := Relaxation.trans }

Matrix.vecMul in Mathlib.Data.Matrix.Mul

def elabVars (idents : Array (TSyntax `CvxLean.Parser.minimizationVar)) :
    TermElabM (Array (Lean.Name × Expr)) := do
  let idents ← idents.concatMapM decomposeBracketedBinder
  let idents ← idents.mapM fun (id, ty) => do
    match id with
      | Syntax.ident _ _ val _ => return (val, ← Term.elabTerm ty none)
      | _ => throwParserError "expected identifier got {id}."
  return idents

let rec mkCovExpr : ℕ → ℕ → MetaM Expr
      | 0, 0 => do synthInstance (← mkAppM ``ChangeOfVariables #[changeFn])
      | 0, _ => do
          let rType := composeDomain (newVars.drop (covIdx + 1))
          mkAppOptM ``ChangeOfVariables.prod_left #[none, none, rType, changeFn, none]
      | l + 1, r => do
          let covExpr' ← mkCovExpr l r
          mkAppOptM ``ChangeOfVariables.prod_right #[none, none, mkConst ``Real, none, covExpr']
    let covExpr ← mkCovExpr covIdx (vars.length - covIdx - 1)

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

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

def fromArray (A : Array (Array (Array (Array Float)))) :
    EncodedMatrixListList := Id.run <| do
  let mut emll := empty
  for (i, ai) in A.data.enum do
    for (j, aij) in ai.data.enum do
      for (k, aijk) in aij.data.enum do
        for (l, aijkl) in aijk.data.enum do
          if k >= l && (aijkl > 0 || aijkl < 0) then
            emll := emll.addEntry (EncodedMatrixListListEntry.mk i j k l aijkl)
  return emll

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

def toExpr (redExpr : ReductionExpr) : Expr :=
  mkApp6 (mkConst ``Minimization.Reduction) redExpr.domainLHS redExpr.domainRHS redExpr.codomain
    redExpr.codomainLHSreorder redExpr.lhs redExpr.rhs

@[tactic removeConstr]
partial def evalRemoveConstr : Tactic := fun stx => match stx with
| `(tactic| remove_constr $id => $tacStx) => do
    (removeConstrBuilder id.getId (← `(term| by admit /- proof elided -/
    ))).toTactic
    saveTacticInfoForToken stx
| _ => throwUnsupportedSyntax

Lean.Elab.Command.CommandElab in Lean.Elab.Command

let arrayListExpr ← Expr.mkArray (← mkAppM ``List #[mkConst ``Real]) exprs

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 }

Float.exp in Init.Data.Float

OfNat.ofNat in Init.Prelude

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

def addEntry (em : EncodedMatrix) (eme : EncodedMatrixEntry) : EncodedMatrix :=
  if eme.value < 0 || eme.value > 0 then
    EncodedMatrix.mk (em.n + 1) (em.values.concat eme)
  else
    em

PiLp.normedAddCommGroup in Mathlib.Analysis.Normed.Lp.PiLp

Neg.neg in Init.Prelude

@[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 := #[]

partial def zip [Inhabited α] [Inhabited β] [ToMessageData α] [ToMessageData β] [ToMessageData γ]
    [ToMessageData δ] : Tree α γ → Tree β δ → MetaM (Tree (α × β) (γ × δ))
  | node val₁ children₁, node val₂ children₂ => do
      return node (val₁, val₂) (← Array.zipWithM zip children₁ children₂)
  | leaf val₁, leaf val₂ => pure <| leaf (val₁, val₂)
  | t1, t2 => throwError "zipped trees do not match {t1} {t2}"

List.toString in Init.Data.ToString.Basic

partial def getMatch (d : DiscrTree α) (e : Expr) : MetaM (Array α) := do
  Core.checkMaxHeartbeats "getMatch"
  let result := getStarResult d
  let (k, args) ← getMatchKeyArgs e (root := true)
  match k with
  | Key.star => return result
  | _        => getMatchRoot d k args result

Finset in Mathlib.Data.Finset.Defs

Matrix.toEuclideanLin in Mathlib.Analysis.InnerProductSpace.PiL2

let mut oldConstrProofs := #[]
      for i in [:originalConstrVars.size] do
        if not isVCond[i]! then
          oldConstrProofs := oldConstrProofs.push <|
            ← mkAppM ``Eq.mpr #[constraintsEq[i]!, mkFVar originalConstrVars[i]!.fvarId]

private def constraintElem (p : Parsec α) : Parsec α :=
  ws' *> p

def getAllOptimizationParams : MetaM (List Name) := do
  return (optimizationParamAttr.ext.getState (← getEnv)).toList

@[tactic dcp]
def evalDcp : Tactic := fun stx => match stx with
  | `(tactic| dcp) => do
      DCP.dcpBuilder.toTactic
      
  | _ => throwUnsupportedSyntax

def addScalarConstraint (p : Problem) (c : Cone) : Problem :=
  { p with scalarConstraints := p.scalarConstraints.addCone c }

MonadReaderOf in Init.Prelude

Matrix.det in Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Lean.LocalDecl.fvarId in Lean.LocalContext

structure Variable extends Constraint where
  conicDual : Option Float

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

def SexpM.decrementDepth: SexpM Unit :=
  modify (fun state => { state with depth := state.depth - 1 })

private def varsTitle : Parsec Unit :=
  skipString "VARIABLES" <* endOfLine

def replaceConstrName (name : Name) (e : Expr) : MetaM Expr := do
  let (_, e) ← decomposeLabel e
  return mkLabel name e

abbrev VCondIdx := Nat

def elabArgKinds (args : Array Syntax) : TermElabM (Array LocalDecl × Array ArgKind) := do
  let (argDecls, argKinds) ← elabArgKindsAux args.toList
  return (argDecls.toArray, argKinds.toArray)

x
</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 PosDef.det_ne_zero [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.PosDef) : M.det ≠ 0

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

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 PosSemidef.mul_mul_of_IsHermitian {M N : Matrix n n 𝕜} (hM : M.PosSemidef)
    (hN : N.IsHermitian) : (N * M * N).PosSemidef

theorem spectral_theorem (xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)) (as : n → ℝ)
    (hxs : ∀ j, Module.End.HasEigenvector (Matrix.toLin' A) (as j) (xs j)) :
    xs.toBasis.toMatrix (Pi.basisFun 𝕜 n) * A =
    diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix (Pi.basisFun 𝕜 n)

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 upperTriangular.toUpperTri_eq {A : Matrix n n ℝ}
    (hA : upperTriangular A) : A.toUpperTri = A

lemma log_prod_gaussianPdf {N n : ℕ} (y : Fin N → Fin n → ℝ) (R : Matrix (Fin n) (Fin n) ℝ)
    (hR : R.PosDef) : log (∏ i : Fin N, gaussianPdf R (y i)) =
    ∑ i : Fin N, (- (log (sqrt ((2 * π) ^ n)) + log (sqrt R.det)) + - R⁻¹.quadForm (y i) / 2)

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

neg_pos_of_neg in Mathlib.Algebra.Order.Group.Unbundled.Basic

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

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_eq_pow_neg_one {a : ℝ} (ha : 0 < a) : a⁻¹ = a ^ (-1 : ℝ)

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

lemma rotateSoCone_rotatedSoCone {n : ℕ} {t : ℝ} {x : Fin n.succ → ℝ} (h : soCone t x) :
    let (v, w, x) := rotateSoCone t x; rotatedSoCone v w x

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

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

lemma soCone_sub_add_two_mul_of_nonneg {x y : ℝ} (z : ℝ) :
    soCone (x - y) ![x + y, 2 * z] ↔ y ≤ x ∧ z ^ (2 : ℝ) ≤ -(x * y)

lemma IsHermitian₁₁_of_IsHermitian_toBlock {A B C D : Matrix n n ℝ}
    (h : (fromBlocks A B C D).IsHermitian) : IsHermitian A

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

@[simp]
lemma inv_lower_eq_lowerInv : (lower hS)⁻¹ = lowerInv hS

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.one_add {A : Matrix n n ℝ} (hA : A.IsHermitian) : (1 + A).IsHermitian

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

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

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

<local_ctx>
import Mathlib.LinearAlgebra.Matrix.PosDef

import Mathlib.LinearAlgebra.Matrix.Spectrum

import Mathlib.LinearAlgebra.Eigenspace.Basic

import Mathlib.LinearAlgebra.Matrix.LDL

import Mathlib.LinearAlgebra.Matrix.DotProduct

import CvxLean.Lib.Math.LinearAlgebra.Matrix.PosDef

import CvxLean.Lib.Math.LinearAlgebra.Matrix.Spectrum

import CvxLean.Lib.Math.LinearAlgebra.Eigenspace

namespace Finset

open BigOperators

end Finset

namespace Matrix

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

open BigOperators Matrix

namespace IsHermitian

variable {𝕜 : Type _} [DecidableEq 𝕜] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian)

end IsHermitian

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

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

