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)

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

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

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

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

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

def toArray (x : Fin n → Float) : Array Float :=
  (Array.range n).map (fun i => if h : i < n then x ⟨i, h⟩ else 0)

Lean.PrettyPrinter.Delaborator.failure in Lean.PrettyPrinter.Delaborator.Basic

Float.neg in Init.Data.Float

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 isConstant (e : Expr) : Bool := (Lean.collectFVars {} e).fvarSet.isEmpty

RCLike.ofReal in Mathlib.Analysis.RCLike.Basic

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

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

Prod in Init.Prelude

instance : ToString EggRewrite where
  toString := EggRewrite.toString

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

Lean.Declaration.defnDecl in Lean.Declaration

def getRegisteredRewriteNames : MetaM (List String) := do
  return (ruleToTacticExt.getState (← getEnv)).toList.map (·.1)

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

Real.instMul in Mathlib.Data.Real.Basic

RCLike in Mathlib.Analysis.RCLike.Basic

partial def delabDomain : DelabM (List (Lean.Name × Term)) := do
  let e ← getExpr
  match e with
  | Expr.app (Expr.app (Expr.const `Prod _) _ty1) _ty2 => do
      let stx1 ← withNaryArg 0 (do delabVar <| e.getArg! 0)
      let stx2 ← withNaryArg 1 (do delabDomain)
      return stx1 :: stx2
  | _ => return [← delabVar e]

Lean.Meta.mkFreshTypeMVar in Lean.Meta.Basic

Option.map₂ in Mathlib.Data.Option.NAry

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)

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

Real.instAdd in Mathlib.Data.Real.Basic

def fromGoal (goal : MVarId) : MetaM ReductionExpr := do
  let goalType ← whnf (← MVarId.getDecl goal).type
  fromExpr goalType

unsafe def generateBasisOfShape (ty : Expr) : MetaM (Array Expr × Array Expr) :=
  match ty.consumeMData with
  
  | .const ``Float _ =>
      return (#[], #[mkFloat 1])
  
  | .forallE _ tyn (.const ``Float _) _ => do
      let mut res := #[]
      for i in ← elemsOfFintype tyn do
        let b ← withLocalDeclD `i' tyn fun i' => do
          let ite ← mkAppM ``ite #[← mkEq i' i, mkFloat 1, mkFloat 0]
          mkLambdaFVars #[i'] ite
        res := res.push b
      return (#[], res)
  
  | .app (.app (.app (.const ``Matrix _) tyn) tym) (.const ``Float _)  => do
      let mut res := #[]
      let elemsn ← elemsOfFintype tyn
      for i in elemsn do
        for j in ← elemsOfFintype tym do
          let b ← withLocalDeclD `i' tyn fun i' => do
            withLocalDeclD `j' tym fun j' => do
              let ite ← mkAppM ``ite #[mkAnd (← mkEq i' i) (← mkEq j' j), mkFloat 1, mkFloat 0]
              mkLambdaFVars #[i', j'] ite
          res := res.push b

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

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

LDL.diag in Mathlib.Analysis.Matrix.LDL

inductive ScalarConeType
  | Zero | PosOrth | Exp | Q | QR

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

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

-- solve p₂

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)

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

@[equiv]
def rewrite_constraint_3 (hrw : ∀ x, c1 x → c2 x → cs x → (c3 x ↔ c3' x)) :
    ⟨f, [[c1, c2, c3, cs]]⟩ ≡ ⟨f, [[c1, c2, c3', cs]]⟩ :=
  equivalence_of_rw_constr hrw

def makeObjFunForward (oldDomain : Expr) (xs : Array Expr) (originalConstrVars : Array LocalDecl)
    (oldProblem : Expr) (constraints : Array Expr) (objFunEq : Expr) : MetaM Expr := do
  
  withLocalDeclD `p oldDomain fun p => do
    let prs := (← Meta.mkProjections oldDomain p).map (·.2.2)

inductive ArgKind where
  | Increasing | Decreasing | Neither | Constant
deriving BEq, Inhabited

Set.restrict in Mathlib.Data.Set.Restrict

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

@[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.Syntax.atom in Init.Prelude

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

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

Fact in Mathlib.Logic.Basic

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

Sum.elim in Init.Data.Sum.Basic

noncomputable instance instMinReal : Min ℝ :=

Matrix.toBlock in Mathlib.Data.Matrix.Block

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

def preparePositivity (mvarId : MVarId) : MetaM MVarId := do
  mvarId.withContext do
    
    let mut hyps := #[]
    let le_lemmas := [``sub_nonneg_of_le, ``neg_nonneg_of_nonpos]
    let lt_lemmas := [``sub_pos_of_lt, ``neg_pos_of_neg]
    let mut lctx ← getLCtx
    for localDecl in lctx do
      let ty := localDecl.type
      for (le_or_lt, lemmas) in [(``LE.le, le_lemmas), (``LT.lt, lt_lemmas)] do
        let ty := Expr.consumeMData ty
        match ty.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]!
            
            let val ← mkAppM le_or_lt_lemma #[localDecl.toExpr]
            let ty ← inferType val
            let n := localDecl.userName
            hyps := hyps.push (Hypothesis.mk n ty val)
        | none => continue

instHAdd in Init.Prelude

def addEntry (eml : EncodedMatrixList) (emle : EncodedMatrixListEntry) : EncodedMatrixList :=
  if emle.value > 0 || emle.value < 0 then
    EncodedMatrixList.mk (eml.n + 1) (eml.values.concat emle)
  else
    eml

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

Lean.mkLambda in Lean.Expr

Lean.FVarId in Lean.Expr

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

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

L in Archive.Hairer

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

Real.instLE in Mathlib.Data.Real.Basic

Lean.mkSort in Lean.Expr

let rhs ← instantiateMVars rhs
      let rhs ← mkLambdaFVars (xs.map Prod.snd) rhs
      let rhs ← instantiateMVars rhs
      simpleAddDefn probId rhs

Lean.mkProj in Lean.Expr

inductive Sexp
  | atom : String → Sexp
  | list : List Sexp → Sexp
  deriving BEq, Inhabited, Repr

def fromIndexAndValue (i : Nat) (v : Float) : EncodedVector :=
  if v > 0 || v < 0 then
    EncodedVector.mk 1 [EncodedVectorEntry.fromIndexAndValue i v]
  else
    EncodedVector.mk 0 []

@[command_elab «equivalence»]
def evalEquivalence : CommandElab := fun stx => match stx with
  | `(equivalence $eqvId / $probId $declSig := $proofStx) => do
      liftTermElabM do
        let (binders, lhsStx) := expandDeclSig declSig.raw
        elabBindersEx binders.getArgs fun xs =>
          evalEquivalenceAux probId eqvId xs lhsStx proofStx false
  | _ => throwUnsupportedSyntax

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

inductive FindAtomResult
  | Success (res : AtomDataTrees)
  | Error (msgs : Array MessageData)

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

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_.MetaM.ofExcept [ToString ε]: Except ε α → MetaM α :=
  fun e =>
    match e with
    | Except.error msg => throwError (toString msg)
    | Except.ok x => return x

def findTactic (rewriteName : String) (direction : EggRewriteDirection) :
    MetaM (TSyntax `tactic × Bool) := do
  match ← getTacticFromRewriteName rewriteName with
  | some (tac, mapObjFun) =>
    if mapObjFun then
      return (tac, true)
    else
      match direction with
      | EggRewriteDirection.Forward => return (tac, false)
      | EggRewriteDirection.Backward =>
          
          return (← `(tactic| (symm; $tac)), false)
  | _ => throwPreDCPError "unknown rewrite name {rewriteName}({direction})."

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

structure EggRequest where
  probName : String
  domains : List (String × EggDomain)
  target : EggMinimization

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

instance : ToString ObjSense where
  toString
  | MAX => "MAX"
  | MIN => "MIN"

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

MonadWithReaderOf in Init.Prelude

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

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 toMinimizationExprLHS (redExpr : ReductionExpr) : MetaM MinimizationExpr :=
  MinimizationExpr.fromExpr redExpr.lhs

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

Lean.MessageData.group in Lean.Message

g in examples.Pendulum2d

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

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

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

Matrix.BlockTriangular in Mathlib.LinearAlgebra.Matrix.Block

@[command_elab «relaxation»]
def evalRelaxation : CommandElab := fun stx => match stx with
| `(relaxation $relIdStx / $probIdStx $declSig := $proofStx) => do
  liftTermElabM do
    let (binders, lhsStx) := expandDeclSig declSig.raw
    elabBindersEx binders.getArgs fun xs => do
      let D ← Meta.mkFreshTypeMVar
      let R ← Meta.mkFreshTypeMVar
      let lhsTy := mkApp2 (Lean.mkConst ``Minimization) D R
      let lhs ← elabTermAndSynthesizeEnsuringType lhsStx (some lhsTy)

unsafe def elemsOfFintype (ty : Expr) : MetaM (Array Expr) := do
  match ty with
  | .app (.const ``Fin _) nExpr => do
    let n : Nat ← evalExpr Nat (mkConst ``Nat) nExpr
    let mut res := #[]
    for i in [:n] do
      res := res.push (← mkFinIdxExpr i n)
    return res
  | .app (.app (.const ``Sum lvl) tyl) tyr => do
    let elemsl := (← elemsOfFintype tyl).map fun e =>
      mkAppN (mkConst ``Sum.inl lvl) #[tyl, tyr, e]
    let elemsr := (← elemsOfFintype tyr).map fun e =>
      mkAppN (mkConst ``Sum.inr lvl) #[tyl, tyr, e]
    return elemsl ++ elemsr
  | _ => throwCoeffsError "unsupported finite type ({ty})."

Lean.levelOne in Lean.Level

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

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

-- set_option trace.Meta.debug true

def unrotateSoCone {n : ℕ} (v w : Real) (x : Fin n → ℝ) : ℝ × (Fin n.succ → ℝ) :=
  ((v + w) / sqrt 2, Matrix.vecCons ((v - w) / sqrt 2) x)

abbrev GraphAtomDataTree := Tree GraphAtomData Expr

x in doc.literate.literate_lean_test

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

decEq in Init.Prelude

point in examples.CircleOptimisation

def toMinimizationExprRHS (relExpr : RelaxationExpr) : MetaM MinimizationExpr :=
  MinimizationExpr.fromExpr relExpr.q

let lhsMinExpr ← eqvExpr.toMinimizationExprLHS
    let vars ← decomposeDomain (← instantiateMVars lhsMinExpr.domain)

let constrForwardBody ← foldAndIntro (oldConstrProofs ++ newConstrProofs)
      let constrForwardBody := constrForwardBody.replaceFVars
        ((originalConstrVars).map (mkFVar ·.fvarId)) hProj
      let constrForwardBody ← mkLambdaFVars #[h] constrForwardBody
      let constrForwardBody := constrForwardBody.replaceFVars xs prs.toArray
      let constrForward ← mkLambdaFVars #[p] constrForwardBody
      trace[CvxLean.debug] "φ feasibility proof: {constrForward}."
      trace[CvxLean.debug] "φ feasibility proof type: {← inferType constrForward}."
      check constrForward

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

Lean.FVarId.getDecl in Lean.Meta.Basic

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

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

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

return (#[], res)
  
  | .app (.app (.const ``Prod _) tyl) tyr => do
      let r₀ ← generateZerosOfShape tyr
      let l₀ ← generateZerosOfShape tyl

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

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

if let _ :: _ ← g.apply fullProof then
      throwError "`remove_constr` error: failed to prove equivalence."

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

Prod.fst in Init.Prelude

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

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

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

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

def shiftingArgs (curv : Curvature) (xs : Array Expr) (argKinds : Array ArgKind)
    (mkConcl : Array Expr → Array Expr → TermElabM Expr) : TermElabM Expr :=
  withCopyOfMonoXs xs argKinds fun monoXs ys monoArgKind => do
    let mut ty := ← mkConcl monoXs ys
    for i' in [:monoXs.size] do
      let i := monoXs.size - 1 - i'
      ty ← match curvatureInArg curv monoArgKind[i]! with
      | Curvature.Concave => mkArrow (← mkLe monoXs[i]! ys[i]!) ty
      | Curvature.Convex => mkArrow (← mkLe ys[i]! monoXs[i]!) ty
      | Curvature.ConvexSet => mkArrow (← mkLe monoXs[i]! ys[i]!) ty
      | _ => throwAtomDeclarationError "invalid curvature"
    return ← mkForallFVars ys ty

def SexpState.fromString (s : String) : SexpState where
  it := s.iter

def removeConstrBuilder (id : Name) (proof : Syntax) : EquivalenceBuilder Unit := fun eqvExpr g =>
  g.withContext do
    let lhsMinExpr ← eqvExpr.toMinimizationExprLHS
    let (idxToRemove, numConstrs, newConstrs, toShow) ←
      withLambdaBody lhsMinExpr.constraints fun p oldConstrsBody => do
        let oldConstrsList ← decomposeConstraints oldConstrsBody
        let idxToRemove := oldConstrsList.findIdx fun c => c.1 == id
        if idxToRemove == oldConstrsList.length then
          throwError "`remove_constr` error: constraint {id} not found."
        let newConstrsList := oldConstrsList.eraseIdx idxToRemove
        let newConstrs ← mkLambdaFVars #[p] <| composeAnd <| newConstrsList.map Prod.snd
        
        let lhsLabeledDomain ← decomposeDomain lhsMinExpr.domain
        let toShow ← withLocalDeclsDNondep lhsLabeledDomain.toArray fun xs => do
          mkLambdaFVars xs <| ← do
            let niceNewConstrsList ← newConstrsList.mapM (fun (n, c) => do
              return (n, ← replaceProjections c p.fvarId! xs))
            let toErase := (oldConstrsList.get! idxToRemove).2;
            let niceToErase ← Meta.replaceProjections toErase p.fvarId! xs
            withLocalDeclsDNondep niceNewConstrsList.toArray fun cs => do
              let (e, _) ← Lean.Elab.Term.TermElabM.run <| Lean.Elab.Term.commitIfNoErrors? <| do
                let v ← Lean.Elab.Term.elabTerm proof niceToErase
                Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
                instantiateMVars v
              if let some e' := e then
                mkLambdaFVars cs e'
              else
                throwError "`remove_constr` error: failed to elaborate proof."
        return (idxToRemove, oldConstrsList.length, newConstrs, toShow)

Real.exp in Mathlib.Analysis.Complex.Exponential

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

Lean.collectFVars in Lean.Util.CollectFVars

Id.run in Init.Control.Id

HAdd.hAdd in Init.Prelude

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

let (constraintsData, sections) ←
    withLambdaBody minExpr.constraints fun p constraints => do
    let mut data : ProblemData := ProblemData.empty
    let mut sections := #[]

Module in Mathlib.Algebra.Module.Defs

IO.FS.withFile in Init.System.IO

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

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

Lean.withRef in Init.Prelude

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

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

Finset in Mathlib.Data.Finset.Defs

def floatToReal (f : Float) : Expr :=
  let nnRatCastToOfScientific :=
    mkApp2 (mkConst ``NNRatCast.toOfScientific ([levelZero] : List Level))
      (mkConst ``Real) (mkConst ``Real.instNNRatCast)
  let realOfScientific :=
    mkApp2 (mkConst ``OfScientific.ofScientific ([levelZero] : List Level))
      (mkConst ``Real) nnRatCastToOfScientific
  match Json.Parser.num f.toString.mkIterator with
  | Parsec.ParseResult.success _ res =>
      let num := mkApp3 realOfScientific
        (mkNatLit res.mantissa.natAbs) (toExpr true) (mkNatLit res.exponent)
      if res.mantissa < 0 then
        mkApp3 (mkConst ``Neg.neg ([levelZero] : List Level))
          (mkConst ``Real) (mkConst ``Real.instNeg) num
      else num
  
  | Parsec.ParseResult.error _ _ =>
      mkApp3 realOfScientific
        (mkNatLit 0) (toExpr true) (mkNatLit 1)

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)

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"

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

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

Lean.TransformStep.continue in Lean.Meta.Transform

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

def evalStep (step : EggRewrite) (vars params : List Name) (paramsDecls : List LocalDecl)
    (tagsMap : HashMap String ℕ) : EquivalenceBuilder Unit := fun eqvExpr g => g.withContext do
  let tag ← liftMetaM <| do
    if step.location == "objFun" then
      return "objFun"
    else if let [_, tag] := step.location.splitOn ":" then
      return tag
    else
      throwPreDCPError "unexpected tag name {step.location}."
  let tagNum := tagsMap.find! step.location
  let atObjFun := tagNum == 0

abbrev VCondsIdxsTree := Tree VCondsIdxs Unit

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

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

Finsupp in Mathlib.Data.Finsupp.Defs

def preElabConstraints (constraints : TSyntax `CvxLean.Parser.constraints) :
    TermElabM (Array (Lean.Name × TSyntax `term)) := do
  match constraints with
  | `(CvxLean.Parser.constraints| $constrs*) => do
      constrs.mapM fun cDecl =>
        match cDecl with
          | `(CvxLean.Parser.constraint| $id:ident : $c) => return (id.getId, c)
          | `(CvxLean.Parser.constraint| _ : $c) => return (Name.anonymous, c)
          | _ => throwParserError "expected constraint got {cDecl}."
  | _ => throwParserError "expected constraints got {constraints}."

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

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

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

LE.le in Init.Prelude

OrderDual.toDual in Mathlib.Order.Synonym

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

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

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

Nat.add in Init.Prelude

Lean.MVarId.getDecl in Lean.Meta.Basic

Matrix.vecCons in Mathlib.Data.Fin.VecNotation

def mkAndIntro (xs : Array Expr) : MetaM Expr := do
  let mut res := xs[xs.size - 1]!
  for i in [:xs.size - 1] do
    res ← mkAppM ``And.intro #[xs[xs.size - 2 - i]!, res]
  return res

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

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

Fin.ofNat in Init.Data.Fin.Basic

abbrev AtomDataTrees := GraphAtomDataTree × ArgumentsTree × CurvatureTree × BCondsTree

instance ChangeOfVariables.id {D} : ChangeOfVariables (fun x : D => x) :=
  { inv := fun x => x
    condition := fun _ => True
    property := fun _ _ => rfl }

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

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

EuclideanSpace in Mathlib.Analysis.InnerProductSpace.PiL2

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

def withBindingBody'' {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m]
    [MonadWithReaderOf SubExpr m] [MonadControlT MetaM m] (n : Name) (x : Expr → m α) : m α := do
  let e ← getExpr
  Meta.withLocalDecl n e.binderInfo e.bindingDomain! fun fvar =>
    descend (e.bindingBody!.instantiate1 fvar) 1 (x fvar)

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

Lean.addDecl in Lean.AddDecl

Float.ofScientific in Init.Data.OfScientific

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

def Vec.rotatedSoCone (v w : m → ℝ) (X : Matrix m n ℝ) : Prop :=
  ∀ i, Real.rotatedSoCone (v i) (w i) (X i)

Lean.mkApp in Lean.Expr

And in Init.Prelude

Lean.LocalDeclKind.default in Lean.LocalContext

Unique in Mathlib.Logic.Unique

Matrix.diagonal in Mathlib.Data.Matrix.Diagonal

inductive SexpTok
  | sexp : Sexp →  SexpTok
  | opening : String.Pos → SexpTok
  deriving BEq, Inhabited, Repr

Lean.Expr.mdata in Lean.Expr

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

Alternative.failure in Init.Control.Basic

Lean.Meta.mkAppOptM in Lean.Meta.AppBuilder

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

Matrix.fromBlocks in Mathlib.Data.Matrix.Block

abbrev NewConstrsTree := Tree (Array Expr) 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

Lean.BinderInfo.default in Lean.Expr

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

@[tactic convConstr]
partial def evalConvConstr : Tactic := fun stx => match stx with
  | `(tactic| conv_constr => $code) => (convertConstrs true code).toTactic
  | `(tactic| conv_constr $h => $code) => (convertConstrWithName true code h.getId).toTactic
  
  | `(tactic| conv_constr =>) => (convertConstrs false stx).toTactic
  | `(tactic| conv_constr $h =>) => (convertConstrWithName false stx h.getId).toTactic
  | _ => throwUnsupportedSyntax

Lean.Core.checkMaxHeartbeats in Lean.CoreM

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

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

Matrix.diag in Mathlib.Data.Matrix.Diagonal

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

LinearMap in Mathlib.Algebra.Module.LinearMap.Defs

Subtype in Init.Prelude

let objFunForward ← mkAppM ``le_of_eq #[objFunEq.replaceFVars xs prs.toArray]

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

withLocalDeclsD argDeclInfo fun ys => do
    f monoXs ys monoArgKind

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 setObjectiveOnlyVector (data : ProblemData) (a : Array Float) (b : Float) : ProblemData :=
  data.setObjective #[] a b

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

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

Sum in Init.Core

def isEmpty (eml : EncodedMatrixList) : Prop := eml.n = 0

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

instance : ToString EggRewriteDirection where
  toString := EggRewriteDirection.toString

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

AddCommMonoid in Mathlib.Algebra.Group.Defs

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

Lean.Elab.Tactic.saveTacticInfoForToken in Lean.Elab.Tactic.Basic

Decidable in Init.Prelude

let newConstrProofs := feasibility.fold #[] fun acc fs =>
          fs.fold acc Array.append

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

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

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

abbrev NewVarsTree := Tree (Array LocalDecl) Unit

structure EncodedMatrixListList where
  n : Nat
  values : List EncodedMatrixListListEntry

def RuleToTacticExt : Type :=
  SimplePersistentEnvExtension RuleToTacticExtEntry RuleToTacticExtState
deriving Inhabited

let currNamespace ← getCurrNamespace
  return currNamespace ++ idStx.getId

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

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

Except in Init.Prelude

def _root_.Real.Computable.norm {n : ℕ} (x : Fin n → Float) : Float :=
  Float.sqrt (sum (fun i => (Float.pow (x i) 2)))

instance : Hashable Key := ⟨Key.hash⟩

IO.FS.writeFile in Init.System.IO

Lean.mkStrLit in Lean.Expr

instance : ToString Problem where
  toString p :=
    "VER \n" ++
    (toString p.version) ++ "\n\n" ++
    "OBJSENSE \n" ++
    (toString p.objSense) ++ "\n\n" ++
    (if p.scalarVariables.isEmpty then "" else
      "VAR \n" ++
      (toString p.scalarVariables) ++ "\n") ++
    (if p.PSDVariables.isEmpty then "" else
      "PSDVAR \n" ++
      (toString p.PSDVariables) ++ "\n") ++
    (if p.scalarConstraints.isEmpty then "" else
      "CON \n" ++
      (toString p.scalarConstraints) ++ "\n") ++
    (if p.PSDConstraints.isEmpty then "" else
      "PSDCON \n" ++
      (toString p.PSDConstraints) ++ "\n") ++
    (if p.objectivePSDVariablesCoord.isEmpty then "" else
      "OBJFCOORD \n" ++
      (toString p.objectivePSDVariablesCoord) ++ "\n") ++
    (if p.objectiveScalarVariablesCoord.isEmpty then "" else
      "OBJACOORD \n" ++
      (toString p.objectiveScalarVariablesCoord) ++ "\n") ++
    (if p.objectiveShiftCoord.isEmpty then "" else
      "OBJBCOORD \n" ++
      (toString p.objectiveShiftCoord) ++ "\n\n") ++
    (if p.scalarConstraintsPSDVariablesCoord.isEmpty then "" else
      "FCOORD \n" ++
      (toString p.scalarConstraintsPSDVariablesCoord) ++ "\n") ++
    (if p.scalarConstraintsScalarVariablesCoord.isEmpty then "" else
      "ACOORD \n" ++
      (toString p.scalarConstraintsScalarVariablesCoord) ++ "\n") ++
    (if p.scalarConstraintsShiftCoord.isEmpty then "" else
      "BCOORD \n" ++
      (toString p.scalarConstraintsShiftCoord) ++ "\n") ++
    (if p.PSDConstraintsScalarVariablesCoord.isEmpty then "" else
      "HCOORD \n" ++
      (toString p.PSDConstraintsScalarVariablesCoord) ++ "\n") ++
    (if p.PSDConstraintsShiftCoord.isEmpty then "" else
      "DCOORD \n" ++
      (toString p.PSDConstraintsShiftCoord) ++ "\n")

def empty : EncodedValue := EncodedValue.mk none

instance : ToString DimensionList where
  toString dl :=
    (toString dl.n) ++ "\n" ++
    (dl.dimensions.foldl (fun acc d => acc ++ (toString d) ++ "\n") "")

Inv.inv in Init.Prelude

Fin.elim0 in Init.Data.Fin.Basic

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

Lean.Syntax.getId in Init.Prelude

D in SciLean.Tactic.CustomSimp.test_simp_guard

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

Lake.logInfo in Lake.Util.Log

let proof ← elabTerm stx (some transfTy)

@[strong_equiv]
def ofRelaxations (Rx₁ : p ≽' q) (Rx₂ : q ≽' p) : p ≡' q :=
  { phi := Rx₁.phi,
    psi := Rx₂.phi,
    phi_feasibility := Rx₁.phi_feasibility,
    psi_feasibility := Rx₂.phi_feasibility,
    phi_optimality := Rx₁.phi_optimality,
    psi_optimality := Rx₂.phi_optimality }

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

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

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

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

abbrev CanonExpr := Expr

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

let (sls₁, mls₁) ← generateBasisOfShape tyl
      let sls ← sls₁.mapM fun l => mkAppM ``Prod.mk #[l, r₀]
      let mls ← mls₁.mapM fun l => mkAppM ``Prod.mk #[l, r₀]

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

LDL.lowerInv in Mathlib.Analysis.Matrix.LDL

Float.exp in Init.Data.Float

Lean.ReducibilityHints.regular in Lean.Declaration

structure Variable extends Constraint where
  conicDual : Option Float

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

def setPSDVariables (p : Problem) (dl : DimensionList) : Problem :=
  { p with PSDVariables := dl }

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

HMul in Init.Prelude

abbrev FeasibilityProof := Expr

def stackPopTillOpen (stk : List SexpTok) (sexps : List Sexp := []) :
    Option (String.Pos × (List SexpTok) × (List Sexp)) :=
  match stk with
  | [] => .none
  | SexpTok.opening openPos :: rest => (.some (openPos, rest, sexps))
  | SexpTok.sexp s :: rest => stackPopTillOpen rest (s :: sexps)

Iff in Init.Core

return backwardMap

Lean.Parser.Term.bracketedBinderF in Lean.Parser.Term

return constrTags
</all_available_defs>

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

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

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

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

lemma prod_gaussianPdf_pos {N n : ℕ} (R : Matrix (Fin n) (Fin n) ℝ) (y : Fin N → Fin n → ℝ)
    (h : R.PosDef) : 0 < ∏ i : Fin N, gaussianPdf R (y i)

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

lemma conj_symm {x : n → 𝕜} {M : Matrix n n 𝕜} (hM : M.IsHermitian) :
    star (star x ⬝ᵥ mulVec M x) = star x ⬝ᵥ mulVec M x

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

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

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

lemma upperTriangular.mul [Fintype m] [LinearOrder m] (hM : upperTriangular M)
    (hN : upperTriangular N) : upperTriangular (M * 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 one_div_eq_pow_neg_one {a : ℝ} (ha : 0 < a) : 1 / a = a ^ (-1 : ℝ)

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

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 induces_original_problem_optimality (Rx : p ≽' q) (phi_inv : E → D)
    (phi_left_inv : Function.LeftInverse Rx.phi phi_inv)
    (h_objFun : ∀ x, p.feasible x → p.objFun x = q.objFun (Rx.phi x)) {y : E}
    (h_opt_y : q.optimal y) (h_feas_y : p.feasible (phi_inv y)) : p.optimal (phi_inv y)

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

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

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

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

lemma soCone_add_sub_two_mul_of_nonneg {x y : ℝ} (z : ℝ)
    (hx : 0 ≤ x) (hy : 0 ≤ y) : soCone (x + y) ![x - y, 2 * z] ↔ z ^ (2 : ℝ) ≤ x * y

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

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

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

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

<local_ctx>
import CvxLean.Lib.Math.LinearAlgebra.Matrix.PosDef

noncomputable section CovarianceEstimation

open Real

open Matrix

open BigOperators

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

def gaussianPdf {n : ℕ} (R : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) : ℝ :=
  (1 / sqrt (((2 * π) ^ n) * R.det)) * exp (- R⁻¹.quadForm x / 2)
</local_ctx>

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

