From 44cfa325a9b4f97f083d9ca284fb866407f8b941 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 31 Jan 2024 15:46:26 -0800
Subject: [PATCH] fix: Mathlib regressions reported by Scott

---
 src/Lean/Meta/Tactic/Simp/Rewrite.lean |  2 +-
 tests/lean/run/regressions3210.lean    | 38 ++++++++++++++++++++++++++
 2 files changed, 39 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/regressions3210.lean

diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 75695d06e73a..8a59cd3cc149 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -163,7 +163,7 @@ private def reduceOfNatNat (e : Expr) : MetaM Expr := do
     return e
   return e.getArg! 1
 
-def simpCtorEq : Simproc := fun e => do
+def simpCtorEq : Simproc := fun e => withReducibleAndInstances do
   match e.eq? with
   | none => return .continue
   | some (_, lhs, rhs) =>
diff --git a/tests/lean/run/regressions3210.lean b/tests/lean/run/regressions3210.lean
new file mode 100644
index 000000000000..4ed0930f3bff
--- /dev/null
+++ b/tests/lean/run/regressions3210.lean
@@ -0,0 +1,38 @@
+-- Regressions for #3210
+
+example : ¬1 % 2 = 0 := by
+  simp
+
+universe u
+
+class One (α : Type u) where
+  one : α
+
+instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
+  ofNat := ‹One α›.1
+instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
+  one := 1
+
+example : Not
+  (@Eq.{1} Nat
+    (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instModNat)
+      (@OfNat.ofNat.{0} Nat (nat_lit 1) (@One.toOfNat1.{0} Nat (@One.ofOfNat1.{0} Nat (instOfNatNat (nat_lit 1)))))
+      (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
+    (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) := by
+  simp
+
+example : Not
+  (@Eq.{1} Nat
+    (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instModNat)
+      (@OfNat.ofNat.{0} Nat 1 (@One.toOfNat1.{0} Nat (@One.ofOfNat1.{0} Nat (instOfNatNat 1))))
+      (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
+    (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) := by
+  simp
+
+def WithTop (α : Type) := Option α
+
+class Top (α : Type) where top : α
+
+instance top : Top (WithTop α) := ⟨none⟩
+
+example {α : Type} (x : α) : ¬ some x = (Top.top : WithTop α) := by simp