Resolve TODOs: drop CLM aliases, upgrade Jordan to CommRing, simplify grind calls, grind in Basic, simplify PosDef.zero_lt proof

Author: dennj

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

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
 

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
 

QuantumInfo/ForMathlib/Matrix.lean

@@ -1141,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) :

QuantumInfo/ForMathlib/SionMinimax.lean

@@ -425,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
@@ -650,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