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>
Eq.mpr in Init.Core

instHPow in Init.Prelude

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

def exp {m} (x : m → Float) : m → Float :=
  fun i => Float.exp (x i)

Lean.mkDefinitionValEx in Lean.Declaration

def setPSDConstraintsShiftCoord (p : Problem) (eml : EncodedMatrixList) : Problem :=
  { p with PSDConstraintsShiftCoord := eml }

def removeTrivialConstrsBuilder : EquivalenceBuilder Unit := fun eqvExpr g => g.withContext do
  let lhs ← eqvExpr.toMinimizationExprLHS
  let constrNames ← withLambdaBody lhs.constraints fun _ constrsBody => do
    let cs ← decomposeConstraints constrsBody
    return cs.map fun c => c.1
  let mut g := g
  for n in constrNames do
    let eqvBuilder := removeConstrBuilder n (← `(term| (by admit /- proof elided -/
    )))
    let gs ← Tactic.run g <|
      Tactic.tryCatch eqvBuilder.toTactic (fun _ => do pure ())
    if gs.length != 1 then
      throwError "`remove_trivial_constrs` error: failed to remove {n}."
    g := gs[0]!

let canonConstrs := pat.canonExprs.constrs.map Tree.val
      let canonConstrs := canonConstrs.filterIdx (fun i => ¬ pat.isVCond[i]!)
      let canonProblem : MinimizationExpr :=
        { domain := E
          codomain := R
          objFun := ← mkDomain pat.canonExprs.objFun.val
          constraints := ← mkDomain <| Meta.composeAnd (canonConstrs ++ pat.newConstrs).toList }
      let canonProblemExpr := canonProblem.toExpr

def EggRewrite.toString (e : EggRewrite) : String :=
  "{" ++
  surroundQuotes "rewrite_name" ++ " : " ++ surroundQuotes e.rewriteName ++ ", " ++
  surroundQuotes "direction" ++ " : " ++ surroundQuotes (e.direction.toString) ++ ", " ++
  surroundQuotes "location" ++ " : " ++ surroundQuotes e.location ++ ", " ++
  surroundQuotes "subexpr_from" ++ " : " ++ surroundQuotes e.subexprFrom ++ ", " ++
  surroundQuotes "subexpr_to" ++ " : " ++ surroundQuotes e.subexprTo ++ ", " ++
  surroundQuotes "expected_term" ++ " : " ++ surroundQuotes e.expectedTerm ++
  "}"

let (gToChange, gNext) ← transf.applyTransitivity <| ← getMainGoal
  let mut gToChange := gToChange
  let mut gNext := gNext

OrderDual.toDual in Mathlib.Order.Synonym

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 mkCanonExprsOC (originalVarsDecls : Array LocalDecl) (newVarDecls : List LocalDecl)
    (atoms : OC GraphAtomDataTree) (newVars : OC NewVarsTree) : MetaM (OC CanonExprsTree) :=
  withExistingLocalDecls originalVarsDecls.toList do
    withExistingLocalDecls newVarDecls do
      let canonExprs ← OC.map2M mkCanonExprs atoms newVars
      trace[CvxLean.debug] "`canonExprs`: {canonExprs}."
      return canonExprs

NNRatCast in Mathlib.Data.Rat.Init

Lean.addAndCompile in Lean.AddDecl

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

Lean.trace in Lean.Util.Trace

Float.exp in Init.Data.Float

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

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

Lean.Core.betaReduce in Lean.Meta.Transform

Max in Init.Prelude

@[command_elab registerObjFunRuleToTactic] def elabRegisterObjFunRuleToTactic : CommandElab
| `(register_objFun_rule_to_tactic $rwName; $rwTarget => $rwGoal := $tac;) => do
    let rwNameStr := rwName.getString
    
    let _rwTargetStr := rwTarget.getString
    let _rwGoalStr := rwGoal.getString
    liftTermElabM <| addRuleToTacticEntry rwNameStr tac true
| _ => throwUnsupportedSyntax

def mkFinIdxExpr (i : Nat) (n : Nat) : MetaM Expr := do
  return mkApp2 (mkConst ``Fin.ofNat) (mkNatLit n.pred) (mkNatLit i)

partial def fold [Inhabited γ] (init : γ) (f : γ → α → γ) : Tree α β → γ
  | node val children => Id.run do
      let mut res := init
      for child in children do
        res ← fold res f child
      res := f res val
      return res
  | leaf _ => init

private def endOfLine : Parsec Unit :=
  skipChar '\u000a' <|> eof

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

let lhsMinExpr ← MinimizationExpr.fromExpr lhs
      let D := lhsMinExpr.domain
      let E ← Meta.mkFreshTypeMVar
      let R := lhsMinExpr.codomain
      let RPreorder ← Meta.mkFreshExprMVar (mkAppN (Lean.mkConst ``Preorder [levelZero]) #[R])
      let rhs ← Meta.mkFreshExprMVar (userName := rhsName)
        (mkAppN (Lean.mkConst ``Minimization) #[E, R])
      let transfTy :=
        match transf with
          | TransformationGoal.Solution =>
              mkAppN (mkConst ``Minimization.Solution) #[D, E, R, RPreorder, lhs]
          | TransformationGoal.Equivalence =>
              mkAppN (mkConst ``Minimization.Equivalence) #[D, E, R, RPreorder, lhs, rhs]
          | TransformationGoal.Reduction =>
              mkAppN (mkConst ``Minimization.Reduction) #[D, E, R, RPreorder, lhs, rhs]
          | TransformationGoal.Relaxation =>
              mkAppN (mkConst ``Minimization.Relaxation) #[D, E, R, RPreorder, lhs, rhs]

return (rhs, ← instantiateMVars proof)
    finally
      modify fun s => { s with syntheticMVars :=
        s.syntheticMVars.mergeBy (fun _ _ a => a) syntheticMVarsSaved }

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

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

def fromComponents (objFun : String × EggTree) (constr : Array (String × EggTree))
    (vars : List String) : MetaM EggOCTreeExtended := do
  let mut domainConstrs := #[]
  let mut i := 0
  for (h, c) in constr do
    
    let h := s!"{i}:" ++ h
    match processDomainExprTree h c vars with
    | some r => domainConstrs := domainConstrs.push r
    | none => pure ()
    i := i + 1

return forwardMap

Lean.mkLambda in Lean.Expr

def makeForwardMap (oldDomain : Expr) (xs : Array Expr) (forwardImagesNewVars : Array Expr) :
    MetaM Expr := do
  withLocalDeclD `p oldDomain fun p => do
    let prs := (← Meta.mkProjections oldDomain p).map (·.2.2)
    let forwardBody := xs ++ forwardImagesNewVars
    let forwardMap ← mkLambdaFVars #[p] <| (← foldProdMk forwardBody).replaceFVars xs prs.toArray
    trace[CvxLean.debug] "Forward map: {forwardMap}."
    check forwardMap
    trace[CvxLean.debug] "Forward map checked."

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

NormedAddGroup in Mathlib.Analysis.Normed.Group.Basic

instance : ToExpr Float where
  toExpr f :=
    match Json.Parser.num f.toString.mkIterator with
    | Parsec.ParseResult.success _ res =>
        let e :=
          mkApp5
            (mkConst ``OfScientific.ofScientific [levelZero])
            (mkConst ``Float)
            (mkConst ``instOfScientificFloat)
            (toExpr res.mantissa.natAbs)
            (toExpr true)
            (toExpr res.exponent)
        if res.mantissa < 0 then
          mkApp (mkConst ``Float.neg) e
        else
          e
    | Parsec.ParseResult.error _ _  =>
        mkApp (mkConst ``Float.ofNat) (toExpr (0 : Nat))
  toTypeExpr := mkConst ``Float

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

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

add in test.generate_revDeriv

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

Fin.val in Init.Prelude

IO.Process.Stdio.piped in Init.System.IO

Matrix.mulVec in Mathlib.Data.Matrix.Mul

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

LinearMap.IsSymmetric in Mathlib.Analysis.InnerProductSpace.Symmetric

def mapM (f : α → MetaM β) (oc : OC α) : MetaM (OC β) := do
  return OC.mk (← f oc.objFun) (← oc.constrs.mapM f)

def ofEggOCTree (oc : EggOCTree) : EggMinimization :=
  { objFun := EggTree.toEggString oc.objFun.2,
    constrs := Array.data <| oc.constrs.map fun (h, c) => (h, EggTree.toEggString c) }

Real.instMul in Mathlib.Data.Real.Basic

def fromIndexAndEncodedMatrixEntry (i : Nat) (eme : EncodedMatrixEntry) : EncodedMatrixListEntry :=
  EncodedMatrixListEntry.mk i eme.i eme.j eme.value

Real.instLE in Mathlib.Data.Real.Basic

Lean.Name in Init.Prelude

Matrix.IsHermitian in Mathlib.LinearAlgebra.Matrix.Hermitian

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

Matrix.vecCons in Mathlib.Data.Fin.VecNotation

@[command_elab «reduction»]
def evalReduction : 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 false
  | _ => throwUnsupportedSyntax

Min.min in Init.Prelude

Sum in Init.Core

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

Lean.Parser.checkColGe in Lean.Parser.Basic

def dcpBuilder : EquivalenceBuilder Unit := fun eqvExpr g => g.withContext do
  let ogProblem ← eqvExpr.toMinimizationExprLHS
  let (_, eqvProof) ← canonize ogProblem
  if ! (← isDefEq (mkMVar g) eqvProof) then
    throwDCPError "failed to prove equivalence."

instance : ToString EncodedVector where
  toString ev :=
    (toString ev.n) ++ "\n" ++
    (ev.values.foldl (fun acc eve => acc ++ (toString eve) ++ "\n") "")

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

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

def findRegisteredAtoms (e : Expr) : MetaM (Array (Arguments × GraphAtomData)) := do
  let discrTree ← getAtomDiscrTree
  let atoms ← discrTree.getMatch (← zetaReduce (← e.removeMData))
  trace[Meta.debug] "discrTree {atoms.size} {e}"
  let mut goodAtoms := #[]
  for atom in atoms do
    let (mvars, _, pattern) ← lambdaMetaTelescope atom.expr
    if ← isDefEq pattern e then
      let args ← mvars.mapM instantiateMVars
      goodAtoms := goodAtoms.push (args, atom.graph!)
    else
      trace[CvxLean.debug]
        "Pattern did not match. (Pattern {toString pattern}; Expression {toString e})"
  
  goodAtoms := goodAtoms.insertionSort (fun a b => (a.2.expr.size - b.2.expr.size != 0))
  return goodAtoms

let atomData := {
        id := id.getId
        curvature := curv
        expr := expr
        argKinds := argKinds
        bconds := #[]
        vconds := vconds
        impVars := impVars
        impObjFun := impObj
        impConstrs := impConstrs.map (·.snd)
        solution := sols
        solEqAtom := solEqAtom
        feasibility := feas
        optimality := opt
        vcondElim := vcondElim
      }
      return atomData

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

def _root_.Lean.Json.getArr! (j : Json) : Array Json :=
  match j with
  | Json.arr a => a
  | _ => #[]

def showVars (goal : MVarId) (p : FVarId) : MetaM MVarId := do
  
  let (revertedVars, goal) ← MVarId.withContext goal do
    let pDecl ← FVarId.getDecl p
    let fVarIds := (← getLCtx).decls.toArray.filterMap id
      |>.filter (fun decl => decl.index > pDecl.index)
      |>.map LocalDecl.fvarId
    let (_, goal) ← MVarId.revert goal fVarIds
    return (fVarIds, goal)
  
  let goal ← MVarId.withContext goal do
    let pDecl ← FVarId.getDecl p
    let domain ← instantiateMVars pDecl.type
    return ← withDomainLocalDecls domain (mkFVar p) fun xs _ => do
      let target ← instantiateMVars (← MVarId.getDecl goal).type
      let newTarget ← Meta.replaceProjections target p xs
      let mVar ← mkFreshExprMVar newTarget MetavarKind.syntheticOpaque
      MVarId.assign goal (← mkLetFVars xs mVar)
      return mVar.mvarId!
  
  let (_, goal) ← MVarId.introNP goal revertedVars.size
  return goal

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

def EggOCTree := OC (String × EggTree)

structure Summary where
  name            : String
  problemStatus   : String
  solutionStatus  : String
  objectiveName   : String
  primalObjective : Float
  dualObjective   : Float

Fintype.card in Mathlib.Data.Fintype.Card

def Vec.soCone (t : m → ℝ) (X : Matrix m n ℝ) : Prop :=
  ∀ i, Real.soCone (t i) (X i)

Eq.mp in Init.Core

instOfScientificFloat in Init.Data.OfScientific

let proof ← elabTerm stx (some transfTy)

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

def constraint : Parser :=
  leading_parser (ppLine >> checkColGe >> ppGroup (Term.binderIdent >> " : " >> termParser))

instance {α} : Inhabited (Trie α) := ⟨Trie.node #[] #[]⟩

HSMul.hSMul in Init.Prelude

def mkOptimalityAndVCondElimOC (originalVarsDecls : Array LocalDecl) (newVarDecls : List LocalDecl)
    (newConstrVarsArray : Array LocalDecl) (atoms : OC GraphAtomDataTree) (args : OC ArgumentsTree)
    (canonExprs : OC CanonExprsTree) (newVars : OC NewVarsTree)
    (newConstrVars : OC NewConstrVarsTree) (curvature : OC CurvatureTree) (bconds : OC BCondsTree)
    (vcondIdx : OC VCondsIdxsTree) : MetaM (OC OptimalityProofsTree × VCondElimMap):=
  withExistingLocalDecls originalVarsDecls.toList do
    withExistingLocalDecls newVarDecls do
      withExistingLocalDecls newConstrVarsArray.toList do
        let optimalityAndVCondElim ← OC.map7M mkOptimalityAndVCondElim atoms args canonExprs newVars
          newConstrVars curvature bconds
        let optimality := optimalityAndVCondElim.map (fun oce => oce.map Prod.fst Prod.fst)
        let vcondElim := optimalityAndVCondElim.map (fun oce => oce.map Prod.snd Prod.snd)
        trace[CvxLean.debug] "`optimality`: {optimality}."
        trace[CvxLean.debug] "`vcondElim`: {vcondElim}."
        trace[CvxLean.debug] "`vcondIdx`: {vcondIdx}."
        let vcondElimWithIdx ← OC.map2M (fun a b => Tree.zip a b) vcondIdx vcondElim
        let vcondElimMap := vcondElimWithIdx.fold {}
          fun (map : VCondElimMap) ci =>
            ci.fold map fun (map : VCondElimMap) ci => Id.run do
              let mut res := map
              for i in [:ci.1.size] do
                res := res.insert ci.1[i]! ci.2[i]!
              return res
        return (optimality, vcondElimMap)

Lean.Meta.mkAppM in Lean.Meta.AppBuilder

match transf with
    | TransformationGoal.Solution =>
        if let [eqv, sol, _, _] ← gToChange.apply (mkConst ``Minimization.Equivalence.toBwd) then
          
          gToChange := eqv
          gNext := sol
        else
          throwTacticBuilderError "could not apply equivalence tactic to `Solution`."
    | TransformationGoal.Equivalence => do
        pure ()
    | TransformationGoal.Reduction => do
        if let [eqv] ← gToChange.apply (mkConst ``Minimization.Reduction.ofEquivalence) then
          gToChange := eqv
        else
          throwTacticBuilderError "could not apply equivalence tactic to `Reduction`."
    | TransformationGoal.Relaxation => do
        throwTacticBuilderError "equivalence tactic does not apply to `Relaxation`."

Set in Mathlib.Data.Set.Defs

def renameVarsBuilder (names : Array Name) : EquivalenceBuilder Unit := fun eqvExpr g => do
  let lhsMinExpr ← eqvExpr.toMinimizationExprLHS
  let vars ← decomposeDomain (← instantiateMVars eqvExpr.domainLHS)

def addScalarValuedAffineConstraint (p : Problem) (c : Cone) (Fk : EncodedMatrixList)
    (ak : EncodedVector) (bk : Float) : Problem :=
  Id.run <| do
    let k := p.scalarConstraints.k
    let mut newP := p
    newP := newP.addScalarConstraint c
    newP := newP.addScalarConstraintsPSDVariablesCoord k Fk
    newP := newP.addScalarConstraintsScalarVariablesCoord k ak
    newP := newP.addScalarConstraintsShiftCoord k bk
    newP

Lean.MessageData in Lean.Message

private def constraintsHeaders : 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' <* endOfLine

noncomputable def klDiv (x y : Real) :=
  x * log (x / y) - x + y

@[delab app]
partial def delabMinimization : Delab := do
  
  match ← getExpr with
  | .app (.app (.app (.app (.const `Minimization.mk _) domain) _codomain) _objFun) constraints =>
      let idents ← withType <| withNaryArg 0 do
        let tys ← delabDomain
        let tys ← tys.mapM fun (name, stx) => do `(Parser.minimizationVar| ($(mkIdent name) : $stx))
        return tys.toArray
      let (objFun, isMax) ← withNaryArg 2 do withDomainBinding domain do
        match ← getExpr with
        | .app (.app (.app (.const ``maximizeNeg _) _) _) e =>
            withExpr e do
              return (← delab, true)
        | _ =>
            return (← delab, false)
      let noConstrs ← withLambdaBody constraints fun _ constrsBody => do
        isDefEq constrsBody (mkConst ``True)
      let constraints := ← withNaryArg 3 do
        let cs ← withDomainBinding domain delabConstraints
        return mkNode ``Parser.constraints #[mkNullNode <| cs.toArray.map (·.raw)]
      if noConstrs then
        if isMax then
          `(optimization $idents* maximize $objFun)
        else
          `(optimization $idents*  minimize $objFun)
      else
        if isMax then
          `(optimization $idents* maximize $objFun subject to $constraints)
        else
          `(optimization $idents* minimize $objFun subject to $constraints)
  | _ => Alternative.failure

def positivityMaybeNormNum : TacticM Unit :=
  withMainContext do
    let g ← getMainGoal
    let t : Q(Prop) ← withReducible g.getType'
    let fvs := (collectFVars {} t).fvarSet
    let tac ←
      if fvs.isEmpty then
        `(tactic| (try { norm_num } <;> positivity))
      else
        `(tactic| positivity)
    let [] ← evalTacticAt tac g | throwError "`positivity_maybe_norm_num` failed."

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

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

Eq in Init.Prelude

Matrix.BlockTriangular in Mathlib.LinearAlgebra.Matrix.Block

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

instance : ChangeOfVariables (fun x : ℝ => x⁻¹) :=
  { inv := fun x => x⁻¹
    
    
    condition := fun x => x ≠ 0
    property := fun x _ => by admit /- proof elided -/

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

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 ds := pat.newConstrVarsArray.map (mkFVar ·.fvarId)
              mkLambdaFVars (xs ++ bs ++ vs ++ zs ++ cs ++ ds) optCondAdjusted

List.get in Init.Prelude

Lean.Expr.mdata in Lean.Expr

private def summary : Parsec Summary :=
  Summary.mk <$>
  ((skipString "NAME" *> ws' *> skipChar ':' *> ws') *> pure "anonymous" <* endOfLine) <*>
  stringSummaryLine "PROBLEM STATUS"   <*>
  stringSummaryLine "SOLUTION STATUS"  <*>
  stringSummaryLine "OBJECTIVE NAME"   <*>
  floatSummaryLine  "PRIMAL OBJECTIVE" <*>
  floatSummaryLine  "DUAL OBJECTIVE"   <* ws' <* endOfLine

Max.max in Init.Prelude

def fromIndexAndEncodedMatrixList (i : Nat) (eml : EncodedMatrixList) :
    EncodedMatrixListList := Id.run <| do
  let mut emll := empty
  for emle in eml.values do
    let emlle := EncodedMatrixListListEntry.fromIndexAndEncodedMatrixList i emle
    emll := emll.addEntry emlle
  emll

def mkOfNatExpr (i : Nat) (ty : Expr) : MetaM Expr := do
  let ie := mkNatLit i
  let inst ← synthInstance (mkApp2 (mkConst ``OfNat [levelZero]) ty ie)
  return mkApp3 (mkConst ``OfNat.ofNat [levelZero]) ty ie inst

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

instance : ToMessageData RealToFloatData where
  toMessageData := fun d =>
    m!"real: {d.real}
    float: {d.float}"

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

def mkVConditions (originalVarsDecls : Array LocalDecl) (oc : OC Expr)
    (constraints : List (Name × Expr)) (atoms : OC GraphAtomDataTree) (args : OC ArgumentsTree)
    (failedAtom : OC Bool) (failedAtomMsgs : OC (Array MessageData))
    (originalConstrVars : Array LocalDecl) :
    MetaM (OC VCondsIdxsTree × Array Bool × OC VCondsTree) := do
  withExistingLocalDecls originalVarsDecls.toList do
    let vcondData ← OC.map2M (findVConditions originalConstrVars oc.constrs) atoms args

Lean.Meta.MetaM in Lean.Meta.Basic

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

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

gNext.setTag Name.anonymous
  setGoals [gNext]

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

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

withLocalDeclsD argDeclInfo fun ys => do
    f monoXs ys monoArgKind

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

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

Lean.mkAtom in Init.Prelude

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

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

Float.pow in Init.Data.Float

guard in Init.Control.Basic

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

def SexpM.matchClosingParen: SexpM Unit := do
  let state ← get
  match stackPopTillOpen state.stack with
  | some (_, stk, sexps) =>
      let sexp := Sexp.list sexps
      modify (fun state => { state with stack := stk })
      SexpM.pushSexp sexp
  | none => throw (SexpError.unmatchedCloseParen state.it)

unsafe def unrollVectors (constraints : Expr) : MetaM (Array Expr) := do
  let mut res := #[]
  let cs ← decomposeConstraints constraints
  for (_, c) in cs do
    let c' := Expr.consumeMData c
    match c' with
    
    | .app (.app (.app (.const ``Real.Vec.zeroCone _) (.app (.const ``Fin _) n)) _) e =>
        let n : Nat ← evalExpr Nat (mkConst ``Nat) n
        for i in [:n] do
          let idxExpr ← mkFinIdxExpr i n
          let ei := mkApp e idxExpr
          res := res.push (← mkAppM ``Real.zeroCone #[ei])
    
    | .app (.app (.app (.const ``Real.Vec.nonnegOrthCone _) (.app (.const ``Fin _) n)) _) e =>
        let n : Nat ← evalExpr Nat (mkConst ``Nat) n
        for i in [:n] do
          let idxExpr ← mkFinIdxExpr i n
          let ei := mkApp e idxExpr
          res := res.push (← mkAppM ``Real.nonnegOrthCone #[ei])
    
    | .app (.app (.app (.app (.app
      (.const ``Real.Vec.expCone _) (.app (.const ``Fin _) n)) _) a) b) c =>
        let n : Nat ← evalExpr Nat (mkConst ``Nat) n
        for i in [:n] do
          let idxExpr ← mkFinIdxExpr i n
          let ai := mkApp a idxExpr
          let bi := mkApp b idxExpr
          let ci := mkApp c idxExpr
          res := res.push (← mkAppM ``Real.expCone #[ai, bi, ci])
    
    | .app (.app (.app (.app (.app (.const ``Real.Vec.soCone _)
        exprN@(.app (.const ``Fin _) _n)) (.app (.const ``Fin _) m)) finTypeN) t) X =>
        let m : Nat ← evalExpr Nat (mkConst ``Nat) m
        for i in [:m] do
          let idxExpr ← mkFinIdxExpr i m
          let ti := mkApp t idxExpr
          let Xi := mkApp X idxExpr
          res := res.push (mkAppN (mkConst ``Real.soCone) #[exprN, finTypeN, ti, Xi])
    
    
    | .app (.app (.app (.app (.app (.app (.const ``Real.Vec.rotatedSoCone _)
        exprN@(.app (.const ``Fin _) _n)) (.app (.const ``Fin _) m)) finTypeN) v) w) X =>
        let m : Nat ← evalExpr Nat (mkConst ``Nat) m
        for i in [:m] do
          let idxExpr ← mkFinIdxExpr i m
          let vi := mkApp v idxExpr
          let wi := mkApp w idxExpr
          let Xi := mkApp X idxExpr
          res := res.push (mkAppN (mkConst ``Real.rotatedSoCone) #[exprN, finTypeN, vi, wi, Xi])
    | _ =>
        res := res.push c

Lean.Parser.termParser in Lean.Parser.Basic

return (objFunBackward, constrBackward)

Matrix.toBlock in Mathlib.Data.Matrix.Block

structure Constraint where
  index      : Nat
  name       : String
  status     : StatusKey
  activity   : Float
  lowerLimit : Option Float
  upperLimit : Option Float
  dualLower  : Option Float
  dualUpper  : Option Float

let (stdin, eggProcess) ← eggProcess.takeStdin
  stdin.putStr requestJson

Lean.Syntax in Init.Prelude

def isEmpty (em : EncodedMatrix) : Prop := em.n = 0

partial def mkNewVars (i : Nat) : GraphAtomDataTree → ArgumentsTree → MetaM (NewVarsTree × Nat)
  | Tree.node atom childAtoms, Tree.node args childArgs => do
      let mut childNewVars := #[]
      let mut i := i
      for k in [:childAtoms.size] do
        let (childNewVar, i') ← mkNewVars i childAtoms[k]! childArgs[k]!
        i := i'
        childNewVars := childNewVars.push $ childNewVar
      let mut newVars : Array LocalDecl := #[]
      for (n, ty) in atom.impVars do
        newVars := newVars.push <|
          LocalDecl.cdecl 0 (← mkFreshFVarId) (Name.mkNum n i) (mkAppNBeta ty args)
            Lean.BinderInfo.default LocalDeclKind.default
        i := i + 1
      return (Tree.node newVars childNewVars, i)
  | Tree.leaf _, Tree.leaf _ => pure (Tree.leaf (), i)
  | _, _ => throwDCPError "new variables tree mismatch."

Lean.ReducibilityHints.regular in Lean.Declaration

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)

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 expCone (x y z : ℝ) : Prop :=
  (0 < y ∧ y * exp (x / y) ≤ z) ∨ (y = 0 ∧ 0 ≤ z ∧ x ≤ 0)

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

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

Lean.mkStrLit in Lean.Expr

Lean.Meta.withLetDecl in Lean.Meta.Basic

partial def toEggString : EggTree → String
  | Tree.node n children =>
    let childrenStr := (children.map EggTree.toEggString).data
    "(" ++ n ++ " " ++ (" ".intercalate childrenStr) ++ ")"
  | Tree.leaf n => n

@[tactic showVars]
def evalShowVars : Tactic
  | `(tactic| show_vars $p) => do
      replaceMainGoal [← Meta.showVars (← getMainGoal) (← withMainContext do getFVarId p)]
  | _ => throwUnsupportedSyntax

