Bump toolchain to 4.28

ClassicalInfo/Distribution.lean

@@ -143,8 +143,7 @@ def extend_left (d : Distribution α) : Distribution (β ⊕ α) :=
 /-- Make a convex mixture of two distributions on the same set. -/
 instance instMixable : Mixable (α → ℝ) (Distribution α) :=
   Mixable.instSubtype (inferInstance) (fun _ _ hab hx hy ↦ by
-    admit -- admitting out because Aristotle fails to load it otherwise
-    -- simp [Mixable.mix_ab, Finset.sum_add_distrib, ← Finset.mul_sum, hab, hx, hy]
+    simp [Mixable.mix_ab, Finset.sum_add_distrib, ← Finset.mul_sum, hab, hx, hy]
   )
 
 /-- Given a distribution on type α and an equivalence to type β, get the corresponding
@@ -198,7 +197,7 @@ theorem fin_two_eq_coin (d : Distribution (Fin 2)) : d = coin (d 0) := by
   fin_cases i
   · simp [coin]
   · simpa only [coin, Fin.mk_one, funlike_apply, one_ne_zero, ↓reduceIte,
-    Prob.coe_one_minus, Subtype.eq_iff, Prob.coe_one_minus, eq_sub_iff_add_eq, add_comm,
+    Prob.coe_one_minus, Subtype.ext_iff, Prob.coe_one_minus, eq_sub_iff_add_eq, add_comm,
         fun_eq_val, Fin.sum_univ_two] using d.property
 
 theorem coin_eq_iff (p : Prob) (f : Distribution (Fin 2)) :
@@ -252,7 +251,7 @@ theorem expect_val_eq_mixable_mix (d : Distribution (Fin 2)) (x₁ x₂ : T) : e
       simp
     _ = (d 0 : ℝ) • Mixable.to_U x₁ + (1 - d 0).val • Mixable.to_U x₂ := by
       congr
