[Merged by Bors] - fix: more stable choice of representative for atoms in ring and abel

MathlibTest/abel.lean

@@ -143,21 +143,18 @@ example [AddCommGroup α] (x y z : α) (h : False) (w : x - x = y + z) : False :
   assumption
 
 abbrev myId (a : ℤ) : ℤ := a
+irreducible_def myIdOpaque : ℤ → ℤ := myId
 
 /-
 Test that when `abel_nf` normalizes multiple expressions which contain a particular atom, it uses a
 form for that atom which is consistent between expression.
-
-Note: This test is useless unless done at `=ₛ` (the level of syntactic equality); doing this test at
-`=` (the level of reducible equality) would not catch the erroneous old behaviour (normalizing one
-expression to `2 • myId x` and the other to `2 • x`).  But to get syntactic equality, we need to
-make the typeclass arguments agree, which requires some handholding in typeclass inference ... which
-is the reason for all the locally deleted instances here.
 -/
-attribute [-instance] Int.instAddGroup AddGroupWithOne.toAddGroup in
 example (x : ℤ) (R : ℤ → ℤ → Prop) (hR : Reflexive R) : True := by
   have : R (myId x + x) (x + myId x) := by
     abel_nf
-    guard_target =ₛ R ((2:ℤ) • myId x) ((2:ℤ) • myId x)
+    -- `guard_target` is using reducible defeq, so we need to make sure it cannot unfold any `myId`s
+    -- in the goal state.
+    rw [← myIdOpaque_def]
+    guard_target = R ((2:ℤ) • myIdOpaque x) ((2:ℤ) • myIdOpaque x)
     apply hR
   trivial

MathlibTest/ring.lean

@@ -85,25 +85,19 @@ example (x : ℝ) (hx : x ≠ 0) :
   ring
 
 abbrev myId (a : ℤ) : ℤ := a
+irreducible_def myIdOpaque : ℤ → ℤ := myId
 
 /-
 Test that when `ring_nf` normalizes multiple expressions which contain a particular atom, it uses a
 form for that atom which is consistent between expressions.
-
-Note: This test is useless unless done at `=ₛ` (the level of syntactic equality); doing this test at
-`=` (the level of reducible equality) would not catch the erroneous old behaviour (normalizing one
-expression to `myId x * 2` and the other to `x * 2`).  But to get syntactic equality, we need to
-make the typeclass arguments agree, which requires some handholding in typeclass inference ... which
-is the reason for all the locally deleted instances here.
 -/
-attribute [-instance] instOfNat instNatCastInt Int.instSemiring Int.instOrderedCommRing
-  Int.instOrderedRing Int.instLinearOrderedCommRing Int.instMul NonUnitalNonAssocRing.toMul
-  NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring
-  NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring in
 example (x : ℤ) (R : ℤ → ℤ → Prop) : True := by
   have : R (myId x + x) (x + myId x) := by
     ring_nf
-    guard_target =ₛ R (myId x * 2) (myId x * 2)
+    -- `guard_target` is using reducible defeq, so we need to make sure it cannot unfold any `myId`s
+    -- in the goal state.
+    rw [← myIdOpaque_def]
+    guard_target = R (myIdOpaque x * 2) (myIdOpaque x * 2)
     exact test_sorry
   trivial