abbrev VCondsIdxs := Array VCondIdx

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

abbrev VCondElimMap := Std.HashMap Nat Expr

inductive EggRewriteDirection where
  | Forward
  | Backward
deriving Inhabited, DecidableEq

let newObjFun ← withLocalDeclD `p newDomain fun p => do
    let objFunBody := mkAppNBeta lhsMinExpr.objFun #[p]
    mkLambdaFVars #[p] objFunBody
  let newConstrs ← withLocalDeclD `p newDomain fun p => do
    let objFunBody := mkAppNBeta lhsMinExpr.constraints #[p]
    mkLambdaFVars #[p] objFunBody
  let rhsMinExpr : MinimizationExpr :=
    { domain := newDomain,
      codomain := lhsMinExpr.codomain,
      objFun := newObjFun,
      constraints := newConstrs }
  if !(← isDefEq eqvExpr.rhs rhsMinExpr.toExpr) then
    throwRenameVarsError "failed to unify the goal."

def getCanonizedProblemAndBwdMap (prob : Expr) : MetaM (MinimizationExpr × Expr) := do
  let ogProb ← MinimizationExpr.fromExpr prob
  let (canonProb, eqvProof) ← DCP.canonize ogProb
  let backwardMap ← mkAppM ``Minimization.Equivalence.psi #[eqvProof]
  return (canonProb, backwardMap)

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