-      simpa only [Subtype.eq_iff, Prob.coe_one_minus, eq_sub_iff_add_eq, add_comm,
+      simpa only [Subtype.ext_iff, Prob.coe_one_minus, eq_sub_iff_add_eq, add_comm,
         fun_eq_val, Fin.sum_univ_two] using d.property
 
 /-- The expectation value of a random variable with constant probability distribution `constant x` is its value at `x` -/

ClassicalInfo/Prob.lean

@@ -85,11 +85,11 @@ instance instInhabited : Inhabited Prob where
   default := 0
 
 instance : LinearOrderedCommMonoidWithZero Prob where
-  mul_le_mul_left := by
-    intros a b h c
-    rw [← Subtype.coe_le_coe]
-    exact mul_le_mul_of_nonneg_left h c.2.1
-  zero_le_one := (0 : Prob).2.2
+  mul_lt_mul_of_pos_left := by
+    intros a ha b h hb
+    rw [← Subtype.coe_lt_coe]
+    exact mul_lt_mul_of_pos_left hb ha
+  zero_le a := a.2.1
 
 @[simp]
 theorem zero_le_coe {p : Prob} : 0 ≤ (p : ℝ) :=
@@ -107,11 +107,11 @@ theorem zero_le {p : Prob} : 0 ≤ p :=
 theorem le_one {p : Prob} : p ≤ 1 :=
   coe_le_one
 
-@[ext] protected theorem eq {n m : Prob} : (n : ℝ) = (m : ℝ) → n = m :=
-  Subtype.eq
+@[ext] protected theorem ext {n m : Prob} : (n : ℝ) = (m : ℝ) → n = m :=
+  Subtype.ext
 
 theorem ne_iff {x y : Prob} : (x : ℝ) ≠ (y : ℝ) ↔ x ≠ y :=
-  not_congr <| Prob.eq_iff.symm
+  not_congr <| Prob.ext_iff.symm
 
 @[simp, norm_cast]
 theorem toReal_mul (x y : Prob) : (x * y : Prob) = (x : ℝ) * (y : ℝ) := by
@@ -209,7 +209,7 @@ theorem mul_eq_one_iff (p q : Prob) : p * q = 1 ↔ p = 1 ∧ q = 1 := by
   cases p
   cases q
   refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-  simp [Prob.eq_iff] at h ⊢
+  simp [Prob.ext_iff] at h ⊢
   constructor <;> nlinarith
 
 end Prob
@@ -351,7 +351,7 @@ namespace Prob
 /-- Probabilities `Prob` themselves are convex. -/
 instance instMixable : Mixable ℝ Prob where
   to_U := Subtype.val
-  to_U_inj := Prob.eq
+  to_U_inj := Prob.ext
   mkT := fun h ↦ ⟨⟨_, Exists.casesOn h fun t ht => ht ▸ t.prop⟩, rfl⟩
   convex := by
     simp [Convex, StarConvex]
@@ -440,7 +440,7 @@ theorem le_negLog_of_le_exp {p : Prob} {x : ℝ} (h : p ≤ Real.exp (-x)) : ENN
         rw [← ENNReal.toReal_lt_toReal ofReal_ne_top coe_ne_top, toReal_ofReal hx]
         simpa using lt_neg_of_lt_neg h
       · apply le_of_eq
-        rw [← ENNReal.toReal_eq_toReal ofReal_ne_top coe_ne_top,
+        rw [← ENNReal.toReal_eq_toReal_iff' ofReal_ne_top coe_ne_top,
           coe_toReal, coe_mk, h, Real.log_exp, neg_neg, toReal_ofReal hx]
   · trans 0
     · simp only [nonpos_iff_eq_zero, ofReal_eq_zero, le_of_not_ge hx]

QuantumInfo/ForMathlib/ContinuousLinearMap.lean

@@ -18,16 +18,17 @@ variable [TopologicalSpace M] [AddCommMonoid M] [TopologicalSpace M₂] [AddComm
 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 σ] : LinearMap.range (0 : M →SL[σ] M₂) = ⊥ :=
-  LinearMap.range_zero
+theorem range_zero [RingHomSurjective σ] : (0 : M →SL[σ] M₂).range = ⊥ := by
+  simp
 
 @[simp]
-theorem ker_zero : LinearMap.ker (0 : M →SL[σ] M₂) = ⊤ :=
-  LinearMap.ker_zero
+theorem ker_zero : (0 : M →SL[σ] M₂).ker = ⊤ := by
+  simp
 
 theorem ker_mk (f : M →ₛₗ[σ] M₂) (hf : Continuous f.toFun) :
-    LinearMap.ker (ContinuousLinearMap.mk f hf) = LinearMap.ker f := by
+    (ContinuousLinearMap.mk f hf).ker = LinearMap.ker f := by
   rfl
 
 end ContinuousLinearMap
@@ -38,7 +39,7 @@ variable {n 𝕜 : Type*} [Fintype n] [RCLike 𝕜]
 
 /-- The support of a Hermitian matrix is the sum of its nonzero eigenspaces. -/
 theorem support_eq_sup_eigenspace_nonzero (A : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n)
-    (hA : A.IsSymmetric) : LinearMap.range A = ⨆ μ ≠ 0, Module.End.eigenspace A μ := by
+    (hA : A.IsSymmetric) : A.range = ⨆ μ ≠ 0, Module.End.eigenspace A μ := by
   apply le_antisymm
   · rintro x ⟨y, hy⟩
     have h_decomp : y ∈ ⨆ (μ : 𝕜), Module.End.eigenspace A.toLinearMap μ := by
@@ -53,7 +54,7 @@ theorem support_eq_sup_eigenspace_nonzero (A : EuclideanSpace 𝕜 n →L[𝕜]
       exact rfl
     have h_eigen (i) : A (f i) = (i : 𝕜) • f i :=
       Module.End.mem_eigenspace_iff.mp (hf₁ i)
-    rw [← hy, h_apply_A, Finset.sum_congr rfl (fun i _ ↦ h_eigen i)]
+    rw [← hy, coe_coe, h_apply_A, Finset.sum_congr rfl (fun i _ ↦ h_eigen i)]
     refine Submodule.sum_mem _ fun i _ ↦ ?_
     by_cases hi0 : i = 0
     · simp [hi0]

QuantumInfo/ForMathlib/Filter.lean

@@ -31,7 +31,7 @@ theorem Filter.Tendsto_inv_nat_mul_div_real (m : ℕ)
           simpa [ div_eq_inv_mul ] using Nat.floor_le ( by positivity : 0 ≤ ( x : ℝ ) / m );
     -- Apply the squeeze theorem to conclude the proof.
     have h_squeeze : Filter.Tendsto (fun x : ℕ => (1 / m : ℝ) - 1 / x) Filter.atTop (nhds (1 / m)) := by
-      simpa using tendsto_const_nhds.sub ( _root_.tendsto_inverse_atTop_nhds_zero_nat );
+      simpa using tendsto_const_nhds.sub (tendsto_inv_atTop_nhds_zero_nat (𝕜 := ℝ))
     exact tendsto_of_tendsto_of_tendsto_of_le_of_le' h_squeeze tendsto_const_nhds ( Filter.eventually_atTop.mpr ⟨ 1, fun x hx => h_floor_bound x hx |>.1 ⟩ ) ( Filter.eventually_atTop.mpr ⟨ 1, fun x hx => h_floor_bound x hx |>.2 ⟩ );
   -- Apply the hypothesis `h_floor` to conclude the proof.
   convert h_floor using 1;

QuantumInfo/ForMathlib/LimSupInf.lean

@@ -1,9 +1,15 @@
 import Mathlib.Algebra.Order.Ring.Star
 import Mathlib.Analysis.Normed.Ring.Lemmas
+import Mathlib.Data.Finset.Attr
 import Mathlib.Data.Int.Star
 import Mathlib.Data.Real.StarOrdered
+import Mathlib.Tactic.Bound
 import Mathlib.Tactic.Peel
-import Mathlib.Topology.Compactness.PseudometrizableLindelof
+import Mathlib.Tactic.Common
+import Mathlib.Tactic.Continuity
+import Mathlib.Tactic.Finiteness.Attr
+import Mathlib.Tactic.SetLike
+import Mathlib.Util.CompileInductive
 import Mathlib.Topology.Instances.ENNReal.Lemmas
 import Mathlib.Topology.Instances.Nat
 
@@ -142,7 +148,9 @@ lemma exists_liminf_zero_of_forall_liminf_le (y : ℝ≥0) (f : ℝ≥0 → ℕ
         refine' lt_of_le_of_lt _ right;
         convert add_le_add_left ( ENNReal.ofReal_le_ofReal hk.le ) ( y : ℝ≥0∞ ) using 1 ; norm_num [ ENNReal.ofReal ];
         · norm_num [ Real.toNNReal_inv ];
-        · rw [ ENNReal.ofReal_sub ] <;> norm_num [ left.le ];
+          rw [add_comm]
+        · rw [ENNReal.ofReal_sub _ (by positivity)]
+          simp [tsub_add_cancel_of_le, left.le]
       refine' ⟨ n ( Max.max x k ), _, _ ⟩
       · simp_all only [ne_eq, add_eq_zero, Nat.cast_eq_zero, one_ne_zero, and_false, not_false_eq_true, ENNReal.coe_inv,
           ENNReal.coe_add, ENNReal.coe_natCast, ENNReal.coe_one]
@@ -220,7 +228,7 @@ lemma exists_limsup_zero_of_forall_limsup_le (y : ℝ≥0) (f : ℝ≥0 → ℕ
       have := hM.2 ( Nat.findGreatest ( fun k => M k ≤ n ) n ) n ?_
       · simp_all only [gt_iff_lt, ge_iff_le, one_div]
         obtain ⟨left, right⟩ := hM
-        exact le_trans this ( add_le_add_left ( le_trans ( by gcongr ) hK.le ) _ );
+        refine le_trans this ( add_le_add_right ( le_trans ( by gcongr ) hK.le ) _ );
       · simp_all only [gt_iff_lt, ge_iff_le]
         obtain ⟨left, right⟩ := hM
         have := Nat.findGreatest_eq_iff.mp ( by aesop : Nat.findGreatest ( fun k => M k ≤ n ) n = Nat.findGreatest ( fun k => M k ≤ n ) n )
@@ -353,7 +361,7 @@ lemma limsup_le_of_block_sequence_bound {α : Type*} (y : ℝ≥0) (f : α → 
         exact Set.finite_iff_bddAbove.2 ⟨ b, fun n hn => le_trans ( hT.id_le _ ) hn ⟩;
       exact ⟨ Finset.max' ( h_finite.toFinset ) ⟨ K, h_finite.mem_toFinset.mpr a ⟩, h_finite.mem_toFinset.mp ( Finset.max'_mem _ _ ), not_le.mp fun h => not_lt_of_ge ( Finset.le_max' _ _ ( h_finite.mem_toFinset.mpr h ) ) ( Nat.lt_succ_self _ ) ⟩;
     rw [ hg k b hk.1 hk.2 ];
-    exact le_trans ( hbound k b hk.1 hk.2 ) ( add_le_add_left ( hK k ( le_of_not_gt fun hk' => by linarith [ hT.monotone hk'.nat_succ_le ] ) ) _ )
+    exact le_trans ( hbound k b hk.1 hk.2 ) ( add_le_add_right ( hK k ( le_of_not_gt fun hk' => by linarith [ hT.monotone hk'.nat_succ_le ] ) ) _ )
 
 /- Version of `exists_liminf_zero_of_forall_liminf_le_with_UB` that lets you stipulate it for
 two different functions simultaneously, one with liminf and one with limsup. -/

QuantumInfo/ForMathlib/LinearEquiv.lean

@@ -17,10 +17,12 @@ def of_relabel (e : d ≃ d₂) : (d₂ → R) ≃ₗ[R] (d → R) := by
   refine' { e.symm.piCongrLeft (fun _ ↦ R) with .. }
   <;> (intros; ext; simp [Equiv.piCongrLeft_apply])
 
+variable (e : d ≃ d₂)
+
 variable (𝕜) in
 @[simps!]
 def euclidean_of_relabel (e : d ≃ d₂) : EuclideanSpace 𝕜 d₂ ≃ₗ[𝕜] EuclideanSpace 𝕜 d :=
-  of_relabel 𝕜 e
+  (WithLp.linearEquiv 2 𝕜 _).trans ((of_relabel _ e).trans (WithLp.linearEquiv 2 𝕜 _).symm)
 
 @[simp]
 theorem of_relabel_refl : of_relabel R (.refl d) = LinearEquiv.refl R (d → R) := by
@@ -47,8 +49,9 @@ theorem reindex_toLin' (e : d₁ ≃ d₃) (f : d₂ ≃ d) (M : Matrix d₁ d
 
 theorem reindex_toEuclideanLin (e : d₁ ≃ d₃) (f : d₂ ≃ d) (M : Matrix d₁ d₂ 𝕜) :
     (M.reindex e f).toEuclideanLin = (LinearEquiv.euclidean_of_relabel 𝕜 e.symm) ∘ₗ
-      M.toEuclideanLin ∘ₗ (LinearEquiv.euclidean_of_relabel 𝕜 f) :=
-  reindex_toLin' e f M
+      M.toEuclideanLin ∘ₗ (LinearEquiv.euclidean_of_relabel 𝕜 f) := by
+  ext
+  simp [mulVec, dotProduct, Equiv.piCongrLeft_apply]
 
 theorem reindex_right_toLin' (e : d ≃ d₂) (M : Matrix d₃ d R) :
     (M.reindex (.refl d₃) e).toLin' = M.toLin' ∘ₗ (LinearEquiv.of_relabel R e) := by
@@ -57,8 +60,9 @@ theorem reindex_right_toLin' (e : d ≃ d₂) (M : Matrix d₃ d R) :
 
 theorem reindex_right_toEuclideanLin (e : d ≃ d₂) (M : Matrix d₃ d 𝕜) :
     (M.reindex (.refl d₃) e).toEuclideanLin =
-      M.toEuclideanLin ∘ₗ (LinearEquiv.euclidean_of_relabel 𝕜 e) :=
-  reindex_right_toLin' e M
+      M.toEuclideanLin ∘ₗ (LinearEquiv.euclidean_of_relabel 𝕜 e) := by
+  ext
+  simp [mulVec, dotProduct, Equiv.piCongrLeft_apply]
 
 theorem reindex_left_toLin' (e : d₁ ≃ d₃) (M : Matrix d₁ d₂ R) :
     (M.reindex e (.refl d₂)).toLin' = (LinearEquiv.of_relabel R e.symm) ∘ M.toLin' := by