diff --git a/ClassicalInfo/Channel.lean b/ClassicalInfo/Channel.lean
index 2ea36c6..edae9f1 100644
--- a/ClassicalInfo/Channel.lean
+++ b/ClassicalInfo/Channel.lean
@@ -49,22 +49,23 @@ def product : Channel (A × C) (B × D) :=
  output distribution `Distribution O`, and this process is applied
  independently on each symbol in the list. -/
 structure DMChannel where
-  symb_dist : I → Distribution O
+  symb_dist : I → ProbDistribution O
 
 namespace DMChannel
 
 /-- Apply a discrete memoryless channel to an n-character string. -/
-def on_fin (C : DMChannel I O) {n : ℕ} (is : Fin n → I) : Distribution (Fin n → O) :=
-  ⟨fun os ↦ ∏ k, C.symb_dist (is k) (os k), by
-    -- change ∑ os in Fintype.piFinset fun x => (Finset.univ : Finset O), ∏ k : Fin n, ((C.symb_dist (is k)) (os k) : ℝ) = 1
-    -- have : ∀i, Finset.sum Finset.univ (C.symb_dist i) = 1 :=
-    --   fun i ↦ Distribution.prop <| C.symb_dist i
-    -- rw [Finset.sum_prod_piFinset]
-    -- simp [this]
-    sorry⟩
+def on_fin (C : DMChannel I O) {n : ℕ} (is : Fin n → I) : ProbDistribution (Fin n → O) :=
+  ProbDistribution.mk' (fun os ↦ ∏ k, (C.symb_dist (is k) (os k) : ℝ))
+    (fun _ ↦ Finset.prod_nonneg fun k _ ↦ Prob.zero_le_coe)
+    (by
+      have h := Finset.sum_prod_piFinset (Finset.univ : Finset O)
+        (fun (k : Fin n) (j : O) ↦ ((C.symb_dist (is k)) j : ℝ))
+      simp only [Fintype.piFinset_univ] at h
+      simp only [h]
+      exact Finset.prod_eq_one fun k _ ↦ ProbDistribution.normalized (C.symb_dist (is k)))
 
 /-- Apply a discrete memoryless channel to a list. -/
-def on_list (C : DMChannel I O) (is : List I) : Distribution (Fin (is.length) → O) :=
-  C.on_fin is.get
+def on_list (C : DMChannel I O) (is : List I) : ProbDistribution (Fin (is.length) → O) :=
+  on_fin I O C is.get
 
 end DMChannel