Lean.SimplePersistentEnvExtension in Lean.EnvExtension

Set.restrict in Mathlib.Data.Set.Restrict

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

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

let (_, mvarId) ← mvarId.assertHypotheses hyps

Lean.Expr.consumeMData in Lean.Expr

Lean.mkAppN in Lean.Expr

Equiv.sumComm in Mathlib.Logic.Equiv.Sum

def norm {n m : ℕ} (x : Fin n → Fin m → ℝ) : Fin n → ℝ :=
  fun i => ‖x i‖

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

def addExpConstraint (data : ProblemData) (a : Array Float) (b : Float) : ProblemData :=
  data.addScalarAffineConstraintOnlyVector a b ScalarConeType.Exp

Float.ofInt in Init.Data.OfScientific

abbrev BCondsTree := Tree BConds BConds

abs in Mathlib.Algebra.Order.Group.Unbundled.Abs

def w := p₃.solution.2.1

@[command_elab atomCommand] unsafe def elabAtomCommand : CommandElab
  | `(declare_atom $id [ $curv ] $args* : $expr :=
      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 (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 #[] 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 #[] impConstrs sols feas.rawImpl
      let opt ← elabOpt curv argDecls expr #[] impVars impObj impConstrs argKinds opt.raw
      let vcondElim ← elabVCondElim curv argDecls #[] vconds vcondMap impVars impConstrs argKinds
        vcondElim.rawImpl

structure Relaxation where
  phi : D → E
  phi_feasibility : ∀ x, p.feasible x → q.feasible (phi x)
  phi_optimality : ∀ x, p.feasible x → q.objFun (phi x) ≤ p.objFun x

Lean.Json.arr in Lean.Data.Json.Basic

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

def mkFeasibilityOC (originalVarsDecls : Array LocalDecl) (atoms : OC GraphAtomDataTree)
    (canonWithSolution : OC CanonExprsWithSolutionTree) (bconds : OC BCondsTree)
    (vcondVars : OC VCondsTree) (originalConstrVars : Array LocalDecl)
    (solEqAtom : OC SolEqAtomProofsTree) : MetaM (OC FeasibilityProofsTree) :=
  withExistingLocalDecls originalVarsDecls.toList do
    withExistingLocalDecls originalConstrVars.toList do
      let feasibility ← OC.map5M mkFeasibility atoms canonWithSolution bconds vcondVars solEqAtom
      trace[CvxLean.debug] "`feasibility`: {feasibility}."
      return feasibility

unsafe def exprFromSolutionData (minExpr : MinimizationExpr) (solData : SolutionData) :
    MetaM Expr := do
  let vars ← decomposeDomainInstantiating minExpr

Sum.inl in Init.Core

Lean.ReducibilityHints in Lean.Declaration

noncomputable instance LDL.invertible_diag : Invertible (LDL.diag hA) :=

partial def delabConstraints : DelabM (List (TSyntax ``Parser.constraint)) := do
  let e ← getExpr
  match e with
  | Expr.app (Expr.app (Expr.const `And _) _l) _r =>
      let l : TSyntax _ ← withNaryArg 0 delabConstraint
      let r : List (TSyntax _) ← withNaryArg 1 delabConstraints
      return l :: r
  | _ => return [← delabConstraint]

