chore: bump to v4.8.0-rc1 and fix proofs (#33)

* chore: bump to v4.8.0-rc1

* chore: update lake manifest

* fix: `OfScientific` instances

* wip: fixing `Lib` errors due to new `mathlib`

* fix: deprecated `SchedulerM`

* wip: fixing more errors in proofs

* fix: all update-related errors fixed, mainly atoms

* fix: syntax issues because of domain binding

* fix: instance name was making `pre_dcp` fail!

* test: fix expected output

* fix: `Solution` is a type

* fix: all case studies

* fix: proofs in truss design

* style: make style chack pass

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

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

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,25 +54,25 @@ 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
 
 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
 
 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

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

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

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

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]

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

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

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

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]
 

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]

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,18 +53,17 @@ 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]
     erw [Basis.toMatrix_apply, OrthonormalBasis.coe_toBasis_repr_apply,
       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