diff --git a/QuantumInfo/Finite/CPTPMap/Dual.lean b/QuantumInfo/Finite/CPTPMap/Dual.lean
index e3d5afc..bc6dc66 100644
--- a/QuantumInfo/Finite/CPTPMap/Dual.lean
+++ b/QuantumInfo/Finite/CPTPMap/Dual.lean
@@ -54,7 +54,8 @@ theorem _root_.Matrix.PosSemidef.trace_mul_nonneg {n : Type*} [Fintype n] [Decid
     0 ≤ (A * B).trace := by
   open scoped Matrix in
   obtain ⟨sqrtB, rfl⟩ : ∃ sqrtB : Matrix n n 𝕜, B = sqrtBᴴ * sqrtB := by
-    exact Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp hB;
+    open MatrixOrder in
+    exact CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hB.nonneg
   simp only [← Matrix.mul_assoc, ← Matrix.trace_mul_comm sqrtB]
   have h : (sqrtB * A * sqrtBᴴ).PosSemidef := by
     convert hA.conjTranspose_mul_mul_same sqrtBᴴ using 1
diff --git a/QuantumInfo/Finite/CPTPMap/Unbundled.lean b/QuantumInfo/Finite/CPTPMap/Unbundled.lean
index 56255c9..2dda071 100644
--- a/QuantumInfo/Finite/CPTPMap/Unbundled.lean
+++ b/QuantumInfo/Finite/CPTPMap/Unbundled.lean
@@ -352,10 +352,12 @@ theorem kron_kronecker_const {C : Matrix d d R} (h : C.PosSemidef) {h₁ h₂ :
   intros n x hx
   have h_kronecker_pos : (x ⊗ₖ C).PosSemidef := by
     -- Since $x$ and $C$ are positive semidefinite, there exist matrices $U$ and $V$ such that $x = U^*U$ and $C = V^*V$.
-    obtain ⟨U, hU⟩ : ∃ U : Matrix (A × Fin n) (A × Fin n) R, x = star U * U :=
-      Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp hx
-    obtain ⟨V, hV⟩ : ∃ V : Matrix d d R, C = star V * V :=
-      Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp h
+    obtain ⟨U, hU⟩ : ∃ U : Matrix (A × Fin n) (A × Fin n) R, x = star U * U := by
+      classical
+      open MatrixOrder in exact CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx.nonneg
+    obtain ⟨V, hV⟩ : ∃ V : Matrix d d R, C = star V * V := by
+      classical
+      open MatrixOrder in exact CStarAlgebra.nonneg_iff_eq_star_mul_self.mp h.nonneg
     -- $W = (U \otimes V)^* (U \otimes V)$ is positive semidefinite.
     have hW_pos : (U ⊗ₖ V).conjTranspose * (U ⊗ₖ V) = x ⊗ₖ C := by
       rw [Matrix.kroneckerMap_conjTranspose, ← Matrix.mul_kronecker_mul]
@@ -596,7 +598,9 @@ theorem conj_isCompletelyPositive (M : Matrix B A R) : (conj M).IsCompletelyPosi
       simp +contextual [ eq_comm ];
     simp only [ h_inner ];
     simpa only [ mul_assoc, mul_comm, mul_left_comm ] using h_reindex
-  obtain ⟨m', rfl⟩ := Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp h
+  obtain ⟨m', rfl⟩ := by
+    classical
+    open MatrixOrder in exact CStarAlgebra.nonneg_iff_eq_star_mul_self.mp h.nonneg
   convert Matrix.posSemidef_conjTranspose_mul_self (m' * (M ⊗ₖ 1 : Matrix (B × Fin n) (A × Fin n) R).conjTranspose) using 1
   simp only [Matrix.conjTranspose_mul, Matrix.conjTranspose_conjTranspose, Matrix.mul_assoc]
   rw [Matrix.mul_assoc, Matrix.mul_assoc]
diff --git a/QuantumInfo/Finite/POVM.lean b/QuantumInfo/Finite/POVM.lean
index f57c4ce..1e447a1 100644
--- a/QuantumInfo/Finite/POVM.lean
+++ b/QuantumInfo/Finite/POVM.lean
@@ -112,7 +112,7 @@ theorem measurementMap_apply_hermitianMat (Λ : POVM X d) (m : HermitianMat d 
   congr!
   ext i j
   simp only [HermitianMat.diagonal, mat_mk, diagonal_apply, single, of_apply]
-  split_ifs <;> (try grind) <;> norm_num
+  split_ifs <;> grind
 
 /-- A POVM leads to a distribution of outcomes on any given mixed state ρ. -/
 def measure (Λ : POVM X d) (ρ : MState d) : ProbDistribution X := .mk'
diff --git a/QuantumInfo/ForMathlib/ContinuousLinearMap.lean b/QuantumInfo/ForMathlib/ContinuousLinearMap.lean
index 205d701..f43c904 100644
--- a/QuantumInfo/ForMathlib/ContinuousLinearMap.lean
+++ b/QuantumInfo/ForMathlib/ContinuousLinearMap.lean
@@ -3,10 +3,8 @@ Copyright (c) 2025 Alex Meiburg. All rights reserved.
 Released under MIT license as described in the file LICENSE.
 Authors: Alex Meiburg
 -/
---For the first three lemmas
 import Mathlib.Topology.Algebra.Module.LinearMap
 
---For the third lemma
 import Mathlib.Analysis.CStarAlgebra.Classes
 import Mathlib.Analysis.InnerProductSpace.Spectrum
 import Mathlib.Order.CompletePartialOrder
@@ -17,16 +15,6 @@ variable {R S : Type*} [Semiring R] [Semiring S] (σ : R →+* S) (M M₂ : Type
 variable [TopologicalSpace M] [AddCommMonoid M] [TopologicalSpace M₂] [AddCommMonoid M₂]
 variable [Module R M] [Module S M₂]
 
---These two theorems might look a bit silly as aliases of `LinearMap.____`, but they don't `simp` on their
---TODO: I think we can remove these now that we've bumped to Lean 4.28.0
-@[simp]
-theorem range_zero [RingHomSurjective σ] : (0 : M →SL[σ] M₂).range = ⊥ := by
-  simp
-
-@[simp]
-theorem ker_zero : (0 : M →SL[σ] M₂).ker = ⊤ := by
-  simp
-
 theorem ker_mk (f : M →ₛₗ[σ] M₂) (hf : Continuous f.toFun) :
     (ContinuousLinearMap.mk f hf).ker = LinearMap.ker f := by
   rfl
diff --git a/QuantumInfo/ForMathlib/HermitianMat/Basic.lean b/QuantumInfo/ForMathlib/HermitianMat/Basic.lean
index 9dc2f49..0ae75a5 100644
--- a/QuantumInfo/ForMathlib/HermitianMat/Basic.lean
+++ b/QuantumInfo/ForMathlib/HermitianMat/Basic.lean
@@ -726,7 +726,7 @@ theorem conj_ne_zero {A : HermitianMat d 𝕜} {M : Matrix d₂ d 𝕜} (hA : A
 theorem conj_ne_zero_iff {A : HermitianMat d 𝕜} {M : Matrix d₂ d 𝕜}
     (h : LinearMap.ker M.toEuclideanLin ≤ A.ker) : A.conj M ≠ 0 ↔ A ≠ 0  := by
   refine ⟨?_, (conj_ne_zero · h)⟩
-  intro h rfl; simp at h--should be grind[= map_zero] but I don't know why. TODO.
+  intro h rfl; grind
 
 section spectrum
 
diff --git a/QuantumInfo/ForMathlib/HermitianMat/Inner.lean b/QuantumInfo/ForMathlib/HermitianMat/Inner.lean
index c9910da..ded7615 100644
--- a/QuantumInfo/ForMathlib/HermitianMat/Inner.lean
+++ b/QuantumInfo/ForMathlib/HermitianMat/Inner.lean
@@ -243,7 +243,7 @@ private theorem inner_zero_iff_aux_lemma [DecidableEq n] (hA₁ : A.mat.PosSemid
             simp_all only [Matrix.zero_apply, map_zero, mul_zero, add_zero, Finset.sum_const_zero]
         exact h_trace_zero_iff _;
       convert h_trace_zero_iff using 3
-      simp [ hC, hD, Matrix.mul_assoc ];
+      simp [ Matrix.mul_assoc ];
       rw [ ← Matrix.trace_mul_comm ]
       have h_trace_cyclic : Matrix.trace (D.conjTranspose * D * C.conjTranspose * C) = Matrix.trace (C * D.conjTranspose * D * C.conjTranspose) := by
         rw [ ← Matrix.trace_mul_comm ]
@@ -269,7 +269,7 @@ private theorem inner_zero_iff_aux_lemma [DecidableEq n] (hA₁ : A.mat.PosSemid
       ext i j
       specialize hAB_zero (EuclideanSpace.single j 1)
       have h1 := hAB_zero
-      simp only [LinearMap.mem_ker, Matrix.toEuclideanLin, Matrix.toLpLin_apply, Matrix.mulVec_mulVec] at h1
+      simp only [Matrix.toEuclideanLin, Matrix.toLpLin_apply, Matrix.mulVec_mulVec] at h1
       have h2 := congr_fun (congrArg WithLp.ofLp h1) i
       simp only [WithLp.ofLp_toLp, WithLp.ofLp_zero, EuclideanSpace.single] at h2
       simpa [Matrix.mul_apply, Matrix.mulVec, dotProduct, Pi.single_apply] using h2
@@ -495,8 +495,7 @@ theorem norm_one : ‖(1 : HermitianMat d 𝕜)‖ = √(Fintype.card d : ℝ) :
   rw [norm_eq_sqrt_real_inner (F := HermitianMat d 𝕜)]
   congr 1
   simp only [inner_def, mat_one, Matrix.one_apply, Matrix.trace, Matrix.diag_apply,
-    Matrix.mul_apply, star_one, one_mul, Finset.sum_ite_eq', Finset.mem_univ, ↑reduceIte,
-    map_one, Finset.sum_const, Finset.card_univ, smul_eq_mul, mul_one]
+    ↑reduceIte, Finset.sum_const, Finset.card_univ, mul_one]
   simp [selfadjMap]
 
 theorem norm_eq_trace_sq : ‖A‖ ^ 2 = (A.mat ^ 2).trace := by
diff --git a/QuantumInfo/ForMathlib/HermitianMat/Jordan.lean b/QuantumInfo/ForMathlib/HermitianMat/Jordan.lean
index 0a415e0..bec0b60 100644
--- a/QuantumInfo/ForMathlib/HermitianMat/Jordan.lean
+++ b/QuantumInfo/ForMathlib/HermitianMat/Jordan.lean
@@ -130,8 +130,8 @@ scoped instance : NonUnitalNonAssocRing (HermitianMat d 𝕜) where
 
 variable [Invertible (2 : 𝕜)] [DecidableEq d]
 
---TODO: Upgrade this to NonAssocCommRing, see #28604 in Mathlib
-scoped instance : NonAssocRing (HermitianMat d 𝕜) where
+scoped instance : NonAssocCommRing (HermitianMat d 𝕜) where
+  mul_comm := HermitianMat.symmMul_comm
 
 end field
 
diff --git a/QuantumInfo/ForMathlib/HermitianMat/LogExp.lean b/QuantumInfo/ForMathlib/HermitianMat/LogExp.lean
index b2e0f39..df5c10e 100644
--- a/QuantumInfo/ForMathlib/HermitianMat/LogExp.lean
+++ b/QuantumInfo/ForMathlib/HermitianMat/LogExp.lean
@@ -135,8 +135,9 @@ The inverse function is operator antitone for positive definite matrices.
 open ComplexOrder in
 theorem inv_antitone (hA : A.mat.PosDef) (h : A ≤ B) : B⁻¹ ≤ A⁻¹ := by
   -- Since $B - A$ is positive semidefinite, we can write it as $C^*C$ for some matrix $C$.
-  obtain ⟨C, hC⟩ : ∃ C : Matrix d d 𝕜, B.mat - A.mat = C.conjTranspose * C :=
-    Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp h
+  obtain ⟨C, hC⟩ : ∃ C : Matrix d d 𝕜, B.mat - A.mat = C.conjTranspose * C := by
+    open MatrixOrder in
+    exact CStarAlgebra.nonneg_iff_eq_star_mul_self.mp (le_iff.mp h).nonneg
   -- Using the fact that $B = A + C^*C$, we can write $B^{-1}$ as $(A + C^*C)^{-1}$.
   have h_inv_posDef : (1 + C * A.mat⁻¹ * C.conjTranspose).PosDef := by
     exact Matrix.PosDef.one.add_posSemidef (hA.inv.posSemidef.mul_mul_conjTranspose_same C)
diff --git a/QuantumInfo/ForMathlib/HermitianMat/NonSingular.lean b/QuantumInfo/ForMathlib/HermitianMat/NonSingular.lean
index 9924be1..7b4c6f9 100644
--- a/QuantumInfo/ForMathlib/HermitianMat/NonSingular.lean
+++ b/QuantumInfo/ForMathlib/HermitianMat/NonSingular.lean
@@ -100,7 +100,7 @@ theorem nonSingular_iff_ker_bot : NonSingular A ↔ A.ker = ⊥ := by
     have hm : (WithLp.toLp 2 y) ∈ A.ker := (mem_ker_iff_mulVec_zero A _).mpr hy
     rw [h] at hm
     have := (Submodule.mem_bot (R := 𝕜)).mp hm
-    simp [WithLp.toLp] at this
+    simp at this
     exact this
   specialize @h_inj x 0
   simp_all
diff --git a/QuantumInfo/ForMathlib/HermitianMat/Proj.lean b/QuantumInfo/ForMathlib/HermitianMat/Proj.lean
index 93e1ff1..5cf661d 100644
--- a/QuantumInfo/ForMathlib/HermitianMat/Proj.lean
+++ b/QuantumInfo/ForMathlib/HermitianMat/Proj.lean
@@ -94,15 +94,15 @@ theorem projector_eq_sum_rankOne (b : OrthonormalBasis ι 𝕜 S) :
   unfold projector;
   ext i j;
   field_simp;
-  simp +decide [ Matrix.vecMulVec, LinearMap.toMatrix_apply ];
+  simp +decide [ Matrix.vecMulVec ];
   -- By definition of orthogonal projection, we can write the projection of $e_j$ onto $S$ as $\sum_{k} \langle e_j, b_k \rangle b_k$.
   have h_proj : ∀ j : n, S.orthogonalProjection (EuclideanSpace.single j 1) = ∑ k, (star (b k |>.1 j)) • (b k |>.1) := by
     intro j
     have h_proj : S.orthogonalProjection (EuclideanSpace.single j 1) = ∑ k, (inner 𝕜 (b k |>.1) (EuclideanSpace.single j 1)) • (b k |>.1) := by
       convert b.sum_repr ( S.orthogonalProjection ( EuclideanSpace.single j 1 ) ) using 1;
       constructor <;> intro h <;> simp_all +decide [ Subtype.ext_iff, b.repr_apply_apply ];
-    convert h_proj using 3 ; simp +decide [ inner, EuclideanSpace.inner_single_right ];
-  convert congr_arg ( fun x : EuclideanSpace ( _ ) n => x i ) ( h_proj j ) using 1 <;> simp +decide [ LinearMap.toMatrix_apply, Matrix.mulVec, dotProduct ];
+    convert h_proj using 3 ; simp +decide [ inner ];
+  convert congr_arg ( fun x : EuclideanSpace ( _ ) n => x i ) ( h_proj j ) using 1 ; simp +decide;
   simp +decide [ Matrix.sum_apply, mul_comm ]
 
 /--
@@ -116,32 +116,32 @@ lemma projector_support_eq_sum : A.supportProj.mat =
     · intro x hx;
       -- By definition of $A.support$, we know that $x$ is in the orthogonal complement of the kernel of $A$.
       have h_orthogonal_complement : x ∈ (A.ker : Submodule (𝕜) (EuclideanSpace (𝕜) n))ᗮ := by
-        convert hx using 1;
-        exact?;
+        convert hx using 1
+        exact ker_orthogonal_eq_support A
       -- By definition of $A.ker$, we know that $x$ is orthogonal to all eigenvectors with zero eigenvalues.
       have h_orthogonal_zero_eigenvalues : ∀ i, A.H.eigenvalues i = 0 → inner (𝕜) (A.H.eigenvectorBasis i) x = 0 := by
         intro i hi
         have h_eigenvector_zero : A.mat.mulVec (A.H.eigenvectorBasis i) = 0 := by
           have := A.H.mulVec_eigenvectorBasis i; aesop;
-        convert h_orthogonal_complement ( A.H.eigenvectorBasis i ) _ using 1;
-        exact?;
+        convert h_orthogonal_complement ( A.H.eigenvectorBasis i ) _ using 1
+        exact (mem_ker_iff_mulVec_zero A ((H A).eigenvectorBasis i)).mpr h_eigenvector_zero
       -- By definition of $A.ker$, we know that $x$ can be written as a linear combination of eigenvectors with non-zero eigenvalues.
       have h_decomp : x = ∑ i, (inner (𝕜) (A.H.eigenvectorBasis i) x) • A.H.eigenvectorBasis i := by
-        exact?;
+        exact Eq.symm (OrthonormalBasis.sum_repr' (H A).eigenvectorBasis x)
       rw [ h_decomp ];
-      exact Submodule.sum_mem _ fun i _ => if hi : A.H.eigenvalues i = 0 then by simp +decide [ hi, h_orthogonal_zero_eigenvalues i hi ] else Submodule.smul_mem _ _ ( Submodule.subset_span ⟨ i, hi, rfl ⟩ );
+      exact Submodule.sum_mem _ fun i _ => if hi : A.H.eigenvalues i = 0 then by simp +decide [ h_orthogonal_zero_eigenvalues i hi ] else Submodule.smul_mem _ _ ( Submodule.subset_span ⟨ i, hi, rfl ⟩ );
     · rw [ Submodule.span_le, Set.image_subset_iff ];
       intro i hi;
       simp_all +decide [ HermitianMat.support ];
       use (1 / A.H.eigenvalues i) • A.H.eigenvectorBasis i;
-      convert congr_arg ( fun x => ( 1 / A.H.eigenvalues i ) • x ) ( A.H.mulVec_eigenvectorBasis i ) using 1 ; simp +decide [ hi, Matrix.mulVec_smul ];
-      simp +decide [ funext_iff, Matrix.mulVec, dotProduct ];
-      exact?;
+      convert congr_arg ( fun x => ( 1 / A.H.eigenvalues i ) • x ) ( A.H.mulVec_eigenvectorBasis i ) using 1 ; simp +decide [ hi ];
+      simp +decide [ funext_iff, Matrix.mulVec, dotProduct ]
+      exact PiLp.ext_iff
   have h_orthonormal_basis : ∃ b : OrthonormalBasis {i : n | A.H.eigenvalues i ≠ 0} (𝕜) (Submodule.span (𝕜) (Set.image (fun i => A.H.eigenvectorBasis i) {i | A.H.eigenvalues i ≠ 0})), ∀ i, b i = A.H.eigenvectorBasis i := by
     refine' ⟨ _, _ ⟩;
     refine' OrthonormalBasis.mk _ _;
     use fun i => ⟨ A.H.eigenvectorBasis i, Submodule.subset_span ( Set.mem_image_of_mem _ i.2 ) ⟩;
-    all_goals simp +decide [ Orthonormal, Subtype.ext_iff ];
+    all_goals simp +decide [ Orthonormal ];
     · intro i j hij; have := A.H.eigenvectorBasis.orthonormal; simp_all +decide [ orthonormal_iff_ite ] ;
       exact fun h => hij <| Subtype.ext h;
     · rw [ Submodule.eq_top_iff' ];
diff --git a/QuantumInfo/ForMathlib/HermitianMat/Schatten.lean b/QuantumInfo/ForMathlib/HermitianMat/Schatten.lean
index b8d05ba..7a308db 100644
--- a/QuantumInfo/ForMathlib/HermitianMat/Schatten.lean
+++ b/QuantumInfo/ForMathlib/HermitianMat/Schatten.lean
@@ -42,12 +42,12 @@ lemma schattenNorm_nonneg (A : Matrix d d ℂ) (p : ℝ) :
     0 ≤ schattenNorm A p := by
   by_cases hp : p = 0 <;> simp +decide [ *, schattenNorm ];
   by_cases h₁ : 0 ≤ RCLike.re ( Matrix.trace ( Matrix.IsHermitian.cfc ( Matrix.isHermitian_mul_conjTranspose_self A.conjTranspose ) fun x => x ^ ( p / 2 ) ) ) <;> simp_all +decide [ Real.rpow_nonneg ];
-  contrapose! h₁; simp_all +decide [ mul_comm, Matrix.trace ] ; ring_nf; norm_num [ Real.exp_nonneg, Real.log_nonneg ] ; (
+  contrapose! h₁; simp_all +decide [ Matrix.trace ] ; ring_nf; norm_num [ Real.exp_nonneg, Real.log_nonneg ] ; (
   refine' Finset.sum_nonneg fun i _ => _ ; norm_num [ Matrix.IsHermitian.cfc ] ; ring_nf ; norm_num [ Real.exp_nonneg, Real.log_nonneg ] ; (
   simp +decide [ Matrix.mul_apply, Matrix.diagonal ] ; ring_nf ; norm_num [ Real.exp_nonneg, Real.log_nonneg ] ; (
-  exact Finset.sum_nonneg fun _ _ => add_nonneg ( mul_nonneg ( sq_nonneg _ ) ( Real.rpow_nonneg ( by
-    exact? ) _ ) ) ( mul_nonneg ( Real.rpow_nonneg ( by
-    exact? ) _ ) ( sq_nonneg _ ) ))));
+  exact Finset.sum_nonneg fun _ _ => add_nonneg ( mul_nonneg ( sq_nonneg _ ) ( Real.rpow_nonneg (
+    Matrix.eigenvalues_conjTranspose_mul_self_nonneg A _) _ ) ) ( mul_nonneg ( Real.rpow_nonneg (
+    Matrix.eigenvalues_conjTranspose_mul_self_nonneg A _) _ ) ( sq_nonneg _ ) ))));
 
 lemma schattenNorm_pow_eq
   (A : HermitianMat d ℂ) (hA : 0 ≤ A) (p k : ℝ) (hp : 0 < p) (hk : 0 < k) :
@@ -97,9 +97,9 @@ For nonneg eigenvalue λ and p > 0, (√λ)^p = λ^{p/2}.
 PROVIDED SOLUTION
 We have √y = y^{1/2} (by Real.sqrt_eq_rpow). So (√y)^p = (y^{1/2})^p = y^{(1/2)·p} = y^{p/2} by Real.rpow_mul (since y ≥ 0). Use rw [Real.sqrt_eq_rpow, ← Real.rpow_mul hy]; ring_nf.
 -/
-lemma sqrt_rpow_eq_rpow_half {y p : ℝ} (hy : 0 ≤ y) (hp : 0 < p) :
+lemma sqrt_rpow_eq_rpow_half {y p : ℝ} (hy : 0 ≤ y) (_hp : 0 < p) :
     Real.sqrt y ^ p = y ^ (p / 2) := by
-  rw [ Real.sqrt_eq_rpow, ← Real.rpow_mul hy ] ; ring
+  rw [ Real.sqrt_eq_rpow, ← Real.rpow_mul hy ] ; ring_nf
 
 /-
 PROBLEM
@@ -129,7 +129,7 @@ lemma schattenNorm_rpow_eq_sum_singularValues (A : Matrix d d ℂ) {p : ℝ} (hp
   · convert schattenNorm_trace_as_eigenvalue_sum A p using 1
     generalize_proofs at *;
     refine' Finset.sum_congr rfl fun i _ => _;
-    unfold singularValues; rw [ Real.sqrt_eq_rpow, ← Real.rpow_mul ( _ ) ] ; ring;
+    unfold singularValues; rw [ Real.sqrt_eq_rpow, ← Real.rpow_mul ( _ ) ] ; ring_nf;
     simp +zetaDelta at *;
     exact Matrix.eigenvalues_conjTranspose_mul_self_nonneg A i;
   · have h_nonneg : ∀ i : d, 0 ≤ ((Matrix.isHermitian_mul_conjTranspose_self A.conjTranspose).eigenvalues i) ^ (p / 2) := by
diff --git a/QuantumInfo/ForMathlib/IsMaximalSelfAdjoint.lean b/QuantumInfo/ForMathlib/IsMaximalSelfAdjoint.lean
index 912ebba..adf8d09 100644
--- a/QuantumInfo/ForMathlib/IsMaximalSelfAdjoint.lean
+++ b/QuantumInfo/ForMathlib/IsMaximalSelfAdjoint.lean
@@ -3,7 +3,7 @@ Copyright (c) 2025 Alex Meiburg. All rights reserved.
 Released under MIT license as described in the file LICENSE.
 Authors: Alex Meiburg
 -/
-import Mathlib.Analysis.Matrix
+import Mathlib.Analysis.Matrix.Normed
 
 /- We want to have `HermitianMat.trace` give 𝕜 when 𝕜 is already a TrivialStar field, but give the "clean" type
 otherwise -- for instance, ℝ when the input field is ℂ. This typeclass lets us do so. -/
diff --git a/QuantumInfo/ForMathlib/Isometry.lean b/QuantumInfo/ForMathlib/Isometry.lean
index 0a9f177..e6bfe81 100644
--- a/QuantumInfo/ForMathlib/Isometry.lean
+++ b/QuantumInfo/ForMathlib/Isometry.lean
@@ -287,8 +287,8 @@ theorem Matrix.commute_euclideanLin (hAB : Commute A B) :
   rw [commute_iff_eq] at hAB ⊢
   ext v i
   convert congr(($hAB).mulVec (WithLp.ofLp v) i) using 0
-  simp only [Module.End.mul_apply, ← Matrix.mulVec_mulVec];
-  simp only [← Matrix.ofLp_toEuclideanLin_apply]
+  simp only [Module.End.mul_apply, ← Matrix.mulVec_mulVec, Matrix.toEuclideanLin,
+    Matrix.ofLp_toLpLin, Matrix.toLin'_apply]
 
 section commute_module
 open Module.End
@@ -527,13 +527,13 @@ theorem star_shared_mul_A_mul_IsDiag : IsDiag
   intro i j hij;
   have := @mulVec_sharedEigenbasisA d;
   specialize this hA hB hAB j;
-  replace this := congr_arg ( fun x => star ( ( sharedEigenbasis hA hB hAB i ).ofLp ) ⬝ᵥ x ) this ; simp_all +decide [ Matrix.mulVec, dotProduct, Finset.mul_sum _ _ _, mul_assoc, mul_comm, mul_left_comm ];
+  replace this := congr_arg ( fun x => star ( ( sharedEigenbasis hA hB hAB i ).ofLp ) ⬝ᵥ x ) this ; simp_all +decide [ Matrix.mulVec, dotProduct, Finset.mul_sum _ _ _, mul_assoc, mul_comm ];
   convert this using 1;
-  · simp +decide [ Matrix.mul_apply, mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _, Finset.sum_mul ];
+  · simp +decide [ Matrix.mul_apply, mul_assoc, mul_comm, Finset.sum_mul ];
     congr! 3;
   · have := ( sharedEigenbasis hA hB hAB ).orthonormal;
     rw [ orthonormal_iff_ite ] at this;
-    simp_all +decide [ inner, Finset.mul_sum _ _ _, mul_assoc, mul_comm, mul_left_comm ];
+    simp_all +decide [ inner ];
     rw [ ← Finset.smul_sum, this i j, if_neg hij, smul_zero ]
 
 /-- Analogous to `Matrix.IsHermitian.star_mul_self_mul_eq_diagonal` for the shared basis. -/
@@ -544,7 +544,7 @@ theorem star_shared_mul_B_mul_IsDiag : IsDiag
   apply Matrix.toEuclideanLin.injective
   apply (EuclideanSpace.basisFun d 𝕜).toBasis.ext
   intro i
-  simp only [toEuclideanLin_apply, OrthonormalBasis.coe_toBasis, EuclideanSpace.basisFun_apply,
+  simp only [toLpLin_apply, OrthonormalBasis.coe_toBasis, EuclideanSpace.basisFun_apply,
     EuclideanSpace.ofLp_single, ← mulVec_mulVec, sharedEigenvectorUnitary_mulVec, ← mulVec_mulVec,
     Matrix.diagonal_mulVec_single, mul_one]
   apply PiLp.ext
@@ -566,14 +566,14 @@ theorem star_shared_mul_B_mul_IsDiag : IsDiag
     · exact Matrix.mem_unitaryGroup_iff.mp ( Matrix.sharedEigenvectorUnitary hA hB hAB ).2;
   simp_all [ Matrix.mulVec, funext_iff ];
   simp_all [ Matrix.mul_apply, dotProduct ];
-  by_cases hij : i = j <;> simp +decide [ hij, h_simp2 ];
+  by_cases hij : i = j <;> simp +decide [ hij ];
   · simp +decide [ hij, Pi.single_apply, Matrix.mulVec, dotProduct ];
     simp +decide only [Finset.mul_sum _ _ _, mul_left_comm];
-    rw [ Finset.sum_comm ] ; simp +decide [ mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _ ] ;
+    rw [ Finset.sum_comm ] ; simp +decide [ mul_comm, mul_left_comm, Finset.mul_sum _ _ _ ] ;
     congr! 3;
   · simp_all +decide [ mul_comm, Matrix.mulVec, dotProduct ];
-    simp_all +decide [ mul_comm, Finset.mul_sum _ _ _, Finset.sum_mul ];
-    rw [ Finset.sum_comm ] ; simp_all +decide [ mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum _ _ _ ] ;
+    simp_all +decide [ mul_comm, Finset.mul_sum _ _ _ ];
+    rw [ Finset.sum_comm ] ; simp_all +decide [ mul_assoc, mul_left_comm ] ;
 
 end Matrix.SharedEigenbasis
 
diff --git a/QuantumInfo/ForMathlib/Matrix.lean b/QuantumInfo/ForMathlib/Matrix.lean
index 2650cef..154345f 100644
--- a/QuantumInfo/ForMathlib/Matrix.lean
+++ b/QuantumInfo/ForMathlib/Matrix.lean
@@ -9,7 +9,9 @@ import Mathlib.Analysis.CStarAlgebra.Matrix
 import Mathlib.Analysis.Matrix.Order
 import Mathlib.Data.Multiset.Functor --Can't believe I'm having to import this
 import Mathlib.LinearAlgebra.Matrix.Kronecker
-import Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus
+import Mathlib.Analysis.SpecialFunctions.Bernstein
+import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
+import Mathlib.Tactic.NormNum.GCD
 import Mathlib.LinearAlgebra.Matrix.PosDef
 import Mathlib.LinearAlgebra.Matrix.IsDiag
 
@@ -1139,18 +1141,7 @@ theorem PosDef.zero_lt {n : Type*} [Nonempty n] [Fintype n] {A : Matrix n n ℂ}
   apply lt_of_le_of_ne
   · replace hA := hA.posSemidef
     rwa [Matrix.nonneg_iff_posSemidef]
-  · rintro rfl
-    --wtf do better. TODO
-    have : ¬(0 < 0) := by trivial
-    classical rw [← Matrix.posDef_natCast_iff (n := n) (R := ℂ)] at this
-    revert hA
-    convert this
-    ext; simp
-    trans ((0 : ℕ) : ℂ)
-    · simp
-    classical
-    change _ = ite _ _ _
-    simp
+  · rintro rfl; exact absurd (hA.diag_pos (i := Classical.arbitrary n)) (by simp)
 
 
 lemma IsHermitian.spectrum_eq_image_eigenvalues [Fintype n] {A : Matrix n n ℂ} (hA : A.IsHermitian) :
@@ -1327,7 +1318,7 @@ theorem IsHermitian.spectrum_subset_Ici_of_sub {d 𝕜 : Type*} [Fintype d] [Dec
             Unitary.conjStarAlgAut_apply]
           simp [ mul_comm, mul_left_comm, Algebra.smul_def ]
           congr! 1
-          simp [Algebra.algebraMap_eq_smul_one, mul_assoc]
+          simp [Algebra.algebraMap_eq_smul_one]
         -- Substitute the decomposition of $A$ into the expression $(star v ⬝ᵥ (A.mulVec v))$.
         have h_subst : (star v ⬝ᵥ (A.mulVec v)) = ∑ i, (hA.eigenvalues i) * (star v ⬝ᵥ (Matrix.mulVec (Matrix.of (fun j k => (hA.eigenvectorBasis i j) * (star (hA.eigenvectorBasis i k)))) v)) := by
           -- Substitute the decomposition of $A$ into the expression $(star v ⬝ᵥ (A.mulVec v))$ and use the linearity of matrix multiplication.
@@ -1550,7 +1541,9 @@ theorem PosSemidef.piProd [RCLike R] (hA : ∀ i, (A i).PosSemidef) :
     have h_decomp : ∀ i, ∃ B : Matrix (d i) (d i) R, A i = B * star B := by
       intro i
       obtain ⟨B, hB⟩ : ∃ B : Matrix (d i) (d i) R, A i = B.conjTranspose * B := by
-        exact Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp (hA i)
+        classical
+        open MatrixOrder in
+        exact CStarAlgebra.nonneg_iff_eq_star_mul_self.mp (hA i).nonneg
       use B.conjTranspose;
       convert hB using 1;
       simp [ Matrix.star_eq_conjTranspose ];
diff --git a/QuantumInfo/ForMathlib/SionMinimax.lean b/QuantumInfo/ForMathlib/SionMinimax.lean
index 2811c4a..36f3ed8 100644
--- a/QuantumInfo/ForMathlib/SionMinimax.lean
+++ b/QuantumInfo/ForMathlib/SionMinimax.lean
@@ -8,7 +8,10 @@ import Mathlib.Analysis.Convex.Quasiconvex
 import Mathlib.Analysis.Convex.Topology
 import Mathlib.Analysis.Normed.Order.Lattice
 import Mathlib.Data.Fintype.Order
-import Mathlib.Topology.Semicontinuous
+import Mathlib.Algebra.Order.Module.Field
+import Mathlib.Data.EReal.Operations
+import Mathlib.Topology.Algebra.InfiniteSum.Order
+import Mathlib.Topology.MetricSpace.Bounded
 import Mathlib.Analysis.SpecificLimits.Basic
 
 @[simp]
@@ -422,8 +425,7 @@ private lemma sion_exists_min_2 (y₁ y₂ : N) (hy₁ : y₁ ∈ T) (hy₂ : y
   have hfxz (x) (hx : x ∈ S) (z) (hz : z ∈ segment ℝ y₁ y₂) : min (f x y₁) (f x y₂) ≤ f x z :=
     (hfq₁ x hx).min_le_mem_segment hy₁ hy₂ hz
   have hC'zAB (z) (hz : z ∈ segment ℝ y₁ y₂) : C' z ⊆ A ∪ B := by
-    --TODO: On newer Mathlib this is just `grind [inf_le_iff, le_trans]`
-    intro; simp [C', A, B]; grind [inf_le_iff, le_trans]
+    intro; grind [inf_le_iff, le_trans]
   have hC'z (z) (hz : z ∈ segment ℝ y₁ y₂) : Convex ℝ (C' z) :=
     hfq₂ z (hT₂.segment_subset hy₁ hy₂ hz) β
   have hC'zAB (z) (hz : z ∈ segment ℝ y₁ y₂) : C' z ⊆ A ∨ C' z ⊆ B := by
@@ -647,8 +649,7 @@ private lemma sion_exists_min_fin
       apply h_bddB.mono
       rintro _ ⟨x, hx, rfl⟩
       use x, hx
-      -- TODO: On a newer mathlib this line is just `grind`
-      rcases max_cases (f x ↑y₀') (f x yₙ) <;> grind
+      grind
     clear h_non_inter
     rw [lt_inf_iff]
     constructor
diff --git a/QuantumInfo/ForMathlib/Unitary.lean b/QuantumInfo/ForMathlib/Unitary.lean
index 2df8f47..b99cf44 100644
--- a/QuantumInfo/ForMathlib/Unitary.lean
+++ b/QuantumInfo/ForMathlib/Unitary.lean
@@ -22,12 +22,12 @@ open Module.End
 @[simp]
 theorem unitary_star_apply_eq (U : unitary (E →ₗ[𝕜] E)) (v : E) :
     (star U.val) (U.val v) = v := by
-  rw [← mul_apply, (unitary.mem_iff.mp U.prop).left, one_apply]
+  rw [← mul_apply, (Unitary.mem_iff.mp U.prop).left, one_apply]
 
 @[simp]
 theorem unitary_apply_star_eq (U : unitary (E →ₗ[𝕜] E)) (v : E) :
     U.val ((star U.val) v) = v := by
-  rw [← mul_apply, (unitary.mem_iff.mp U.prop).right, one_apply]
+  rw [← mul_apply, (Unitary.mem_iff.mp U.prop).right, one_apply]
 
 /-- Conjugating a linear map by a unitary operator gives a map whose μ-eigenspace is
   isomorphic (same dimension) as those of the original linear map. -/
@@ -70,7 +70,33 @@ variable {n : ℕ} (hn : Module.finrank 𝕜 E = n)
 and the eigenvalues of that operator conjugated by a unitary. -/
 def conj_unitary_eigenvalue_equiv (U : unitary (E →ₗ[𝕜] E)) (hT : T.IsSymmetric) :
     { σ : Equiv.Perm (Fin n) // (hT.conj_unitary_IsSymmetric U).eigenvalues hn = hT.eigenvalues hn ∘ σ } := by
-  sorry --use conj_unitary_eigenspace_equiv
+  set hS := hT.conj_unitary_IsSymmetric U
+  have heigen : ∀ μ, HasEigenvalue (U.val * T * star U.val) μ ↔ HasEigenvalue T μ := by
+    intro μ; rw [hasEigenvalue_iff, hasEigenvalue_iff, ne_eq, ne_eq, not_iff_not,
+      ← Submodule.finrank_eq_zero (R := 𝕜), ← Submodule.finrank_eq_zero (R := 𝕜),
+      (conj_unitary_eigenspace_equiv T U μ).finrank_eq]
+  suffices heq : hS.eigenvalues hn = hT.eigenvalues hn by exact ⟨1, by simp [heq]⟩
+  apply List.ofFn_injective
+  apply List.Perm.eq_of_sortedGE
+    (hS.eigenvalues_antitone hn).sortedGE_ofFn (hT.eigenvalues_antitone hn).sortedGE_ofFn
+  rw [← Multiset.coe_eq_coe, ← Fin.univ_val_map, ← Fin.univ_val_map]; ext a
+  simp only [Multiset.count_map]
+  suffices ∀ (R : E →ₗ[𝕜] E) (hR : R.IsSymmetric),
+      (Multiset.filter (fun x => a = hR.eigenvalues hn x) Finset.univ.val).card =
+      Finset.card {i | (hR.eigenvalues hn i : 𝕜) = ↑a} from by
+    rw [this _ hS, this _ hT]
+    by_cases ha : HasEigenvalue T (↑a : 𝕜)
+    · rw [hS.card_filter_eigenvalues_eq hn (heigen _|>.mpr ha),
+          hT.card_filter_eigenvalues_eq hn ha,
+          (conj_unitary_eigenspace_equiv T U ↑a).finrank_eq]
+    · have h1 : ∀ i, hT.eigenvalues hn i ≠ a :=
+        fun i h => ha (h ▸ hT.hasEigenvalue_eigenvalues hn i)
+      have h2 : ∀ i, hS.eigenvalues hn i ≠ a :=
+        fun i h => mt (heigen _).mp ha (h ▸ hS.hasEigenvalue_eigenvalues hn i)
+      simp [h1, h2]
+  intro R hR
+  change Finset.card (Finset.univ.filter (fun x => a = hR.eigenvalues hn x)) = _
+  congr 1; ext i; simp [eq_comm]
 
 end IsSymmetric
 end LinearMap