Equiv in Mathlib.Logic.Equiv.Defs

List in Init.Prelude

ε in examples.Pendulum2d

def SexpM.peek : SexpM (Option (Char × String.Pos)) := do
  let state ← get
  return if state.it.atEnd then none else some (state.it.curr, state.it.i)

Lean.Syntax.missing in Init.Prelude

Nat.add in Init.Prelude

Lean.Literal.natVal in Lean.Expr

instance : ToString EncodedMatrixList where
  toString eml :=
    (toString eml.n) ++ "\n" ++
    (eml.values.foldl (fun acc emle => acc ++ (toString emle) ++ "\n") "")

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

IO.FS.removeFile in Init.System.IO

decEq in Init.Prelude

Neg.neg in Init.Prelude

abbrev NewConstrVarsTree := Tree (Array LocalDecl) Unit

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

Real.sqrt in Mathlib.Data.Real.Sqrt

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)

@[tactic convOpt]
partial def evalConvOpt : Tactic := fun stx => match stx with
  | `(tactic| conv_opt => $code) => (convertFullProb true code).toTactic
  
  | `(tactic| conv_opt =>) => do (convertFullProb false stx).toTactic
  | _ => throwUnsupportedSyntax

HAdd in Init.Prelude

Lean.ToMessageData in Lean.Message

