From 6b36fa12391d8a65b7906a45bcbcb3f562e11969 Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Thu, 2 May 2024 16:59:52 -0400
Subject: [PATCH 01/14] chore: bump to v4.8.0-rc1

---
 lakefile.lean  | 4 +---
 lean-toolchain | 2 +-
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index d40f0c64..70a939f8 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -12,7 +12,7 @@ package CvxLean where
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4" @
-  "c838d28fb418158125f1551662ef55113d22eeec"
+  "efad919b6687484ee26ac7c65a29c972d2112b8d"
 
 meta if get_config? env = some "scilean" then
 require scilean from git
@@ -52,7 +52,6 @@ def buildCargo (targetFile : FilePath) (manifestFile : FilePath) (targetDest : F
       args := #[targetFile.toString, targetDest.toString]
     }
 
-@[default_target]
 target EggPreDCP (pkg) : FilePath := do
   let buildDir := pkg.dir / "egg-pre-dcp"
   let binFile := buildDir / "target" / "release" / "egg-pre-dcp"
@@ -60,7 +59,6 @@ target EggPreDCP (pkg) : FilePath := do
   let manifestFile := buildDir / "Cargo.toml"
   buildCargo binFile manifestFile dest #[] false
 
-@[default_target]
 target EggPreDCPStopOnSuccess (pkg) : FilePath := do
   let buildDir := pkg.dir / "egg-pre-dcp"
   let binFile := buildDir / "target" / "release" / "egg-pre-dcp"
diff --git a/lean-toolchain b/lean-toolchain
index cfcdd327..d8a6d7ef 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.0-rc1
+leanprover/lean4:v4.8.0-rc1

From 0f38433d1f6f5a92ee627cbd880684fd2decd67d Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Thu, 2 May 2024 17:02:21 -0400
Subject: [PATCH 02/14] chore: update lake manifest

---
 lake-manifest.json | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 3d9812ca..4258127b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "276953b13323ca151939eafaaec9129bf7970306",
+   "rev": "3025cb124492b423070f20cf0a70636f757d117f",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "6beed82dcfbb7731d173cd517675df27d62ad0f4",
+   "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,16 +31,16 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "af1e86cf7a37389632a02f4a111e6b501b2b818f",
+   "rev": "fe1eff53bd0838c657aa6126fe4dd75ad9939d9a",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.27",
+   "inputRev": "v0.0.35",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
+   "rev": "188eb34fcf1125e89d651ad462d02598219718ca",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,10 +58,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "c838d28fb418158125f1551662ef55113d22eeec",
+   "rev": "efad919b6687484ee26ac7c65a29c972d2112b8d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "c838d28fb418158125f1551662ef55113d22eeec",
+   "inputRev": "efad919b6687484ee26ac7c65a29c972d2112b8d",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "CvxLean",

From 2f92e463f118402c3f6f19b33db5d78bcc982244 Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Thu, 2 May 2024 17:06:13 -0400
Subject: [PATCH 03/14] fix: `OfScientific` instances

---
 CvxLean/Command/Solve/Float/FloatToReal.lean | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/CvxLean/Command/Solve/Float/FloatToReal.lean b/CvxLean/Command/Solve/Float/FloatToReal.lean
index 90ba5631..c60617b8 100644
--- a/CvxLean/Command/Solve/Float/FloatToReal.lean
+++ b/CvxLean/Command/Solve/Float/FloatToReal.lean
@@ -12,25 +12,23 @@ open Lean
 
 /-- Convert a `Float` to an `Expr` of type `Real`. -/
 def floatToReal (f : Float) : Expr :=
-  let divisionRingToOfScientific :=
-    mkApp2 (mkConst ``DivisionRing.toOfScientific ([levelZero] : List Level))
-      (mkConst ``Real)
-      (mkConst ``Real.instDivisionRingReal)
+  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)
-      divisionRingToOfScientific
+      (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.instNegReal) num
+          (mkConst ``Real) (mkConst ``Real.instNeg) num
       else num
   -- On parser error return zero.
   | Parsec.ParseResult.error _ _ =>
       mkApp3 realOfScientific
-        (mkConst ``Int.zero) (toExpr true) (mkNatLit 1)
+        (mkNatLit 0) (toExpr true) (mkNatLit 1)
 
 end CvxLean

From 0132023059d678b0fe2fcbdc2de2aa42bda9dad3 Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Thu, 2 May 2024 17:32:29 -0400
Subject: [PATCH 04/14] wip: fixing `Lib` errors due to new `mathlib`

---
 .../InnerProductSpace/GramSchmidtOrtho.lean    |  7 +++----
 .../Analysis/InnerProductSpace/Spectrum.lean   | 17 ++++++++---------
 .../Math/LinearAlgebra/Matrix/Spectrum.lean    | 18 ++++++++----------
 3 files changed, 19 insertions(+), 23 deletions(-)

diff --git a/CvxLean/Lib/Math/Analysis/InnerProductSpace/GramSchmidtOrtho.lean b/CvxLean/Lib/Math/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
index a2384f45..25038321 100644
--- a/CvxLean/Lib/Math/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
+++ b/CvxLean/Lib/Math/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
@@ -6,7 +6,7 @@ The Gram-Schmidt algorithm respects basis vectors.
 
 section GramSchmidt
 
-variable (𝕜 : Type _) {E : Type _} [IsROrC 𝕜]
+variable (𝕜 : Type _) {E : Type _} [RCLike 𝕜]
 variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
 variable {ι : Type _} [LinearOrder ι] [LocallyFiniteOrderBot ι]
 variable [IsWellOrder ι (· < · : ι → ι → Prop)]
@@ -17,9 +17,8 @@ local notation "⟪" x "," y "⟫" => @inner 𝕜 _ _ x y
 
 lemma repr_gramSchmidt_diagonal {i : ι} (b : Basis ι 𝕜 E) :
     b.repr (gramSchmidt 𝕜 b i) i = 1 := by
-  rw [gramSchmidt_def, LinearEquiv.map_sub, Finsupp.sub_apply, Basis.repr_self,
-    Finsupp.single_eq_same, sub_eq_self, map_sum, Finsupp.coe_finset_sum,
-    Finset.sum_apply, Finset.sum_eq_zero]
+  rw [gramSchmidt_def, map_sub, Finsupp.sub_apply, Basis.repr_self, Finsupp.single_eq_same,
+    sub_eq_self, map_sum, Finsupp.coe_finset_sum, Finset.sum_apply, Finset.sum_eq_zero]
   intros j hj
   rw [Finset.mem_Iio] at hj
   simp [orthogonalProjection_singleton, gramSchmidt_triangular hj]
diff --git a/CvxLean/Lib/Math/Analysis/InnerProductSpace/Spectrum.lean b/CvxLean/Lib/Math/Analysis/InnerProductSpace/Spectrum.lean
index 64e368ab..5e47b8dd 100644
--- a/CvxLean/Lib/Math/Analysis/InnerProductSpace/Spectrum.lean
+++ b/CvxLean/Lib/Math/Analysis/InnerProductSpace/Spectrum.lean
@@ -6,7 +6,7 @@ Version of the spectral theorem.
 
 namespace LinearMap
 
-variable {𝕜 : Type _} [IsROrC 𝕜] [DecidableEq 𝕜]
+variable {𝕜 : Type _} [RCLike 𝕜] [DecidableEq 𝕜]
 variable {E : Type _} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
 variable [FiniteDimensional 𝕜 E]
 variable {n : ℕ} (hn : FiniteDimensional.finrank 𝕜 E = n)
@@ -19,14 +19,13 @@ lemma spectral_theorem' (v : E) (i : Fin n)
     (xs : OrthonormalBasis (Fin n) 𝕜 E) (as : Fin n → ℝ)
     (hxs : ∀ j, Module.End.HasEigenvector T (as j) (xs j)) :
     xs.repr (T v) i = as i * xs.repr v i := by
