lint

Author: kim-em

Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean

@@ -60,10 +60,18 @@ variable {J : Type w}
 inductive WalkingParallelFamily (J : Type w) : Type w
   | zero : WalkingParallelFamily J
   | one : WalkingParallelFamily J
-deriving DecidableEq, Inhabited
+deriving Inhabited
 
 open WalkingParallelFamily
 
+-- We do not use `deriving DecidableEq` here
+-- because it generates an instance with unnecessary hypotheses.
+instance : DecidableEq (WalkingParallelFamily J)
+  | zero, zero => isTrue rfl
+  | zero, one => isFalse fun t => by grind
+  | one, zero => isFalse fun t => by grind
+  | one, one => isTrue rfl
+
 -- Don't generate unnecessary `sizeOf_spec` lemma which the `simpNF` linter will complain about.
 set_option genSizeOfSpec false in
 /-- The type family of morphisms for the diagram indexing a wide (co)equalizer. -/

MathlibTest/grind/lint.lean

@@ -1,5 +1,13 @@
 import Mathlib
 
+#adaptation_note
+/--
+FIXME: please investigate these lemmas, and add guard conditions as needed.
+(These appeared at nightly-2025-12-13.)
+--/
+#grind_lint skip Path.symm_apply
+#grind_lint skip Set.Icc.convexCombo_symm
+
 -- This check verifies that `grind` annotations in Mathlib do not trigger run-away instantiations.
 -- If this test fails, please modify newly introduced `grind` annotations to use the
 -- `grind_pattern ... where ...` syntax to add side conditions that will prevent the run-away.