instance [ToMessageData α] [ToMessageData β] : ToMessageData (Tree α β) where
  toMessageData := toMessageData

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)

Lean.ToExpr in Lean.ToExpr

let responseType := (outJson.getObjValD "response").getStr!

invertibleMul in Mathlib.Algebra.Group.Invertible.Defs

let canonVars ← (originalVars ++ newVars).mapM fun x => do
        let decl ← x.fvarId!.getDecl
        return (decl.userName, decl.type)

def makeConstrForward (oldDomain : Expr) (xs : Array Expr) (originalConstrVars : Array LocalDecl)
    (oldProblem : Expr) (constraints : Array Expr) (isVCond : Array Bool)
    (constraintsEq : Array Expr) (feasibility : OC FeasibilityProofsTree) : MetaM Expr := do
  
  withLocalDeclD `p oldDomain fun p => do
    let prs := (← Meta.mkProjections oldDomain p).map (·.2.2)

String.join in Init.Data.String.Defs

instance {n} : ToExpr (Fin n) where
  toExpr x := mkApp (mkConst ``Fin.ofNat) (toExpr x.val)
  toTypeExpr := mkApp (mkConst ``Fin) (toExpr n)

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

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ᵀ

instance : ToString MatrixAffine where
  toString sa := s!"MatrixAffine [{sa.n}, {sa.H}, {sa.D}]"

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

instance : ToString EncodedMatrixEntry where
  toString eme :=
    (toString eme.i) ++ " " ++
    (toString eme.j) ++ " " ++
    (toString eme.value)

Lean.LocalDecl.cdecl in Lean.LocalContext

structure EncodedMatrixListEntry where
  i : Nat
  j : Nat
  k : Nat
  value : Float

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

target EggPreDCP (pkg) : FilePath := do
  let buildDir := pkg.dir / "egg-pre-dcp"
  let binFile := buildDir / "target" / "release" / "egg-pre-dcp"
  let dest := buildDir / "utils" / "egg-pre-dcp"
  let manifestFile := buildDir / "Cargo.toml"
  buildCargo binFile manifestFile dest #[] false

def EggRewriteDirection.toString : EggRewriteDirection → String
  | Forward => "fwd"
  | Backward => "bwd"

Lean.Literal in Lean.Expr

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

ToString.toString in Init.Data.ToString.Basic

target EggPreDCPStopOnSuccess (pkg) : FilePath := do
  let buildDir := pkg.dir / "egg-pre-dcp"
  let binFile := buildDir / "target" / "release" / "egg-pre-dcp"
  let dest := buildDir / "utils" / "egg-pre-dcp"
  let manifestFile := buildDir / "Cargo.toml"
  buildCargo binFile manifestFile dest #[] true

Lean.Expr.app in Lean.Expr

Real.rpow in Mathlib.Analysis.SpecialFunctions.Pow.Real

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

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

Matrix.blockDiagonal in Mathlib.Data.Matrix.Block

private def summaryIdentifier (id : String) : Parsec Unit :=
  skipString id *> ws' *> skipChar ':' *> ws'

abbrev AtomDataTrees := GraphAtomDataTree × ArgumentsTree × CurvatureTree × BCondsTree

def stack (eml1 eml2 : EncodedMatrixList) : EncodedMatrixList :=
  EncodedMatrixList.mk (eml1.n + eml2.n) (eml1.values ++ eml2.values)

def addRotatedSOConstraint (data : ProblemData) (a : Array Float) (b : Float) : ProblemData :=
  data.addScalarAffineConstraintOnlyVector a b ScalarConeType.QR

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

let gs ← getUnsolvedGoals
    if gs.length != 0 then
      throwError "`remove_constr` error: failed to close all goals."

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

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

liftM in Init.Prelude

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

instance : Hashable Key := ⟨Key.hash⟩

Sum.inr in Init.Core

IsGreatest in Mathlib.Order.Bounds.Defs

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

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

instance : ToString ConeProduct where
  toString cp :=
    (toString cp.n) ++ " " ++ (toString cp.k) ++ "\n" ++
    (cp.cones.foldl (fun acc c => acc ++ (toString c) ++ "\n") "")

HDiv.hDiv in Init.Prelude

Lean.Parser.ppSpace in Lean.Parser.Extra

let atomData ← addAtomDataDecls id.getId atomData

Lean.Parser.Category.tactic in Init.Notation

Array.toList in Init.Prelude

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

Lean.Json.getArr? in Lean.Data.Json.Basic

def runTransformationTactic (transf : TransformationGoal) (mvarId : MVarId) (stx : Syntax) :
    TermElabM Unit := do
  let tacticStx := ⟨stx[1]⟩
  let rflTacticStx ←
    match transf with
      | TransformationGoal.Solution => `(tactic| skip)
      | TransformationGoal.Equivalence => `(tactic| equivalence_rfl)
      | TransformationGoal.Reduction => `(tactic| reduction_rfl)
      | TransformationGoal.Relaxation => `(tactic| relaxation_rfl)
  let code ← `(tactic| $tacticStx <;> $rflTacticStx)