-  suffices : ∀ w : EuclideanSpace 𝕜 (Fin n),
-    T (xs.repr.symm w) = xs.repr.symm (fun i => as i * w i)
-  { simpa only [LinearIsometryEquiv.symm_apply_apply,
-      LinearIsometryEquiv.apply_symm_apply]
-      using congr_arg (fun (v : E) => (xs.repr) v i) (this ((xs.repr) v)) }
+  suffices hsuff : ∀ (w : EuclideanSpace 𝕜 (Fin n)),
+    T (xs.repr.symm w) = xs.repr.symm (fun i => as i * w i) by
+      simpa only [LinearIsometryEquiv.symm_apply_apply,
+        LinearIsometryEquiv.apply_symm_apply]
+        using congr_arg (fun (v : E) => (xs.repr) v i) (hsuff ((xs.repr) v))
   intros w
-  simp_rw [← OrthonormalBasis.sum_repr_symm, map_sum,
-    LinearMap.map_smul, fun j => Module.End.mem_eigenspace_iff.mp (hxs j).1,
-    smul_smul, mul_comm]
+  simp_rw [← OrthonormalBasis.sum_repr_symm, map_sum, LinearMap.map_smul,
+    fun j => Module.End.mem_eigenspace_iff.mp (hxs j).1, smul_smul, mul_comm]
 
 end LinearMap
diff --git a/CvxLean/Lib/Math/LinearAlgebra/Matrix/Spectrum.lean b/CvxLean/Lib/Math/LinearAlgebra/Matrix/Spectrum.lean
index 91fe4d97..464df97b 100644
--- a/CvxLean/Lib/Math/LinearAlgebra/Matrix/Spectrum.lean
+++ b/CvxLean/Lib/Math/LinearAlgebra/Matrix/Spectrum.lean
@@ -7,7 +7,7 @@ Version of the spectral theorem for matrices.
 
 namespace Matrix
 
-variable {𝕜 : Type _} [IsROrC 𝕜] [DecidableEq 𝕜]
+variable {𝕜 : Type _} [RCLike 𝕜] [DecidableEq 𝕜]
 variable {n : Type _} [Fintype n] [DecidableEq n]
 variable {A : Matrix n n 𝕜}
 
@@ -25,7 +25,7 @@ noncomputable def frobeniusNormedAddCommGroup' [NormedAddCommGroup 𝕜] :
 attribute [-instance] Pi.normedAddCommGroup
 
 noncomputable instance : InnerProductSpace 𝕜 (n → 𝕜) :=
-  EuclideanSpace.instInnerProductSpace
+  PiLp.innerProductSpace (fun _ : n => 𝕜)
 
 lemma IsHermitian.hasEigenvector_eigenvectorBasis (hA : A.IsHermitian) (i : n) :
     Module.End.HasEigenvector (Matrix.toLin' A) (hA.eigenvalues i) (hA.eigenvectorBasis i) := by
@@ -37,15 +37,14 @@ diagonalized by a change of basis using a matrix consisting of eigenvectors. -/
 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 (IsROrC.ofReal ∘ as) * xs.toBasis.toMatrix (Pi.basisFun 𝕜 n) := by
+    diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix (Pi.basisFun 𝕜 n) := by
   rw [basis_toMatrix_basisFun_mul]
   ext i j
   let xs' := xs.reindex (Fintype.equivOfCardEq (Fintype.card_fin _)).symm
   let as' : Fin (Fintype.card n) → ℝ :=
     fun i => as <| (Fintype.equivOfCardEq (Fintype.card_fin _)) i
-  have hxs' :
-    ∀ j, Module.End.HasEigenvector (Matrix.toLin' A) (as' j) (xs' j) := by
-    simp only [OrthonormalBasis.coe_reindex, Equiv.symm_symm]
+  have hxs' : ∀ j, Module.End.HasEigenvector (Matrix.toLin' A) (as' j) (xs' j) := by
+    simp only [xs', OrthonormalBasis.coe_reindex, Equiv.symm_symm]
     intros j
     exact (hxs ((Fintype.equivOfCardEq (Fintype.card_fin _)) j))
   convert @LinearMap.spectral_theorem' 𝕜 _
@@ -54,10 +53,9 @@ theorem spectral_theorem (xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n))
     ((Fintype.equivOfCardEq (Fintype.card_fin _)).symm i)
     xs' as' hxs'
   { erw [toLin'_apply]
-    simp only [OrthonormalBasis.coe_toBasis_repr_apply, of_apply,
+    simp only [xs', OrthonormalBasis.coe_toBasis_repr_apply, of_apply,
       OrthonormalBasis.repr_reindex]
-    erw [Equiv.symm_apply_apply, EuclideanSpace.single,
-      WithLp.equiv_symm_pi_apply 2, mulVec_single]
+    erw [Equiv.symm_apply_apply, EuclideanSpace.single, WithLp.equiv_symm_pi_apply 2, mulVec_single]
     simp_rw [mul_one]
     rfl }
   { simp only [diagonal_mul, Function.comp]
@@ -65,7 +63,7 @@ theorem spectral_theorem (xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n))
       OrthonormalBasis.repr_reindex, Pi.basisFun_apply, LinearMap.coe_stdBasis,
       EuclideanSpace.single, WithLp.equiv_symm_pi_apply 2,
       Equiv.symm_apply_apply, Equiv.apply_symm_apply]
-    rfl }
+    congr; simp }
 
 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 := by

From 6061f82fe50f76aeab18966e523a27824222b981 Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Thu, 2 May 2024 17:33:27 -0400
Subject: [PATCH 05/14] fix: deprecated `SchedulerM`

---
 lakefile.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lakefile.lean b/lakefile.lean
