chore: adaptations for leanprover/lean4#2923 (#9011)

This PR is targeting the `bump/v4.5.0` branch. It contains the adaptations required for leanprover/lean4#2923, which have now landed in the `2023-12-12` nightly toolchain.

The only changes are in `simp [...] says ...` statements, where some spurious lemmas are now no longer reported.

*Many* further `simp only` statements in Mathlib contain spurious lemmas which would now no longer be produced by a fresh `simp?`, and I would strongly encourage anyone interested in removing these! For now such changes will need to be made in a PR targeting `bump/v4.5.0` (like this PR), or in January they can be done on `master`.



Co-authored-by: Scott Morrison <[email protected]>

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -92,21 +92,21 @@ def normalize' (l : AList (fun _ : ℕ => Bool)) :
               · simp_all
         · have := ht₃ v
           have := he₃ v
-          simp_all? says simp_all only [Option.elim, ne_eq, normalized, Bool.and_eq_true,
+          simp_all? says simp_all only [Option.elim, normalized, Bool.and_eq_true,
               Bool.not_eq_true', AList.lookup_insert, imp_false]
           obtain ⟨⟨⟨tn, tc⟩, tr⟩, td⟩ := ht₂
           split <;> rename_i h'
           · subst h'
             simp_all
-          · simp_all? says simp_all only [ne_eq, hasNestedIf, Bool.or_self, hasConstantIf,
-              and_self, hasRedundantIf, Bool.or_false, beq_eq_false_iff_ne, not_false_eq_true,
+          · simp_all? says simp_all only [hasNestedIf, Bool.or_self, hasConstantIf, and_self,
+              hasRedundantIf, Bool.or_false, beq_eq_false_iff_ne, ne_eq, not_false_eq_true,
               disjoint, List.disjoint, decide_True, Bool.and_self]
         · have := ht₃ w
           have := he₃ w
           by_cases h : w = v
           · subst h; simp_all
-          · simp_all? says simp_all only [Option.elim, ne_eq, normalized, Bool.and_eq_true,
-              Bool.not_eq_true', not_false_eq_true, AList.lookup_insert_ne]
+          · simp_all? says simp_all only [Option.elim, normalized, Bool.and_eq_true,
+              Bool.not_eq_true', ne_eq, not_false_eq_true, AList.lookup_insert_ne]
             obtain ⟨⟨⟨en, ec⟩, er⟩, ed⟩ := he₂
             split at b <;> rename_i h'
             · subst h'; simp_all

Mathlib/CategoryTheory/Monoidal/Preadditive.lean

@@ -283,9 +283,8 @@ theorem leftDistributor_ext_left {J : Type} [Fintype J] {X Y : C} {f : J → C}
   apply (cancel_epi (leftDistributor X f).inv).mp
   ext
   simp? [leftDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc, dite_comp] says
-    simp only [leftDistributor_inv, Preadditive.comp_sum_assoc, ne_eq, biproduct.ι_π_assoc,
-      dite_comp, zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp,
-      ite_true]
+    simp only [leftDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc, dite_comp,
+      zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
   apply w
 
 @[ext]
@@ -295,7 +294,7 @@ theorem leftDistributor_ext_right {J : Type} [Fintype J] {X Y : C} {f : J → C}
   ext
   simp? [leftDistributor_hom, Preadditive.sum_comp, Preadditive.comp_sum_assoc, biproduct.ι_π,
     comp_dite] says
-    simp only [leftDistributor_hom, Category.assoc, Preadditive.sum_comp, ne_eq, biproduct.ι_π,
+    simp only [leftDistributor_hom, Category.assoc, Preadditive.sum_comp, biproduct.ι_π,
       comp_dite, comp_zero, Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id,
       ite_true]
   apply w
@@ -327,7 +326,7 @@ theorem rightDistributor_ext_left {J : Type} [Fintype J]
   apply (cancel_epi (rightDistributor f X).inv).mp
   ext
   simp? [rightDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc, dite_comp] says
-    simp only [rightDistributor_inv, Preadditive.comp_sum_assoc, ne_eq, biproduct.ι_π_assoc,
+    simp only [rightDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc,
       dite_comp, zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp,
       ite_true]
   apply w
@@ -340,7 +339,7 @@ theorem rightDistributor_ext_right {J : Type} [Fintype J]
   ext
   simp? [rightDistributor_hom, Preadditive.sum_comp, Preadditive.comp_sum_assoc, biproduct.ι_π,
     comp_dite] says
-    simp only [rightDistributor_hom, Category.assoc, Preadditive.sum_comp, ne_eq, biproduct.ι_π,
+    simp only [rightDistributor_hom, Category.assoc, Preadditive.sum_comp, biproduct.ι_π,
       comp_dite, comp_zero, Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id,
       ite_true]
   apply w

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.4.0-rc1
+leanprover/lean4:nightly-2023-12-12

test/abel.lean

@@ -98,15 +98,8 @@ error: abel_nf made no progress
 example [AddCommGroup α] (x y z : α) (_w : x = y + z) : False := by
   abel_nf at *
 
-/--
-error: no goals to be solved
--/
--- This error message is confusing: it is saying that it closed the main goal,
--- and so then had nothing to do on the hypotheses.
--- The user has to guess that they should remove the `at *`.
-#guard_msgs in
 example [AddCommGroup α] (x y z : α) (_w : x = y + z) : x - x = 0 := by
-  abel_nf at *
+  abel_nf
 
 /--
 error: abel_nf made no progress

test/matrix.lean

@@ -10,8 +10,6 @@ import Std.Tactic.GuardExpr
 
 open Qq
 
--- TODO: uncomment above imports when they are ported
-
 variable {α β : Type} [Semiring α] [Ring β]
 
 namespace Matrix
@@ -138,10 +136,10 @@ example {a b c d e f g h : α} : ![a, b, c, d, e, f, g, h] 99 = d := by simp
 example {α : Type _} [CommRing α] {a b c d : α} :
     Matrix.det !![a, b; c, d] = a * d - b * c := by
   simp? [Matrix.det_succ_row_zero, Fin.sum_univ_succ] says
-    simp only [det_succ_row_zero, Nat.odd_iff_not_even, of_apply, cons_val', empty_val',
+    simp only [det_succ_row_zero, of_apply, cons_val', empty_val',
       cons_val_fin_one, cons_val_zero, det_unique, Fin.default_eq_zero, submatrix_apply,
-      Fin.succ_zero_eq_one, ne_eq, cons_val_one, head_fin_const, Fin.sum_univ_succ, Fin.val_zero,
-      pow_zero, one_mul, not_true_eq_false, Fin.zero_succAbove, head_cons, Finset.univ_unique,
+      Fin.succ_zero_eq_one, cons_val_one, head_fin_const, Fin.sum_univ_succ, Fin.val_zero,
+      pow_zero, one_mul, Fin.zero_succAbove, head_cons, Finset.univ_unique,
       Fin.val_succ, Fin.coe_fin_one, zero_add, pow_one, cons_val_succ, neg_mul,
       Fin.succ_succAbove_zero, Finset.sum_const, Finset.card_singleton, smul_neg, one_smul]
   ring
@@ -150,12 +148,12 @@ example {α : Type _} [CommRing α] {a b c d e f g h i : α} :
     Matrix.det !![a, b, c; d, e, f; g, h, i] =
       a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g := by
   simp? [Matrix.det_succ_row_zero, Fin.sum_univ_succ] says
-    simp only [det_succ_row_zero, Nat.odd_iff_not_even, of_apply, cons_val', empty_val',
-      cons_val_fin_one, cons_val_zero, submatrix_apply, Fin.succ_zero_eq_one, cons_val_one, head_cons,
-      submatrix_submatrix, det_unique, Fin.default_eq_zero, Function.comp_apply, Fin.succ_one_eq_two,
-      ne_eq, cons_val_two, tail_cons, head_fin_const, Fin.sum_univ_succ, Fin.val_zero, pow_zero,
-      one_mul, not_true_eq_false, Fin.zero_succAbove, Finset.univ_unique, Fin.val_succ,
-      Fin.coe_fin_one, zero_add, pow_one, neg_mul, Fin.succ_succAbove_zero, Finset.sum_neg_distrib,
+    simp only [det_succ_row_zero, of_apply, cons_val', empty_val',
+      cons_val_fin_one, cons_val_zero, submatrix_apply, Fin.succ_zero_eq_one, cons_val_one,
+      head_cons, submatrix_submatrix, det_unique, Fin.default_eq_zero, Function.comp_apply,
+      Fin.succ_one_eq_two, cons_val_two, tail_cons, head_fin_const, Fin.sum_univ_succ, Fin.val_zero,
+      pow_zero, one_mul, Fin.zero_succAbove, Finset.univ_unique, Fin.val_succ, Fin.coe_fin_one,
+      zero_add, pow_one, neg_mul, Fin.succ_succAbove_zero, Finset.sum_neg_distrib,
       Finset.sum_singleton, cons_val_succ, Fin.succ_succAbove_one, even_add_self, Even.neg_pow,
       one_pow, Finset.sum_const, Finset.card_singleton, one_smul]
   ring