@[rel]
def refl : p ≽' p :=
  { phi := id,
    phi_feasibility := fun _ h => h,
    phi_optimality := fun _ _ => le_refl _ }

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

def h := p₃.solution.1

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 getAllOptimizationParams : MetaM (List Name) := do
  return (optimizationParamAttr.ext.getState (← getEnv)).toList

abbrev Solution := Array NewVarAssignment

noncomputable def entr (x : Real) :=
  -(x * log x)

unsafe def evalFloat (e : Expr) : MetaM Float := do
  evalExpr Float (mkConst ``Float) e

inductive SexpError
  | unmatchedOpenParen (ix: String.Iterator) : SexpError
  | unmatchedCloseParen (ix: String.Iterator) : SexpError
  | notSingleSexp (s: String) (xs: List Sexp) : SexpError
  deriving BEq, Repr

List.cons in Init.Prelude

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

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

structure Problem where
  version : Nat
  objSense : ObjSense
  scalarVariables : ConeProduct
  PSDVariables : DimensionList
  scalarConstraints : ConeProduct
  PSDConstraints : DimensionList
  objectivePSDVariablesCoord : EncodedMatrixList
  objectiveScalarVariablesCoord : EncodedVector
  objectiveShiftCoord : EncodedValue
  scalarConstraintsPSDVariablesCoord : EncodedMatrixListList
  scalarConstraintsScalarVariablesCoord : EncodedMatrix
  scalarConstraintsShiftCoord : EncodedVector
  PSDConstraintsScalarVariablesCoord : EncodedMatrixListList
  PSDConstraintsShiftCoord : EncodedMatrixList

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