index 70a939f8..8aa4da5c 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -41,7 +41,7 @@ def compileCargo (name : String) (manifestFile : FilePath) (cargo : FilePath :=
 
 def buildCargo (targetFile : FilePath) (manifestFile : FilePath) (targetDest : FilePath)
     (oFileJobs : Array (BuildJob FilePath)) (stopOnSuccess : Bool) :
-    SchedulerM (BuildJob FilePath) :=
+    SpawnM (BuildJob FilePath) :=
   let name := targetFile.fileName.getD targetFile.toString
   buildFileAfterDepArray targetFile oFileJobs fun _ => do
     let env := if stopOnSuccess then #[("RUSTFLAGS", some "--cfg stop_on_success")] else #[]

From 061134729291ad7df4085a4818b6638a1be7a261 Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Fri, 3 May 2024 17:59:41 -0400
Subject: [PATCH 06/14] wip: fixing more errors in proofs

---
 .../Solve/Float/RealToFloatLibrary.lean       | 22 ++++++++--------
 CvxLean/Lib/Math/CovarianceEstimation.lean    | 15 ++++++-----
 .../Lib/Math/LinearAlgebra/Matrix/Block.lean  |  6 ++---
 .../Lib/Math/LinearAlgebra/Matrix/LDL.lean    |  2 +-
 .../Lib/Math/LinearAlgebra/Matrix/PosDef.lean |  8 +++---
 CvxLean/Lib/Math/LogDet.lean                  |  6 ++---
 CvxLean/Lib/Math/SchurComplement.lean         | 16 ++++++------
 CvxLean/Lib/Math/Subadditivity.lean           |  8 +++---
 CvxLean/Meta/Minimization.lean                |  3 ++-
 CvxLean/Syntax/Minimization.lean              |  2 +-
 CvxLean/Tactic/Basic/RewriteOpt.lean          |  4 +--
 CvxLean/Tactic/PreDCP/Egg/ToExpr.lean         | 25 +++++++++----------
 12 files changed, 58 insertions(+), 59 deletions(-)

diff --git a/CvxLean/Command/Solve/Float/RealToFloatLibrary.lean b/CvxLean/Command/Solve/Float/RealToFloatLibrary.lean
index 822b28dc..14eda00b 100644
--- a/CvxLean/Command/Solve/Float/RealToFloatLibrary.lean
+++ b/CvxLean/Command/Solve/Float/RealToFloatLibrary.lean
@@ -17,25 +17,25 @@ section Basic
 add_real_to_float : Real :=
   Float
 
-add_real_to_float : Real.instInhabitedReal :=
+add_real_to_float : Real.instInhabited :=
   instInhabitedFloat
 
-add_real_to_float : Real.instZeroReal :=
+add_real_to_float : Real.instZero :=
   Zero.mk (0 : Float)
 
-add_real_to_float : Real.instOneReal :=
+add_real_to_float : Real.instOne :=
   One.mk (1 : Float)
 
-add_real_to_float : Real.instLEReal :=
+add_real_to_float : Real.instLE :=
   instLEFloat
 
-add_real_to_float : Real.instLTReal :=
+add_real_to_float : Real.instLT :=
   instLTFloat
 
 add_real_to_float : Real.instDivReal  :=
   instDivFloat
 
-add_real_to_float : Real.instPowReal :=
+add_real_to_float : Real.instPow :=
   Pow.mk Float.pow
 
 add_real_to_float (n : Nat) (i) : @OfNat.ofNat Real n i :=
@@ -54,9 +54,9 @@ add_real_to_float (k : Nat) :
 add_real_to_float (i) : @Ring.toNeg Real i :=
   Neg.mk Float.neg
 
-add_real_to_float : Real.instNegReal := instNegFloat
+add_real_to_float : Real.instNeg := instNegFloat
 
-add_real_to_float : Real.instAddReal := instAddFloat
+add_real_to_float : Real.instAdd := instAddFloat
 
 add_real_to_float (i) : @HAdd.hAdd Real Real Real i :=
   Float.add
@@ -64,7 +64,7 @@ add_real_to_float (i) : @HAdd.hAdd Real Real Real i :=
 add_real_to_float (i) : @instHAdd Real i :=
   @HAdd.mk Float Float Float Float.add
 
-add_real_to_float : Real.instSubReal := instSubFloat
+add_real_to_float : Real.instSub := instSubFloat
 
 add_real_to_float (i) : @HSub.hSub Real Real Real i :=
   Float.sub
@@ -72,7 +72,7 @@ add_real_to_float (i) : @HSub.hSub Real Real Real i :=
 add_real_to_float (i) : @instHSub Real i :=
   @HSub.mk Float Float Float Float.sub
 
-add_real_to_float : Real.instMulReal := instMulFloat
+add_real_to_float : Real.instMul := instMulFloat
 
 add_real_to_float (i) : @HMul.hMul Real Real Real i :=
   Float.mul
@@ -128,7 +128,7 @@ add_real_to_float (n) (i) : @Norm.norm.{0} (Fin n → ℝ) i :=
 add_real_to_float (i) : @OfScientific.ofScientific Real i :=
   Float.ofScientific
 
-add_real_to_float : Real.natCast :=
+add_real_to_float : Real.instNatCast :=
   NatCast.mk Float.ofNat
 
 end Basic
diff --git a/CvxLean/Lib/Math/CovarianceEstimation.lean b/CvxLean/Lib/Math/CovarianceEstimation.lean
index ef9d623d..bd7857dd 100644
--- a/CvxLean/Lib/Math/CovarianceEstimation.lean
+++ b/CvxLean/Lib/Math/CovarianceEstimation.lean
@@ -58,14 +58,13 @@ lemma sum_quadForm {n : ℕ} (R : Matrix (Fin n) (Fin n) ℝ) {m : ℕ} (y : Fin
   { subst h; simp }
   simp only [Matrix.quadForm, Matrix.trace, covarianceMatrix, diag, mul_apply, Finset.sum_mul,
     Finset.sum_div]
-  simp_rw [@Finset.sum_comm _ (Fin m), Finset.mul_sum]
-  apply congr_arg
-  ext i
-  unfold dotProduct
-  have : (m : ℝ) ≠ 0 := by simp [h]
-  simp_rw [← mul_assoc, mul_div_cancel' _ this]
-  apply congr_arg
-  ext j
+  erw [Finset.sum_comm (γ := Fin m)]
+  simp_rw [Finset.mul_sum]
+  congr; ext i
+  have hmnz : (m : ℝ) ≠ 0 := by simp [h]
+  simp_rw [← mul_assoc, mul_div_cancel₀ _ hmnz]
+  erw [Finset.sum_comm (α := Fin m)]
+  congr; ext j
   simp_rw [mul_assoc, ← Finset.mul_sum]
   apply congr_arg
   unfold Matrix.mulVec
diff --git a/CvxLean/Lib/Math/LinearAlgebra/Matrix/Block.lean b/CvxLean/Lib/Math/LinearAlgebra/Matrix/Block.lean
index c96acc25..17a72c28 100644
--- a/CvxLean/Lib/Math/LinearAlgebra/Matrix/Block.lean
+++ b/CvxLean/Lib/Math/LinearAlgebra/Matrix/Block.lean
@@ -57,7 +57,7 @@ lemma toBlock_inverse_mul_toBlock_eq_one_of_BlockTriangular [LinearOrder α]
   have h_sum : M⁻¹.toBlock p p * M.toBlock p p +
       M⁻¹.toBlock p (fun i => ¬ p i) * M.toBlock (fun i => ¬ p i) p = 1 := by
     rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
-  have h_zero : M.toBlock (fun i => ¬ p i) p = 0
+  have h_zero : M.toBlock (fun i => ¬ p i) p = 0 := by
   { ext i j
     simpa using hM (lt_of_lt_of_le j.2 (le_of_not_lt i.2)) }
   simpa [h_zero] using h_sum
@@ -87,7 +87,7 @@ lemma toSquareBlock_inv_mul_toSquareBlock_eq_one [LinearOrder α]
       M⁻¹.toBlock p (λ i => ¬ p i) * M.toBlock (λ i => ¬ p i) p = 1 := by
     rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
   have h_zero : ∀ i j l,
-    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
+    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0 := by
   { intro i j l
     by_cases hj : b j.1 ≤ k
     { have hj := lt_of_le_of_ne hj j.2
@@ -98,7 +98,7 @@ lemma toSquareBlock_inv_mul_toSquareBlock_eq_one [LinearOrder α]
       apply mul_eq_zero_of_right
       simpa using hM (lt_of_eq_of_lt l.2 hj) }}
   have h_zero' :
-    M⁻¹.toBlock p (λ (i : m) => ¬p i) * M.toBlock (λ (i : m) => ¬p i) p = 0
+    M⁻¹.toBlock p (λ (i : m) => ¬p i) * M.toBlock (λ (i : m) => ¬p i) p = 0 := by
   { ext i l
     apply sum_eq_zero (λ j _ => h_zero i j l) }
   simpa [h_zero'] using h_sum
diff --git a/CvxLean/Lib/Math/LinearAlgebra/Matrix/LDL.lean b/CvxLean/Lib/Math/LinearAlgebra/Matrix/LDL.lean
index 4a737ebe..534d25b4 100644
--- a/CvxLean/Lib/Math/LinearAlgebra/Matrix/LDL.lean
+++ b/CvxLean/Lib/Math/LinearAlgebra/Matrix/LDL.lean
@@ -8,7 +8,7 @@ import CvxLean.Lib.Math.LinearAlgebra.Matrix.Triangular
 More results about LDL factorization (see `Mathlib.LinearAlgebra.Matrix.LDL`).
 -/
 
-variable {𝕜 : Type _} [IsROrC 𝕜]
+variable {𝕜 : Type _} [RCLike 𝕜]
 variable {n : Type _} [LinearOrder n] [IsWellOrder n (· < · : n → n → Prop)]
 variable [LocallyFiniteOrderBot n]
 
diff --git a/CvxLean/Lib/Math/LinearAlgebra/Matrix/PosDef.lean b/CvxLean/Lib/Math/LinearAlgebra/Matrix/PosDef.lean
index ca955387..258a9878 100644
--- a/CvxLean/Lib/Math/LinearAlgebra/Matrix/PosDef.lean
+++ b/CvxLean/Lib/Math/LinearAlgebra/Matrix/PosDef.lean
@@ -10,8 +10,8 @@ namespace Matrix
 
 variable {m n : Type _} [Fintype m] [Fintype n]
 variable {𝕜 : Type _}
-variable [NormedField 𝕜] [PartialOrder 𝕜] [StarOrderedRing 𝕜]
-variable [IsROrC 𝕜]
+variable [NormedField 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜]
+variable [RCLike 𝕜]
 
 lemma PosSemidef.det_nonneg {M : Matrix n n ℝ} (hM : M.PosSemidef) [DecidableEq n] : 0 ≤ det M := by
   rw [hM.1.det_eq_prod_eigenvalues]
@@ -39,7 +39,7 @@ lemma PosSemidef_diagonal [DecidableEq n] {f : n → ℝ} (hf : ∀ i, 0 ≤ f i
     (diagonal f).PosSemidef := by
   refine' ⟨isHermitian_diagonal _, _⟩
   intro x
-  simp only [star, id.def, IsROrC.re_to_real]
+  simp only [star, id_def, RCLike.re_to_real]
   apply Finset.sum_nonneg'
   intro i
   rw [mulVec_diagonal f x i, mul_comm, mul_assoc]
@@ -48,7 +48,7 @@ lemma PosSemidef_diagonal [DecidableEq n] {f : n → ℝ} (hf : ∀ i, 0 ≤ f i
 lemma PosDef_diagonal [DecidableEq n] {f : n → ℝ} (hf : ∀ i, 0 < f i) : (diagonal f).PosDef := by
   refine' ⟨isHermitian_diagonal _, _⟩
   intros x hx
-  simp only [star, id.def, IsROrC.re_to_real]
+  simp only [star, id_def, RCLike.re_to_real]
   apply Finset.sum_pos'
   { intros i _
     rw [mulVec_diagonal f x i, mul_comm, mul_assoc]
diff --git a/CvxLean/Lib/Math/LogDet.lean b/CvxLean/Lib/Math/LogDet.lean
index 190ec7ca..44df9055 100644
--- a/CvxLean/Lib/Math/LogDet.lean
+++ b/CvxLean/Lib/Math/LogDet.lean
@@ -18,7 +18,7 @@ namespace Matrix
 open Matrix BigOperators
 
 variable {n : Type} [Fintype n] [LinearOrder n] [LocallyFiniteOrderBot n]
-variable {𝕜 : Type} [IsROrC 𝕜]
+variable {𝕜 : Type} [RCLike 𝕜]
 variable {A : Matrix n n ℝ} (hA : A.PosDef)
 
 noncomputable instance LDL.invertible_diag : Invertible (LDL.diag hA) := by
@@ -51,7 +51,7 @@ lemma LogDetAtom.feasibility_PosDef {D Z : Matrix n n ℝ} (hD : D = LDL.diag hA
 
 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 := by
-  have hY_tri : upperTriangular Y
+  have hY_tri : upperTriangular Y := by
   { rw [hY]
     apply upperTriangular.mul
     apply BlockTriangular_diagonal
@@ -113,7 +113,7 @@ lemma LogDetAtom.optimality_Ddet_le_Adet {t : n → ℝ} {Y Z D : Matrix n n ℝ
   by_cases h_nonempty : Nonempty n
   { have h_D_pd : D.PosDef := LogDetAtom.optimality_D_posdef ht hD hZ hPSD
     haveI h_D_invertible : Invertible D := h_D_pd.Invertible
-    have h_Zdet : Z.det = D.det
+    have h_Zdet : Z.det = D.det := by
     { rw [hZ, det_of_upperTriangular (upperTriangular_toUpperTri Y), hD, det_diagonal]
       simp [toUpperTri] }
     have h_ZDZ_semidef : (Zᴴ * D⁻¹ * Z).PosSemidef :=
diff --git a/CvxLean/Lib/Math/SchurComplement.lean b/CvxLean/Lib/Math/SchurComplement.lean
index 1ad2d927..fa2bacb7 100644
--- a/CvxLean/Lib/Math/SchurComplement.lean
+++ b/CvxLean/Lib/Math/SchurComplement.lean
@@ -21,7 +21,7 @@ namespace Matrix
 
 open scoped Matrix ComplexOrder
 
-variable {n : Type _} {m : Type _} {𝕜 : Type _} [IsROrC 𝕜]
+variable {n : Type _} {m : Type _} {𝕜 : Type _} [RCLike 𝕜]
 
 scoped infix:65 " ⊕ᵥ " => Sum.elim
 
@@ -50,17 +50,17 @@ lemma schur_complement_eq₂₂ [Fintype m] [Fintype n] [DecidableEq n] (A : Mat
 lemma IsHermitian.fromBlocks₁₁ [Fintype m] [DecidableEq m] {A : Matrix m m 𝕜} (B : Matrix m n 𝕜)
     (D : Matrix n n 𝕜) (hA : A.IsHermitian) :
     (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (D - Bᴴ * A⁻¹ * B).IsHermitian := by
-  have hBAB : (Bᴴ * A⁻¹ * B).IsHermitian
-  { apply isHermitian_conjTranspose_mul_mul
-    apply hA.inv }
+  have hBAB : (Bᴴ * A⁻¹ * B).IsHermitian := by
+    apply isHermitian_conjTranspose_mul_mul
+    apply hA.inv
   rw [isHermitian_fromBlocks_iff]
   constructor
-  { intro h
-    apply IsHermitian.sub h.2.2.2 hBAB }
-  { intro h
+  . intro h
+    apply IsHermitian.sub h.2.2.2 hBAB
+  . intro h
     refine' ⟨hA, rfl, conjTranspose_conjTranspose B, _⟩
     rw [← sub_add_cancel D]
-    apply IsHermitian.add h hBAB }
+    apply IsHermitian.add h hBAB
 
 lemma IsHermitian.fromBlocks₂₂ [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜) (B : Matrix m n 𝕜)
     {D : Matrix n n 𝕜} (hD : D.IsHermitian) :
diff --git a/CvxLean/Lib/Math/Subadditivity.lean b/CvxLean/Lib/Math/Subadditivity.lean
index b63da3c8..0609322a 100644
--- a/CvxLean/Lib/Math/Subadditivity.lean
+++ b/CvxLean/Lib/Math/Subadditivity.lean
@@ -41,14 +41,14 @@ open BigOperators Matrix
 
 namespace IsHermitian
 
-variable {𝕜 : Type _} [DecidableEq 𝕜] [IsROrC 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian)
+variable {𝕜 : Type _} [DecidableEq 𝕜] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian)
 
 lemma eigenvectorMatrix_inv_mul : hA.eigenvectorMatrixInv * hA.eigenvectorMatrix = 1 := by
   apply Basis.toMatrix_mul_toMatrix_flip
 
 -- NOTE: There is a `spectral_theorem'`.
 theorem spectral_theorem'' :
-    hA.eigenvectorMatrix * diagonal (IsROrC.ofReal ∘ hA.eigenvalues) * hA.eigenvectorMatrixᴴ =
+    hA.eigenvectorMatrix * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * hA.eigenvectorMatrixᴴ =
     A := by
   rw [conjTranspose_eigenvectorMatrix, Matrix.mul_assoc, ← spectral_theorem,
     ← Matrix.mul_assoc, eigenvectorMatrix_mul_inv, Matrix.one_mul]
@@ -109,7 +109,7 @@ lemma PosSemidef.PosDef_iff_det_ne_zero [DecidableEq n] {M : Matrix n n ℝ} (hM
   rw [← hM.sqrt_mul_sqrt, ← mulVec_mulVec, dotProduct_mulVec, ← transpose_transpose hM.1.sqrt,
     vecMul_transpose, transpose_transpose, ← conjTranspose_eq_transpose,
     hM.PosSemidef_sqrt.1.eq]
-  simp only [IsROrC.re_to_real, star, id]
+  simp only [RCLike.re_to_real, star, id]
   change @inner ℝ (EuclideanSpace ℝ _) _ (hM.1.sqrt.mulVec x) (hM.1.sqrt.mulVec x) ≠ 0
   intro hinner
   have sqrtMdet0 : hM.1.sqrt.det = 0 := by
@@ -130,7 +130,7 @@ lemma det_add_det_le_det_add' [Nonempty n] (A B : Matrix n n ℝ) (hA : A.PosDef
     isUnit_iff_ne_zero.2 hA.PosDef_sqrt.det_ne_zero
   have : IsUnit sqrtA :=
     (isUnit_iff_isUnit_det _).2 isUnit_det_sqrtA
-  have IsHermitian_sqrtA : sqrtA⁻¹.IsHermitian
+  have IsHermitian_sqrtA : sqrtA⁻¹.IsHermitian := by
   { apply IsHermitian.nonsingular_inv (hA.posSemidef.PosSemidef_sqrt.1)
     exact isUnit_det_sqrtA }
   have PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef :=
diff --git a/CvxLean/Meta/Minimization.lean b/CvxLean/Meta/Minimization.lean
index d1f6e67d..dd8f1594 100644
--- a/CvxLean/Meta/Minimization.lean
+++ b/CvxLean/Meta/Minimization.lean
@@ -192,7 +192,8 @@ partial def generateNewName (base : String) (set : HashSet Name) : MetaM Name :=
   tryNumber 1 set
 where
   tryNumber (i : Nat) vars : MetaM Name :=
-    let name := s!"{base}{i}"; if vars.contains name then tryNumber (i + 1) vars else return name
+    let name := Name.mkSimple s!"{base}{i}"
+    if vars.contains name then tryNumber (i + 1) vars else return name
 
 end Meta
 
diff --git a/CvxLean/Syntax/Minimization.lean b/CvxLean/Syntax/Minimization.lean
index d5b5db07..7808e967 100644
--- a/CvxLean/Syntax/Minimization.lean
+++ b/CvxLean/Syntax/Minimization.lean
@@ -195,7 +195,7 @@ partial def delabConstraints : DelabM (List (TSyntax ``Parser.constraint)) := do
 /-- Delaborate with variable names replaced. -/
 def withDomainBinding {α} [Inhabited α] (domain : Expr) (x : DelabM α) : DelabM α := do
   guard (← getExpr).isLambda
-  withBindingBody' `p fun p => do
+  withBindingBody' (x := pure) `p fun p => do
     withDomainLocalDecls domain p fun xs _prs => do
       let e ← getExpr
       let e ← replaceProjections e p.fvarId! xs
diff --git a/CvxLean/Tactic/Basic/RewriteOpt.lean b/CvxLean/Tactic/Basic/RewriteOpt.lean
index e3e849ff..cae5678b 100644
--- a/CvxLean/Tactic/Basic/RewriteOpt.lean
+++ b/CvxLean/Tactic/Basic/RewriteOpt.lean
@@ -161,7 +161,7 @@ def rewriteConstrLemma (rwIdx : Nat) (numConstrs : Nat) : MetaM (Name × Name) :
 
 section RIntro
 
-open Lean.Parser.Category Std.Tactic.RCases
+open Lean.Parser.Category
 
 def nameToRintroPat (n : Name) : TSyntax `rcasesPat :=
   Unhygienic.run `(rcasesPat| $(Lean.mkIdent n):ident)
@@ -233,7 +233,7 @@ def rewriteConstrBuilderFromTactic (shouldEval : Bool) (constrTag : Name)
       else
         let toRIntro ← namesToRintroPat constrTagsAfter
         let (gsAfterRIntro, _) ← TermElabM.run <|
-          Std.Tactic.RCases.rintro #[toRIntro] none gAfterIntros1
+          RCases.rintro #[toRIntro] none gAfterIntros1
         if gsAfterRIntro.length != 1 then
           throwRwConstrError "could not introduce optimization variables."
         return (fvarIds[0]!, gsAfterRIntro[0]!)
diff --git a/CvxLean/Tactic/PreDCP/Egg/ToExpr.lean b/CvxLean/Tactic/PreDCP/Egg/ToExpr.lean
index 443e18a9..46c91d64 100644
--- a/CvxLean/Tactic/PreDCP/Egg/ToExpr.lean
+++ b/CvxLean/Tactic/PreDCP/Egg/ToExpr.lean
@@ -62,20 +62,19 @@ partial def EggTree.toExpr (vars params : List String) : EggTree → MetaM Expr
       match Json.Parser.num s.mkIterator with
       | Parsec.ParseResult.success _ res => do
           -- NOTE: not ideal, but `norm_num` should get us to where we want.
-          let divisionRingToOfScientific :=
-            mkApp2 (mkConst ``DivisionRing.toOfScientific [levelZero])
-              (mkConst ``Real)
-              (mkConst ``Real.instDivisionRingReal)
+          let nnRatCastToOfScientific :=
+            mkApp2 (mkConst ``NNRatCast.toOfScientific ([levelZero] : List Level))
+              (mkConst ``Real) (mkConst ``Real.instNNRatCast)
           let realOfScientific :=
             mkApp2 (mkConst ``OfScientific.ofScientific [levelZero])
               (mkConst ``Real)
-              divisionRingToOfScientific
+              nnRatCastToOfScientific
           let num := mkApp3 realOfScientific
             (mkNatLit res.mantissa.natAbs) (Lean.toExpr true) (mkNatLit res.exponent)
           let expr :=
             if res.mantissa < 0 then
               mkApp3
-                (mkConst ``Neg.neg [levelZero]) (mkConst ``Real) (mkConst ``Real.instNegReal) num
+                (mkConst ``Neg.neg [levelZero]) (mkConst ``Real) (mkConst ``Real.instNeg) num
             else num
           let simpResult ←
             Mathlib.Meta.NormNum.deriveSimp (ctx := ← Simp.Context.mkDefault) (e := expr)
@@ -110,19 +109,19 @@ partial def EggTree.toExpr (vars params : List String) : EggTree → MetaM Expr
       let t ← toExpr vars params t
       return mkAppN
         (mkConst ``Neg.neg [levelZero])
-        #[(mkConst ``Real), (mkConst ``Real.instNegReal), t]
+        #[(mkConst ``Real), (mkConst ``Real.instNeg), t]
   -- Inverse.
   | Tree.node "inv" #[t] => do
       let t ← toExpr vars params t
       return mkAppN
         (mkConst ``Inv.inv [levelZero])
-        #[(mkConst ``Real), (mkConst ``Real.instInvReal), t]
+        #[(mkConst ``Real), (mkConst ``Real.instInv), t]
   -- Absolute value.
   | Tree.node "abs" #[t] => do
       let t ← toExpr vars params t
       return mkAppN
         (mkConst ``abs [levelZero])
-        #[(mkConst ``Real), (mkConst ``Real.lattice), (mkConst ``Real.instAddGroupReal), t]
+        #[(mkConst ``Real), (mkConst ``Real.lattice), (mkConst ``Real.instAddGroup), t]
   -- Square root.
   | Tree.node "sqrt" #[t] => do
       let t ← toExpr vars params t
@@ -159,17 +158,17 @@ partial def EggTree.toExpr (vars params : List String) : EggTree → MetaM Expr
   | Tree.node "add" #[t1, t2] => do
       let t1 ← toExpr vars params t1
       let t2 ← toExpr vars params t2
-      return mkRealHBinAppExpr ``HAdd.hAdd ``instHAdd 1 ``Real.instAddReal t1 t2
+      return mkRealHBinAppExpr ``HAdd.hAdd ``instHAdd 1 ``Real.instAdd t1 t2
   -- Subtraction.
   | Tree.node "sub" #[t1, t2] => do
       let t1 ← toExpr vars params t1
       let t2 ← toExpr vars params t2
-      return mkRealHBinAppExpr ``HSub.hSub ``instHSub 1 ``Real.instSubReal t1 t2
+      return mkRealHBinAppExpr ``HSub.hSub ``instHSub 1 ``Real.instSub t1 t2
   -- Multiplication.
   | Tree.node "mul" #[t1, t2] => do
       let t1 ← toExpr vars params t1
       let t2 ← toExpr vars params t2
-      return mkRealHBinAppExpr ``HMul.hMul ``instHMul 1 ``Real.instMulReal t1 t2
+      return mkRealHBinAppExpr ``HMul.hMul ``instHMul 1 ``Real.instMul t1 t2
   -- Division.
   | Tree.node "div" #[t1, t2] => do
       let t1 ← toExpr vars params t1
@@ -179,7 +178,7 @@ partial def EggTree.toExpr (vars params : List String) : EggTree → MetaM Expr
   | Tree.node "pow" #[t1, t2] => do
       let t1 ← toExpr vars params t1
       let t2 ← toExpr vars params t2
-      return mkRealHBinAppExpr ``HPow.hPow ``instHPow 2 ``Real.instPowReal t1 t2
+      return mkRealHBinAppExpr ``HPow.hPow ``instHPow 2 ``Real.instPow t1 t2
   -- Quad over Lin.
   | Tree.node "qol" #[t1, t2] =>
       EggTree.toExpr vars params (Tree.node "div" #[Tree.node "pow" #[t1, Tree.leaf "2"], t2])

From 46bc1a01fbcf35bdd1cae8e3a8077f08c6c87fe7 Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Fri, 3 May 2024 18:14:29 -0400
Subject: [PATCH 07/14] fix: all update-related errors fixed, mainly atoms

---
 CvxLean/Command/Solve/Conic.lean                    | 10 +++++-----
 CvxLean/Tactic/Basic/ChangeOfVariables.lean         |  2 +-
 CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean       |  2 +-
 CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean         |  4 ++--
 CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean      | 13 ++++++-------
 CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean         |  8 ++++----
 CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean       |  4 ++--
 CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean |  2 +-
 CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean          |  4 +---
 9 files changed, 23 insertions(+), 26 deletions(-)

diff --git a/CvxLean/Command/Solve/Conic.lean b/CvxLean/Command/Solve/Conic.lean
index be75b0b4..e62b8012 100644
--- a/CvxLean/Command/Solve/Conic.lean
+++ b/CvxLean/Command/Solve/Conic.lean
@@ -79,13 +79,13 @@ unsafe def solutionDataFromProblemData (minExpr : MinimizationExpr) (data : Prob
 
         match Sol.Parser.parse output with
         | Except.ok res =>
-          return Except.ok <| Sol.Result.toSolutionData res
+            return Except.ok <| Sol.Result.toSolutionData res
         | Except.error err =>
-          return Except.error ("MOSEK output parsing failed. " ++ err)
+            return Except.error ("MOSEK output parsing failed. " ++ err)
 
-    match res with
-    | Except.ok res => return res
-    | Except.error err => throwSolveError err
+  match res with
+  | Except.ok res => return res
+  | Except.error err => throwSolveError err
 
 /-- -/
 unsafe def exprFromSolutionData (minExpr : MinimizationExpr) (solData : SolutionData) :
diff --git a/CvxLean/Tactic/Basic/ChangeOfVariables.lean b/CvxLean/Tactic/Basic/ChangeOfVariables.lean
index b95b5057..53b9566d 100644
--- a/CvxLean/Tactic/Basic/ChangeOfVariables.lean
+++ b/CvxLean/Tactic/Basic/ChangeOfVariables.lean
@@ -122,7 +122,7 @@ instance {a : ℝ} : ChangeOfVariables (fun x : ℝ => a * x) :=
 instance {a : ℝ} : ChangeOfVariables (fun x : ℝ => a / x) :=
   { inv := fun x => a / x
     condition := fun x => x ≠ 0 ∧ a ≠ 0
-    property := fun _ ⟨_, ha⟩ => by field_simp; rw [mul_comm] }
+    property := fun _ ⟨_, ha⟩ => by field_simp }
 
 instance {a : ℝ} : ChangeOfVariables (fun x : ℝ => x + a) :=
   { inv := fun x => x - a
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean
index 571c4486..2d9771f9 100644
--- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean
+++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean
@@ -109,7 +109,7 @@ optimality by
     { unfold nonnegOrthCone; simpa using c1 i }
     { unfold nonnegOrthCone; simpa using c2 i }
     { unfold nonnegOrthCone; simpa using c3 i }
-    { unfold rotatedSoCone; simp [sq_nonneg]; norm_num }
+    { unfold rotatedSoCone; simp [sq_nonneg] }
     { unfold nonnegOrthCone; simp [sub_nonneg, abs] }
     { unfold nonnegOrthCone; simp [← sub_le_iff_le_add, abs] }
 
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean
index 948d4fdf..aafeb2eb 100644
--- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean
+++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean
@@ -121,12 +121,12 @@ feasibility
   (c1 : by
     intros t i
     rw [vec_soCone_apply_to_soCone_add_sub_two]
-    dsimp
+    dsimp [t]
     rw [Real.one_div_eq_pow_neg_one (hx i)]
     exact powNegOne.feasibility0 (x i) (hx i))
   (c2 : by
     intros t i
-    dsimp
+    dsimp [t]
     rw [Real.one_div_eq_pow_neg_one (hx i)]
     have hinv : 0 < (x i) ^ (-1 : ℝ) := by rw [rpow_neg_one, inv_pos]; exact hx i
     exact le_of_lt hinv)
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean
index d68166d0..7f06e895 100644
--- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean
+++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean
@@ -17,8 +17,10 @@ namespace CvxLean
 
 open Matrix
 
-declare_atom Matrix.logDet [concave] (n : ℕ)&
-(A : Matrix.{0,0,0} (Fin n) (Fin n) ℝ)? : Real.log A.det :=
+set_option maxHeartbeats 400000
+
+declare_atom Matrix.logDet [concave] (n : ℕ)& (A : Matrix.{0,0,0} (Fin n) (Fin n) ℝ)? :
+  Real.log A.det :=
 vconditions (hA : A.PosDef)
 implementationVars (t : Fin n → ℝ) (Y : Matrix (Fin n) (Fin n) ℝ)
 -- The lower left values of `Y` are unused. CVXPY uses a vector `z` instead of a matrix `Y`.
@@ -63,9 +65,7 @@ optimality by
     apply c_exp
   dsimp at c_posdef
   -- NOTE: Not matching instances, hence `convert` not `exact`.
-  have h := Matrix.LogDetAtom.optimality
-    (A := A) (t := t) (Y := Y) ht rfl rfl (by convert c_posdef)
-  convert h
+  convert Matrix.LogDetAtom.optimality (A := A) (t := t) (Y := Y) ht rfl rfl (by convert c_posdef)
 vconditionElimination
   (hA : by
     have ht : ∀ (i : Fin n), Real.exp (t i) ≤ Matrix.diag Y i := by
@@ -73,7 +73,6 @@ vconditionElimination
       rw [Real.exp_iff_expCone]
       unfold Real.Vec.expCone at c_exp
       apply c_exp
-    exact Matrix.LogDetAtom.cond_elim
-      (A := A) (t := t) (Y := Y) ht rfl rfl (by convert c_posdef))
+    exact Matrix.LogDetAtom.cond_elim (A := A) (t := t) (Y := Y) ht rfl rfl (by convert c_posdef))
 
 end CvxLean
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean
index 1398b9b6..7226ac5f 100644
--- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean
+++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean
@@ -73,8 +73,8 @@ homogenity by
 additivity by
   ring
 optimality by
-  intros y' hy
-  apply mul_le_mul_of_nonpos_left hy hx
+  intros y' hy i
+  simpa using mul_le_mul_of_nonpos_left (hy i) (hx i)
 
 declare_atom Vec.mul4 [affine] (n : ℕ)& (x : Fin n → ℝ)- (y : Fin n → ℝ)& : x * y :=
 bconditions (hy : y ≤ 0)
@@ -83,7 +83,7 @@ homogenity by
 additivity by
   ring
 optimality by
-  intros y' hx
-  apply mul_le_mul_of_nonpos_right hx hy
+  intros y' hx i
+  simpa using mul_le_mul_of_nonpos_right (hx i) (hy i)
 
 end CvxLean
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean
index 4a8117c7..8aca24f3 100644
--- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean
+++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean
@@ -139,14 +139,14 @@ optimality by
   have hynn := le_of_lt hypos
   have hy2pos : 0 < y ^ (2 : ℝ):= by
     rw [rpow_two]
-    exact pow_two_pos_of_ne_zero y (ne_of_gt hypos)
+    exact pow_two_pos_of_ne_zero (ne_of_gt hypos)
   have ht₁pos : 0 < t₁ := by
     cases (lt_or_eq_of_le c4) with
     | inl h => exact h
     | inr h => rw [← h] at c1; linarith
   have ht₁2pos : 0 < t₁ ^ (2 : ℝ) := by
     rw [rpow_two]
-    exact pow_two_pos_of_ne_zero t₁ (ne_of_gt ht₁pos)
+    exact pow_two_pos_of_ne_zero (ne_of_gt ht₁pos)
   have ht₁inv : 0 < t₁ ^ (-1 : ℝ) := by rwa [rpow_neg_one, inv_pos]
   have ht₀pos : 0 < t₀ := by
     cases (lt_or_eq_of_le c3) with
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean
index 915d4dd2..65ee2f29 100644
--- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean
+++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean
@@ -91,7 +91,7 @@ feasibility
     have hynn : 0 ≤ y := fun i => by
       have hyi := hy i
       simp at hyi; positivity
-    intros t i; dsimp;
+    intros t i; dsimp [t];
     rw [rpow_two]
     exact div_nonneg (pow_two_nonneg (x i)) (hynn i))
   (c3 : by
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean
index 18cf21f2..43cc0cac 100644
--- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean
+++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean
@@ -24,9 +24,7 @@ solution
 solutionEqualsAtom rfl
 feasibility
   (c1 : by
-    unfold rotatedSoCone
-    simp
-    exact ⟨sq_nonneg x, zero_le_two⟩)
+    simp [rotatedSoCone, sq_nonneg x])
 optimality by
   unfold rotatedSoCone at c1
   have h := c1.1

From e031235e61dd5efb948748284433d14deb9bb2bc Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Fri, 3 May 2024 19:25:01 -0400
Subject: [PATCH 08/14] fix: syntax issues because of domain binding

---
 CvxLean/Meta/Util/SubExpr.lean   | 8 ++++++++
 CvxLean/Syntax/Minimization.lean | 2 +-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/CvxLean/Meta/Util/SubExpr.lean b/CvxLean/Meta/Util/SubExpr.lean
index 471b15e1..c4c16226 100644
--- a/CvxLean/Meta/Util/SubExpr.lean
+++ b/CvxLean/Meta/Util/SubExpr.lean
@@ -19,6 +19,14 @@ variable [MonadLiftT IO m]
 def withExpr (e : Expr) (x : m α) : m α := do
   withTheReader SubExpr (fun cfg => { cfg with expr := e, pos := cfg.pos }) x
 
+/-- Old version of `withBindingBody'`, needed for parsing.
+TODP: Why does `withBindingBody' (x := pure)` not work? -/
+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)
+
 end SubExpr
 
 end Lean.PrettyPrinter.Delaborator
diff --git a/CvxLean/Syntax/Minimization.lean b/CvxLean/Syntax/Minimization.lean
index 7808e967..8a3b78d1 100644
--- a/CvxLean/Syntax/Minimization.lean
+++ b/CvxLean/Syntax/Minimization.lean
@@ -195,7 +195,7 @@ partial def delabConstraints : DelabM (List (TSyntax ``Parser.constraint)) := do
 /-- Delaborate with variable names replaced. -/
 def withDomainBinding {α} [Inhabited α] (domain : Expr) (x : DelabM α) : DelabM α := do
   guard (← getExpr).isLambda
-  withBindingBody' (x := pure) `p fun p => do
+  withBindingBody'' `p fun p => do
     withDomainLocalDecls domain p fun xs _prs => do
       let e ← getExpr
       let e ← replaceProjections e p.fvarId! xs

From cbf5106a930a9441fc791fd9bfd6c74be04972ea Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Mon, 20 May 2024 15:22:03 +0100
Subject: [PATCH 09/14] fix: instance name was making `pre_dcp` fail!

---
 CvxLean/Tactic/PreDCP/Egg/ToExpr.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CvxLean/Tactic/PreDCP/Egg/ToExpr.lean b/CvxLean/Tactic/PreDCP/Egg/ToExpr.lean
index 46c91d64..2a35df13 100644
--- a/CvxLean/Tactic/PreDCP/Egg/ToExpr.lean
+++ b/CvxLean/Tactic/PreDCP/Egg/ToExpr.lean
@@ -103,7 +103,7 @@ partial def EggTree.toExpr (vars params : List String) : EggTree → MetaM Expr
       let t2 ← toExpr vars params t2
       return mkAppN
         (mkConst ``LE.le [levelZero])
-        #[(mkConst `Real), (mkConst `Real.instLEReal), t1, t2]
+        #[(mkConst `Real), (mkConst ``Real.instLE), t1, t2]
   -- Negation.
   | Tree.node "neg" #[t] => do
       let t ← toExpr vars params t

From 7f3967af9267210ed37120dd7f5b28df6c5a1079 Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Mon, 20 May 2024 15:26:45 +0100
Subject: [PATCH 10/14] test: fix expected output

---
 CvxLean/Test/PreDCP/DGP.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/CvxLean/Test/PreDCP/DGP.lean b/CvxLean/Test/PreDCP/DGP.lean
index 4e936af4..f833a135 100644
--- a/CvxLean/Test/PreDCP/DGP.lean
+++ b/CvxLean/Test/PreDCP/DGP.lean
@@ -29,10 +29,10 @@ time_cmd reduction red1/dcp1 : gp1 := by
   pre_dcp
 
 #print dcp1
--- optimization (x : ℝ)
---   minimize x
+-- optimization (u : ℝ)
+--   minimize u
 --   subject to
---     h2 : x * 2 ≤ log (10123 / 1000)
+--     h2 : u ≤ log (sqrt (10123 / 1000))
 
 solve dcp1
 

From a65cf985c4df52be82cc5479f15ceedef6a7ca93 Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Mon, 20 May 2024 15:28:31 +0100
Subject: [PATCH 11/14] fix: `Solution` is a type

---
 CvxLean/Test/Solve/Problems/Linear.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CvxLean/Test/Solve/Problems/Linear.lean b/CvxLean/Test/Solve/Problems/Linear.lean
index 4085d323..381f5701 100644
--- a/CvxLean/Test/Solve/Problems/Linear.lean
+++ b/CvxLean/Test/Solve/Problems/Linear.lean
@@ -35,7 +35,7 @@ example : linear2 =
       (fun p => 12 ≤ p.1 + p.2 ∧ 16 ≤ 2 * p.1 + p.2) :=
   rfl
 
-lemma linear2Solution : Solution linear2 :=
+def linear2Solution : Solution linear2 :=
   { point := ⟨4, 8⟩,
     isOptimal := by
       split_ands <;> try norm_num

From 7ac3d0fe80d7522dd5628033d840470b87c4151a Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Mon, 20 May 2024 15:34:38 +0100
Subject: [PATCH 12/14] fix: all case studies

---
 CvxLean/Examples/FittingSphere.lean          | 4 ++--
 CvxLean/Examples/VehicleSpeedScheduling.lean | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/CvxLean/Examples/FittingSphere.lean b/CvxLean/Examples/FittingSphere.lean
index b0a6246e..52886c3c 100644
--- a/CvxLean/Examples/FittingSphere.lean
+++ b/CvxLean/Examples/FittingSphere.lean
@@ -171,14 +171,14 @@ lemma optimal_convex_implies_optimal_t (hm : 0 < m) (c : Fin n → ℝ) (t : ℝ
     have h_t_eq := leastSquaresVec_optimal_eq_mean hm a t h_ls
     have h_c2_eq : ‖c‖ ^ 2 = (1 / m) * ∑ i : Fin m, ‖c‖ ^ 2 := by
       simp [sum_const]
-      field_simp; ring
+      field_simp
     have h_t_add_c2_eq : t + ‖c‖ ^ 2 = (1 / m) * ∑ i, ‖(x i) - c‖ ^ 2 := by
       rw [h_t_eq]; dsimp [mean]
       rw [h_c2_eq, mul_sum, mul_sum, mul_sum, ← sum_add_distrib]
       congr; funext i; rw [← mul_add]
       congr; simp [Vec.norm]
       rw [norm_sub_sq (𝕜 := ℝ) (E := Fin n → ℝ)]
-      congr
+      simp [a]; congr
     -- We use the result to establish that `t + ‖c‖ ^ 2` is non-negative.
     rw [← rpow_two, h_t_add_c2_eq]
     apply mul_nonneg (by norm_num)
diff --git a/CvxLean/Examples/VehicleSpeedScheduling.lean b/CvxLean/Examples/VehicleSpeedScheduling.lean
index 51d96420..fe01e8cd 100644
--- a/CvxLean/Examples/VehicleSpeedScheduling.lean
+++ b/CvxLean/Examples/VehicleSpeedScheduling.lean
@@ -152,7 +152,7 @@ def dₚ : Fin nₚ → ℝ :=
   ![1.9501, 1.2311, 1.6068, 1.4860, 1.8913, 1.7621, 1.4565, 1.0185, 1.8214, 1.4447]
 
 lemma dₚ_pos : StrongLT 0 dₚ := by
-  intro i; fin_cases i <;> (simp [dₚ]; norm_num)
+  intro i; fin_cases i <;> (dsimp [dₚ]; norm_num)
 
 @[optimization_param, reducible]
 def τminₚ : Fin nₚ → ℝ :=
@@ -177,7 +177,7 @@ lemma sminₚ_pos : StrongLT 0 sminₚ := by
 lemma sminₚ_nonneg : 0 ≤ sminₚ := le_of_strongLT sminₚ_pos
 
 lemma sminₚ_le_smaxₚ : sminₚ ≤ smaxₚ := by
-  intro i; fin_cases i <;> (simp [sminₚ, smaxₚ]; norm_num)
+  intro i; fin_cases i <;> (dsimp [sminₚ, smaxₚ]; norm_num)
 
 @[simp]
 lemma smaxₚ_nonneg : 0 ≤ smaxₚ := le_trans sminₚ_nonneg sminₚ_le_smaxₚ
@@ -190,7 +190,7 @@ lemma aₚ_nonneg : 0 ≤ aₚ := by unfold aₚ; norm_num
 
 @[simp]
 lemma aₚdₚ2_nonneg : 0 ≤ aₚ • (dₚ ^ (2 : ℝ)) := by
-  intros i; fin_cases i <;> (simp [aₚ, dₚ]; norm_num)
+  intros i; fin_cases i <;> (dsimp [aₚ, dₚ]; norm_num)
 
 @[optimization_param]
 def bₚ : ℝ := 6

From 178e510c0685b429a9dfce18c86c8c954ce038a7 Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Mon, 20 May 2024 15:37:57 +0100
Subject: [PATCH 13/14] fix: proofs in truss design

---
 CvxLean/Examples/TrussDesign.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/CvxLean/Examples/TrussDesign.lean b/CvxLean/Examples/TrussDesign.lean
index c573718e..eb3f6e7d 100644
--- a/CvxLean/Examples/TrussDesign.lean
+++ b/CvxLean/Examples/TrussDesign.lean
@@ -84,15 +84,15 @@ equivalence* eqv₁/trussDesignGP (hmin hmax wmin wmax Rmax σ F₁ F₂ : ℝ)
   -- Simplify objective function.
   rw_obj into (2 * A * sqrt (w ^ 2 + h ^ 2)) =>
     rw [rpow_two, sq_sqrt (h_A_div_2π_add_r2_nonneg r A c_r c_R_lb)]
-    ring_nf; field_simp; ring
+    ring_nf; field_simp
   -- Simplify constraint `c_F₁`.
   rw_constr c_F₁ into (F₁ * sqrt (w ^ 2 + h ^ 2) / (2 * h) ≤ σ * A) =>
     rw [rpow_two (sqrt (_ + r ^ 2)), sq_sqrt (h_A_div_2π_add_r2_nonneg r A c_r c_R_lb)]
-    rw [iff_eq_eq]; congr; ring_nf; field_simp; ring
+    rw [iff_eq_eq]; congr; ring_nf; field_simp
   -- Simplify constraint `c_F₂`.
   rw_constr c_F₂ into (F₂ * sqrt (w ^ 2 + h ^ 2) / (2 * w) ≤ σ * A) =>
     rw [rpow_two (sqrt (_ + r ^ 2)), sq_sqrt (h_A_div_2π_add_r2_nonneg r A c_r c_R_lb)]
-    rw [iff_eq_eq]; congr; ring_nf; field_simp; ring
+    rw [iff_eq_eq]; congr; ring_nf; field_simp
 
 #print trussDesignGP
 -- minimize 2 * A * sqrt (w ^ 2 + h ^ 2)
@@ -246,6 +246,7 @@ def wₚ_opt := sol.2.1
 def rₚ_opt := sol.2.2.1
 def Rₚ_opt := sol.2.2.2
 
+-- NOTE: These numbers may differ slighlty depending on the rewrites found by `pre_dcp`.
 #eval hₚ_opt -- 1.000000
 #eval wₚ_opt -- 1.000517
 #eval rₚ_opt -- 0.010162

From b8f7e283f950ede3b52875cf37fd1abc3ccb72b6 Mon Sep 17 00:00:00 2001
From: Ramon Fernandez Mir <rfernandezmir@gmail.com>
Date: Mon, 20 May 2024 15:51:02 +0100
Subject: [PATCH 14/14] style: make style chack pass

---
 CvxLean/Examples/FittingSphere.lean          | 2 +-
 CvxLean/Lib/Math/SchurComplement.lean        | 4 ++--
 CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean  | 3 +--
 CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean | 3 +--
 4 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/CvxLean/Examples/FittingSphere.lean b/CvxLean/Examples/FittingSphere.lean
index 52886c3c..b6c6700d 100644
--- a/CvxLean/Examples/FittingSphere.lean
+++ b/CvxLean/Examples/FittingSphere.lean
@@ -127,7 +127,7 @@ equivalence* eqv/fittingSphereT (n m : ℕ) (x : Fin m → Fin n → ℝ) : fitt
     apply ChangeOfVariablesBij.toEquivalence
       (fun (ct : (Fin n → ℝ) × ℝ) => (ct.1, sqrt (ct.2 + ‖ct.1‖ ^ 2))) covBij
     · rintro cr h; exact h
-    . rintro ct _; simp [covBij, sq_nonneg]
+    · rintro ct _; simp [covBij, sq_nonneg]
   rename_vars [c, t]
   rename_constrs [h₁, h₂]
   conv_constr h₁ => dsimp
diff --git a/CvxLean/Lib/Math/SchurComplement.lean b/CvxLean/Lib/Math/SchurComplement.lean
index fa2bacb7..e718ddf2 100644
--- a/CvxLean/Lib/Math/SchurComplement.lean
+++ b/CvxLean/Lib/Math/SchurComplement.lean
@@ -55,9 +55,9 @@ lemma IsHermitian.fromBlocks₁₁ [Fintype m] [DecidableEq m] {A : Matrix m m 
     apply hA.inv
   rw [isHermitian_fromBlocks_iff]
   constructor
-  . intro h
+  · intro h
     apply IsHermitian.sub h.2.2.2 hBAB
-  . intro h
+  · intro h
     refine' ⟨hA, rfl, conjTranspose_conjTranspose B, _⟩
     rw [← sub_add_cancel D]
     apply IsHermitian.add h hBAB
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean
index e48d27bc..31103e3e 100644
--- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean
+++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean
@@ -20,8 +20,7 @@ solutionEqualsAtom by
   rfl;
 feasibility (c_exp : by
   unfold expCone
-  simp
-  rw [Real.exp_log cond])
+  simp [Real.exp_log cond])
 optimality by
   intros y hy
   unfold expCone at c_exp
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean
index 3d146175..11715c13 100644
--- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean
+++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean
@@ -26,8 +26,7 @@ feasibility
     dsimp
     unfold rotatedSoCone
     refine ⟨?_, cond, by norm_num⟩
-    simp
-    rw [sq_sqrt cond])
+    simp [sq_sqrt cond])
 optimality by
   intros y hy
   unfold rotatedSoCone at c1