diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index 840610417b..e46a07904d 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -716,7 +716,7 @@ where pure dontCare else let arg ← expandOffsetPatterns arg - unless isEqBwdParent do + unless isEqBwdParent || inSupport do /- **Note**: We ignore symbols in ground patterns if the parent is the auxiliary ``Grind.eqBwdPattern We do that because we want to sign an error in examples such as: diff --git a/tests/lean/run/grind_ground_pat_issue.lean b/tests/lean/run/grind_ground_pat_issue.lean new file mode 100644 index 0000000000..6d8ca1a9db --- /dev/null +++ b/tests/lean/run/grind_ground_pat_issue.lean @@ -0,0 +1,43 @@ +/-! + Test for a regression introduced by #11589 +-/ + +section Mathlib.Order.Defs.LinearOrder + +class LinearOrder (α : Type) extends Max α where + +end Mathlib.Order.Defs.LinearOrder +section Mathlib.Data.Int.Order.Basic + +instance instLinearOrder : LinearOrder Int where + +end Mathlib.Data.Int.Order.Basic +section Mathlib.Order.Lattice + +variable {α : Type} + +class SemilatticeSup (α : Type) where + sup : α → α → α + +instance SemilatticeSup.toMax [SemilatticeSup α] : Max α where max a b := SemilatticeSup.sup a b + +instance LinearOrder.toSemilatticeSup {α : Type} [LinearOrder α] : SemilatticeSup α where + sup := max + +end Mathlib.Order.Lattice + +section Mathlib.Algebra.Order.Group.Unbundled.Abs + +variable {α : Type} [SemilatticeSup α] [Neg α] {a b : α} + +@[grind] +def abs (a : α) : α := max a (-a) + +end Mathlib.Algebra.Order.Group.Unbundled.Abs + +@[grind =] theorem max_def [Max α] [LE α] [DecidableLE α] (a b : α) + : max a b = if a ≤ b then b else a := + sorry + +theorem abs_lt_one_iff {a : Int} : abs a < 1 ↔ a = 0 := by + grind