def cleanUpCompBuilder : EquivalenceBuilder Unit := fun eqvExpr g => g.withContext do
  let lhsMinExpr ← eqvExpr.toMinimizationExprLHS
  let newObjFun ← cleanUpCompAux lhsMinExpr.objFun "objFun"
  let newConstraints ← cleanUpCompAux lhsMinExpr.constraints "constr"
  let rhsMinExpr := { lhsMinExpr with objFun := newObjFun, constraints := newConstraints }
  let newEqvExpr := { eqvExpr with lhs := lhsMinExpr.toExpr, rhs := rhsMinExpr.toExpr }
  if (← isDefEq (mkMVar g) newEqvExpr.toExpr) then
    throwError "`clean_up_comp` error: Failed to unify the goal."
  let simpComp ← ({} : SimpTheorems).addDeclToUnfold ``Function.comp
  let simpContext := { config := {}, simpTheorems := #[simpComp] }
  if let (some newGoal, _) ← simpTarget g simpContext then
    if let _ :: _ ← evalTacticAt (← `(tactic| equivalence_rfl)) newGoal then
      throwError "`clean_up_comp` error: Failed to close the goal."

abbrev SolEqAtomProofsTree := Tree SolEqAtomProof SolEqAtomProof

@[equiv]
def ofReductions (R₁ : p ≼ q) (R₂ : q ≼ p) : p ≡ q :=
  { phi := R₂.psi,
    psi := R₁.psi,
    phi_optimality := R₂.psi_optimality,
    psi_optimality := R₁.psi_optimality }

@[red]
noncomputable def map_objFun_log {f : D → ℝ} (h : ∀ x, cs x → f x > 0) :
    ⟨f, cs⟩ ≼ ⟨fun x => (Real.log (f x)), cs⟩ :=
  ofEquivalence <| Equivalence.map_objFun_log h

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

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

return constrForward

Lean.Meta.inferType in Lean.Meta.Basic

Lean.Name.quickLt in Lean.Data.Name

Lean.Core.transform in Lean.Meta.Transform

abbrev Argument := Expr

Except.error in Init.Prelude

Array.empty in Init.Prelude
</all_available_defs>

<all_available_lemmas>
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 upperTriangular_toUpperTri {m : Type _} [LinearOrder m]
    (A : Matrix m m ℝ) : A.toUpperTri.upperTriangular

lemma PosSemidef₂₂_of_PosSemidef_toBlock {A B C D : Matrix n n ℝ}
    (h : (fromBlocks A B C D).PosSemidef) :
    PosSemidef D

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

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

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

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

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

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

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

lemma PosSemidef.add {M N : Matrix n n 𝕜} (hM : M.PosSemidef) (hN : N.PosSemidef) :
    (M + N).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 lowerTriangular_inv_of_lowerTriangular [Fintype m] [LinearOrder m]
    [Invertible M] (hM : lowerTriangular M) : lowerTriangular M⁻¹

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 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 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 LDL.diagEntries_pos {A : Matrix n n ℝ} (hA: A.PosDef) (i : n) :
    0 < LDL.diagEntries hA i

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

lemma unrotateSoCone_soCone {n : ℕ} {v w : ℝ} {x : Fin n → ℝ} (h : rotatedSoCone v w x) :
    let (t, x) := unrotateSoCone v w x; soCone t x

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

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

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

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

theorem vecCons_zero_zero {n} [Zero α] : vecCons (0 : α) (0 : Fin n → α) = 0

neg_nonneg_of_nonpos in Mathlib.Algebra.Order.Group.Defs

lemma le_div_iff (hc : StrongLT 0 c) : a ≤ b / c ↔ a * c ≤ b
</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>
@[simp]
lemma PosSemidef.sqrt_mul_sqrt {A : Matrix n n ℝ} (hA : A.PosSemidef) :
    hA.1.sqrt * hA.1.sqrt = A :=
</target_theorem>

