From 3a1823ac342af678212bad3502da4c44b306f48d Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed, 13 Nov 2024 11:13:09 -0500
Subject: [PATCH 01/15] test ci

---
 Mathlib/Tactic/Abel.lean                   |  6 +++---
 Mathlib/Tactic/ITauto.lean                 |  2 +-
 Mathlib/Tactic/Linarith/Preprocessing.lean |  6 +++---
 Mathlib/Tactic/Module.lean                 |  7 ++++---
 Mathlib/Tactic/Ring/Basic.lean             | 17 ++++++++++-------
 Mathlib/Tactic/TFAE.lean                   | 10 +++++-----
 Mathlib/Util/AtomM.lean                    |  6 +++---
 MathlibTest/abel.lean                      | 10 ++++++++++
 MathlibTest/ring.lean                      | 10 ++++++++++
 9 files changed, 49 insertions(+), 25 deletions(-)

diff --git a/Mathlib/Tactic/Abel.lean b/Mathlib/Tactic/Abel.lean
index dafcc98e2ffe0..4002862603dbc 100644
--- a/Mathlib/Tactic/Abel.lean
+++ b/Mathlib/Tactic/Abel.lean
@@ -247,11 +247,11 @@ theorem term_atom_pfg {α} [AddCommGroup α] (x x' : α) (h : x = x') : x = term
 /-- Interpret an expression as an atom for `abel`'s normal form. -/
 def evalAtom (e : Expr) : M (NormalExpr × Expr) := do
   let { expr := e', proof?, .. } ← (← readThe AtomM.Context).evalAtom e
-  let i ← AtomM.addAtom e'
+  let (i, a) ← AtomM.addAtom e'
   let p ← match proof? with
   | none => iapp ``term_atom #[e]
-  | some p => iapp ``term_atom_pf #[e, e', p]
-  return (← term' (← intToExpr 1, 1) (i, e') (← zero'), p)
+  | some p => iapp ``term_atom_pf #[e, a, p]
+  return (← term' (← intToExpr 1, 1) (i, a) (← zero'), p)
 
 theorem unfold_sub {α} [SubtractionMonoid α] (a b c : α) (h : a + -b = c) : a - b = c := by
   rw [sub_eq_add_neg, h]
diff --git a/Mathlib/Tactic/ITauto.lean b/Mathlib/Tactic/ITauto.lean
index f0449d9828b14..f87cbcddd6ec3 100644
--- a/Mathlib/Tactic/ITauto.lean
+++ b/Mathlib/Tactic/ITauto.lean
@@ -486,7 +486,7 @@ partial def reify (e : Q(Prop)) : AtomM IProp :=
   | ~q(@Ne Prop $a $b) => return .not (.eq (← reify a) (← reify b))
   | e =>
     if e.isArrow then return .imp (← reify e.bindingDomain!) (← reify e.bindingBody!)
-    else return .var (← AtomM.addAtom e)
+    else return .var (← AtomM.addAtom e).1
 
 /-- Once we have a proof object, we have to apply it to the goal. -/
 partial def applyProof (g : MVarId) (Γ : NameMap Expr) (p : Proof) : MetaM Unit :=
diff --git a/Mathlib/Tactic/Linarith/Preprocessing.lean b/Mathlib/Tactic/Linarith/Preprocessing.lean
index 418da06138f72..a7294e77c4538 100644
--- a/Mathlib/Tactic/Linarith/Preprocessing.lean
+++ b/Mathlib/Tactic/Linarith/Preprocessing.lean
@@ -273,12 +273,12 @@ partial def findSquares (s : RBSet (Nat × Bool) lexOrd.compare) (e : Expr) :
   | (``HPow.hPow, #[_, _, _, _, a, b]) => match b.numeral? with
     | some 2 => do
       let s ← findSquares s a
-      let ai ← AtomM.addAtom a
+      let (ai, _) ← AtomM.addAtom a
       return (s.insert (ai, true))
     | _ => e.foldlM findSquares s
   | (``HMul.hMul, #[_, _, _, _, a, b]) => do
-    let ai ← AtomM.addAtom a
-    let bi ← AtomM.addAtom b
+    let (ai, _) ← AtomM.addAtom a
+    let (bi, _) ← AtomM.addAtom b
     if ai = bi then do
       let s ← findSquares s a
       return (s.insert (ai, false))
diff --git a/Mathlib/Tactic/Module.lean b/Mathlib/Tactic/Module.lean
index 4df4c398c9ef4..015c5296d96da 100644
--- a/Mathlib/Tactic/Module.lean
+++ b/Mathlib/Tactic/Module.lean
@@ -464,9 +464,10 @@ partial def parse (iM : Q(AddCommMonoid $M)) (x : Q($M)) :
     pure ⟨0, q(Nat), q(Nat.instSemiring), q(AddCommGroup.toNatModule), [], q(NF.zero_eq_eval $M)⟩
   /- anything else should be treated as an atom -/
   | _ =>
-    let k : ℕ ← AtomM.addAtom x
-    pure ⟨0, q(Nat), q(Nat.instSemiring), q(AddCommGroup.toNatModule), [((q(1), x), k)],
-      q(NF.atom_eq_eval $x)⟩
+    let (k, x') ← AtomM.addAtom x
+    have x' : Q($M) := x'
+    pure ⟨0, q(Nat), q(Nat.instSemiring), q(AddCommGroup.toNatModule), [((q(1), x'), k)],
+      (q(NF.atom_eq_eval $x'):)⟩
 
 /-- Given expressions `R` and `M` representing types such that `M`'s is a module over `R`'s, and
 given two terms `l₁`, `l₂` of type `qNF R M`, i.e. lists of `(Q($R) × Q($M)) × ℕ`s (two `Expr`s
diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean
index 84faee3f1a0d4..be4dd945a0c12 100644
--- a/Mathlib/Tactic/Ring/Basic.lean
+++ b/Mathlib/Tactic/Ring/Basic.lean
@@ -513,8 +513,9 @@ partial def ExBase.evalNatCast {a : Q(ℕ)} (va : ExBase sℕ a) : AtomM (Result
   match va with
   | .atom _ => do
     let a' : Q($α) := q($a)
-    let i ← addAtom a'
-    pure ⟨a', ExBase.atom i, (q(Eq.refl $a') : Expr)⟩
+    let (i, b) ← addAtom a'
+    let b' : Q($α) := b
+    pure ⟨b', ExBase.atom i, (q(Eq.refl $b') : Expr)⟩
   | .sum va => do
     let ⟨_, vc, p⟩ ← va.evalNatCast
     pure ⟨_, .sum vc, p⟩
@@ -952,11 +953,12 @@ Evaluates an atom, an expression where `ring` can find no additional structure.
 def evalAtom (e : Q($α)) : AtomM (Result (ExSum sα) e) := do
   let r ← (← read).evalAtom e
   have e' : Q($α) := r.expr
-  let i ← addAtom e'
-  let ve' := (ExBase.atom i (e := e')).toProd (ExProd.mkNat sℕ 1).2 |>.toSum
+  let (i, a) ← addAtom e'
+  have a' : Q($α) := a
+  let ve' := (ExBase.atom i (e := a')).toProd (ExProd.mkNat sℕ 1).2 |>.toSum
   pure ⟨_, ve', match r.proof? with
   | none => (q(atom_pf $e) : Expr)
-  | some (p : Q($e = $e')) => (q(atom_pf' $p) : Expr)⟩
+  | some (p : Q($e = $a')) => (q(atom_pf' $p) : Expr)⟩
 
 theorem inv_mul {R} [DivisionRing R] {a₁ a₂ a₃ b₁ b₃ c}
     (_ : (a₁⁻¹ : R) = b₁) (_ : (a₃⁻¹ : R) = b₃)
@@ -978,8 +980,9 @@ variable (dα : Q(DivisionRing $α))
 /-- Applies `⁻¹` to a polynomial to get an atom. -/
 def evalInvAtom (a : Q($α)) : AtomM (Result (ExBase sα) q($a⁻¹)) := do
   let a' : Q($α) := q($a⁻¹)
-  let i ← addAtom a'
-  pure ⟨a', ExBase.atom i, (q(Eq.refl $a') : Expr)⟩
+  let (i, b) ← addAtom a'
+  let b' : Q($α) := b
+  pure ⟨b', ExBase.atom i, (q(Eq.refl $b') : Expr)⟩
 
 /-- Inverts a polynomial `va` to get a normalized result polynomial.
 
diff --git a/Mathlib/Tactic/TFAE.lean b/Mathlib/Tactic/TFAE.lean
index 45405bfe5ad58..ac5f1114a8529 100644
--- a/Mathlib/Tactic/TFAE.lean
+++ b/Mathlib/Tactic/TFAE.lean
@@ -298,18 +298,18 @@ elab_rules : tactic
   goal.withContext do
     let (tfaeListQ, tfaeList) ← getTFAEList (← goal.getType)
     closeMainGoal `tfae_finish <|← AtomM.run .reducible do
-      let is ← tfaeList.mapM AtomM.addAtom
+      let is ← tfaeList.mapM (fun e ↦ Prod.fst <$> AtomM.addAtom e)
       let mut hyps := #[]
       for hyp in ← getLocalHyps do
         let ty ← whnfR <|← instantiateMVars <|← inferType hyp
         if let (``Iff, #[p1, p2]) := ty.getAppFnArgs then
-          let q1 ← AtomM.addAtom p1
-          let q2 ← AtomM.addAtom p2
+          let (q1, _) ← AtomM.addAtom p1
+          let (q2, _) ← AtomM.addAtom p2
           hyps := hyps.push (q1, q2, ← mkAppM ``Iff.mp #[hyp])
           hyps := hyps.push (q2, q1, ← mkAppM ``Iff.mpr #[hyp])
         else if ty.isArrow then
-          let q1 ← AtomM.addAtom ty.bindingDomain!
-          let q2 ← AtomM.addAtom ty.bindingBody!
+          let (q1, _) ← AtomM.addAtom ty.bindingDomain!
+          let (q2, _) ← AtomM.addAtom ty.bindingBody!
           hyps := hyps.push (q1, q2, hyp)
       proveTFAE hyps (← get).atoms is tfaeListQ
 
diff --git a/Mathlib/Util/AtomM.lean b/Mathlib/Util/AtomM.lean
index 0b829028c0b11..59a2ec70a7540 100644
--- a/Mathlib/Util/AtomM.lean
+++ b/Mathlib/Util/AtomM.lean
@@ -46,11 +46,11 @@ def AtomM.run {α : Type} (red : TransparencyMode) (m : AtomM α)
 
 /-- Get the index corresponding to an atomic expression, if it has already been encountered, or
 put it in the list of atoms and return the new index, otherwise. -/
-def AtomM.addAtom (e : Expr) : AtomM Nat := do
+def AtomM.addAtom (e : Expr) : AtomM (Nat × Expr) := do
   let c ← get
   for h : i in [:c.atoms.size] do
     if ← withTransparency (← read).red <| isDefEq e c.atoms[i] then
-      return i
-  modifyGet fun c ↦ (c.atoms.size, { c with atoms := c.atoms.push e })
+      return (i, c.atoms[i])
+  modifyGet fun c ↦ ((c.atoms.size, e), { c with atoms := c.atoms.push e })
 
 end Mathlib.Tactic
diff --git a/MathlibTest/abel.lean b/MathlibTest/abel.lean
index d59304f17cbfb..907f94d654e91 100644
--- a/MathlibTest/abel.lean
+++ b/MathlibTest/abel.lean
@@ -141,3 +141,13 @@ example [AddCommGroup α] (x y z : α) (h : False) (w : x - x = y + z) : False :
   abel_nf at *
   guard_hyp w : 0 = y + z
   assumption
+
+-- test that when `abel_nf` normalizes multiple expressions which contain a particular atom, it uses
+-- a form for that atom which is consistent between expressions
+example (x : ℤ) (R : ℤ → ℤ → Prop) (hR : Reflexive R) : True := by
+  let a := x
+  have : R (a + x) (x + a) := by
+    abel_nf
+    guard_target = R ((2:ℤ) • a) ((2:ℤ) • a)
+    apply hR
+  trivial
diff --git a/MathlibTest/ring.lean b/MathlibTest/ring.lean
index ffdfe755e4dec..19e3f86325d71 100644
--- a/MathlibTest/ring.lean
+++ b/MathlibTest/ring.lean
@@ -84,6 +84,16 @@ example (x : ℝ) (hx : x ≠ 0) :
   field_simp
   ring
 
+-- 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
+example (x : ℤ) (R : ℤ → ℤ → Prop) : True := by
+  let a := x
+  have : R (a + x) (x + a) := by
+    ring_nf
+    guard_target = R (a * 2) (a * 2)
+    exact test_sorry
+  trivial
+
 -- As reported at
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ring_nf.20failing.20to.20fully.20normalize
 example (x : ℤ) (h : x - x + x = 0) : x = 0 := by

From 732ad024a6cd4cba57775816b91667faea554b0f Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Fri, 15 Nov 2024 18:21:04 -0500
Subject: [PATCH 02/15] fix

---
 Mathlib/Tactic/Polyrith.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/Polyrith.lean b/Mathlib/Tactic/Polyrith.lean
index 57ef95ad04cbb..50e42c8eecbd1 100644
--- a/Mathlib/Tactic/Polyrith.lean
+++ b/Mathlib/Tactic/Polyrith.lean
@@ -133,7 +133,7 @@ partial def parse {u : Level} {α : Q(Type u)} (sα : Q(CommSemiring $α))
     (c : Ring.Cache sα) (e : Q($α)) : AtomM Poly := do
   let els := do
     try pure <| Poly.const (← (← NormNum.derive e).toRat)
-    catch _ => pure <| Poly.var (← addAtom e)
+    catch _ => pure <| Poly.var (← addAtom e).1
   let .const n _ := (← withReducible <| whnf e).getAppFn | els
   match n, c.rα with
   | ``HAdd.hAdd, _ | ``Add.add, _ => match e with

From f9ce2759d03b972b4b62d7b71fda43cd63ff7029 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Fri, 15 Nov 2024 21:20:04 -0500
Subject: [PATCH 03/15] adjust tests

---
 MathlibTest/abel.lean | 15 ++++++++++++---
 MathlibTest/ring.lean | 18 +++++++++++++++---
 2 files changed, 27 insertions(+), 6 deletions(-)

diff --git a/MathlibTest/abel.lean b/MathlibTest/abel.lean
index 907f94d654e91..bf383880c78f7 100644
--- a/MathlibTest/abel.lean
+++ b/MathlibTest/abel.lean
@@ -142,12 +142,21 @@ example [AddCommGroup α] (x y z : α) (h : False) (w : x - x = y + z) : False :
   guard_hyp w : 0 = y + z
   assumption
 
--- test that when `abel_nf` normalizes multiple expressions which contain a particular atom, it uses
--- a form for that atom which is consistent between expressions
+/-
+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 • a` 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
   let a := x
   have : R (a + x) (x + a) := by
     abel_nf
-    guard_target = R ((2:ℤ) • a) ((2:ℤ) • a)
+    guard_target =ₛ R ((2:ℤ) • a) ((2:ℤ) • a)
     apply hR
   trivial
diff --git a/MathlibTest/ring.lean b/MathlibTest/ring.lean
index 19e3f86325d71..93d7dd6dd0fe3 100644
--- a/MathlibTest/ring.lean
+++ b/MathlibTest/ring.lean
@@ -84,13 +84,25 @@ example (x : ℝ) (hx : x ≠ 0) :
   field_simp
   ring
 
--- 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
+/-
+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 `a * 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
   let a := x
   have : R (a + x) (x + a) := by
     ring_nf
-    guard_target = R (a * 2) (a * 2)
+    guard_target =ₛ R (a * 2) (a * 2)
     exact test_sorry
   trivial
 

From 4e567c4c7861e93952f2d6e5db6e164bacc4cd5f Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Mon, 18 Nov 2024 13:53:32 -0500
Subject: [PATCH 04/15] new docstring

---
 Mathlib/Util/AtomM.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Util/AtomM.lean b/Mathlib/Util/AtomM.lean
index 59a2ec70a7540..da5962d3c8e38 100644
--- a/Mathlib/Util/AtomM.lean
+++ b/Mathlib/Util/AtomM.lean
@@ -44,8 +44,10 @@ def AtomM.run {α : Type} (red : TransparencyMode) (m : AtomM α)
     MetaM α :=
   (m { red, evalAtom }).run' {}
 
-/-- Get the index corresponding to an atomic expression, if it has already been encountered, or
-put it in the list of atoms and return the new index, otherwise. -/
+/-- If an atomic expression has already been encountered, get the index and the stored form of the
+atom (which will be defeq at the specified transparency, but not necessarily syntactically equal).
+If the atomic expression has *not* already been encountered, store it in the list of atoms, and
+return the new index (and the stored form of the atom, which will be itself). -/
 def AtomM.addAtom (e : Expr) : AtomM (Nat × Expr) := do
   let c ← get
   for h : i in [:c.atoms.size] do

From 6d962f60e6a0215a66ad4cac2b72bff8e4e89f00 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Mon, 18 Nov 2024 13:59:07 -0500
Subject: [PATCH 05/15] Qq version

---
 Mathlib/Tactic/Module.lean     | 3 +--
 Mathlib/Tactic/Ring/Basic.lean | 9 +++------
 Mathlib/Util/AtomM.lean        | 8 ++++++++
 3 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Tactic/Module.lean b/Mathlib/Tactic/Module.lean
index 015c5296d96da..fa5424c828c25 100644
--- a/Mathlib/Tactic/Module.lean
+++ b/Mathlib/Tactic/Module.lean
@@ -464,8 +464,7 @@ partial def parse (iM : Q(AddCommMonoid $M)) (x : Q($M)) :
     pure ⟨0, q(Nat), q(Nat.instSemiring), q(AddCommGroup.toNatModule), [], q(NF.zero_eq_eval $M)⟩
   /- anything else should be treated as an atom -/
   | _ =>
-    let (k, x') ← AtomM.addAtom x
-    have x' : Q($M) := x'
+    let (k, x') ← AtomM.addAtomQ x
     pure ⟨0, q(Nat), q(Nat.instSemiring), q(AddCommGroup.toNatModule), [((q(1), x'), k)],
       (q(NF.atom_eq_eval $x'):)⟩
 
diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean
index be4dd945a0c12..188d4b92dd43f 100644
--- a/Mathlib/Tactic/Ring/Basic.lean
+++ b/Mathlib/Tactic/Ring/Basic.lean
@@ -513,8 +513,7 @@ partial def ExBase.evalNatCast {a : Q(ℕ)} (va : ExBase sℕ a) : AtomM (Result
   match va with
   | .atom _ => do
     let a' : Q($α) := q($a)
-    let (i, b) ← addAtom a'
-    let b' : Q($α) := b
+    let (i, b') ← addAtomQ a'
     pure ⟨b', ExBase.atom i, (q(Eq.refl $b') : Expr)⟩
   | .sum va => do
     let ⟨_, vc, p⟩ ← va.evalNatCast
@@ -953,8 +952,7 @@ Evaluates an atom, an expression where `ring` can find no additional structure.
 def evalAtom (e : Q($α)) : AtomM (Result (ExSum sα) e) := do
   let r ← (← read).evalAtom e
   have e' : Q($α) := r.expr
-  let (i, a) ← addAtom e'
-  have a' : Q($α) := a
+  let (i, a') ← addAtomQ e'
   let ve' := (ExBase.atom i (e := a')).toProd (ExProd.mkNat sℕ 1).2 |>.toSum
   pure ⟨_, ve', match r.proof? with
   | none => (q(atom_pf $e) : Expr)
@@ -980,8 +978,7 @@ variable (dα : Q(DivisionRing $α))
 /-- Applies `⁻¹` to a polynomial to get an atom. -/
 def evalInvAtom (a : Q($α)) : AtomM (Result (ExBase sα) q($a⁻¹)) := do
   let a' : Q($α) := q($a⁻¹)
-  let (i, b) ← addAtom a'
-  let b' : Q($α) := b
+  let (i, b') ← addAtomQ a'
   pure ⟨b', ExBase.atom i, (q(Eq.refl $b') : Expr)⟩
 
 /-- Inverts a polynomial `va` to get a normalized result polynomial.
diff --git a/Mathlib/Util/AtomM.lean b/Mathlib/Util/AtomM.lean
index da5962d3c8e38..e7396c20b7ef3 100644
--- a/Mathlib/Util/AtomM.lean
+++ b/Mathlib/Util/AtomM.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Init
 import Lean.Meta.Tactic.Simp.Types
+import Qq
 
 /-!
 # A monad for tracking and deduplicating atoms
@@ -55,4 +56,11 @@ def AtomM.addAtom (e : Expr) : AtomM (Nat × Expr) := do
       return (i, c.atoms[i])
   modifyGet fun c ↦ ((c.atoms.size, e), { c with atoms := c.atoms.push e })
 
+open Qq in
+/-- If an atomic expression has already been encountered, get the index and the stored form of the
+atom (which will be defeq at the specified transparency, but not necessarily syntactically equal).
+If the atomic expression has *not* already been encountered, store it in the list of atoms, and
+return the new index (and the stored form of the atom, which will be itself). -/
+def AtomM.addAtomQ {u : Level} {α : Q(Type u)} (e : Q($α)) : AtomM (Nat × Q($α)) := AtomM.addAtom e
+
 end Mathlib.Tactic

From b51be4406902c941a3fb76a9eb30afb17ce17a92 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Mon, 18 Nov 2024 14:29:41 -0500
Subject: [PATCH 06/15] change test from let to abbrev

---
 MathlibTest/abel.lean | 13 +++++++------
 MathlibTest/ring.lean | 13 +++++++------
 2 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/MathlibTest/abel.lean b/MathlibTest/abel.lean
index bf383880c78f7..305faf161d664 100644
--- a/MathlibTest/abel.lean
+++ b/MathlibTest/abel.lean
@@ -142,21 +142,22 @@ example [AddCommGroup α] (x y z : α) (h : False) (w : x - x = y + z) : False :
   guard_hyp w : 0 = y + z
   assumption
 
+abbrev myId (a : ℤ) : ℤ := a
+
 /-
 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 • a` 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.
+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
-  let a := x
-  have : R (a + x) (x + a) := by
+  have : R (myId x + x) (x + myId x) := by
     abel_nf
-    guard_target =ₛ R ((2:ℤ) • a) ((2:ℤ) • a)
+    guard_target =ₛ R ((2:ℤ) • myId x) ((2:ℤ) • myId x)
     apply hR
   trivial
diff --git a/MathlibTest/ring.lean b/MathlibTest/ring.lean
index 93d7dd6dd0fe3..36d7c2bce48d8 100644
--- a/MathlibTest/ring.lean
+++ b/MathlibTest/ring.lean
@@ -84,25 +84,26 @@ example (x : ℝ) (hx : x ≠ 0) :
   field_simp
   ring
 
+abbrev myId (a : ℤ) : ℤ := a
+
 /-
 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 `a * 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.
+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
-  let a := x
-  have : R (a + x) (x + a) := by
+  have : R (myId x + x) (x + myId x) := by
     ring_nf
-    guard_target =ₛ R (a * 2) (a * 2)
+    guard_target =ₛ R (myId x * 2) (myId x * 2)
     exact test_sorry
   trivial
 

From 38609a0f650c85d953f514942d61e113be72c7f8 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Tue, 19 Nov 2024 11:08:25 -0500
Subject: [PATCH 07/15] Apply suggestions from code review

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
---
 Mathlib/Util/AtomM.lean | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Util/AtomM.lean b/Mathlib/Util/AtomM.lean
index e7396c20b7ef3..dadcc738fee02 100644
--- a/Mathlib/Util/AtomM.lean
+++ b/Mathlib/Util/AtomM.lean
@@ -48,7 +48,10 @@ def AtomM.run {α : Type} (red : TransparencyMode) (m : AtomM α)
 /-- If an atomic expression has already been encountered, get the index and the stored form of the
 atom (which will be defeq at the specified transparency, but not necessarily syntactically equal).
 If the atomic expression has *not* already been encountered, store it in the list of atoms, and
-return the new index (and the stored form of the atom, which will be itself). -/
+return the new index (and the stored form of the atom, which will be itself).
+
+In a normalizing tactic, the expression returned by `addAtom` should be considered the normal form.
+-/
 def AtomM.addAtom (e : Expr) : AtomM (Nat × Expr) := do
   let c ← get
   for h : i in [:c.atoms.size] do
@@ -60,7 +63,9 @@ open Qq in
 /-- If an atomic expression has already been encountered, get the index and the stored form of the
 atom (which will be defeq at the specified transparency, but not necessarily syntactically equal).
 If the atomic expression has *not* already been encountered, store it in the list of atoms, and
-return the new index (and the stored form of the atom, which will be itself). -/
+return the new index (and the stored form of the atom, which will be itself).
+
+In a normalizing tactic, the expression returned by `addAtom` should be considered the normal form. -/
 def AtomM.addAtomQ {u : Level} {α : Q(Type u)} (e : Q($α)) : AtomM (Nat × Q($α)) := AtomM.addAtom e
 
 end Mathlib.Tactic

From bbd9e2d19b91f3cb2d9353fd0b2b066da927481a Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Tue, 19 Nov 2024 12:21:30 -0500
Subject: [PATCH 08/15] Update Mathlib/Util/AtomM.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Util/AtomM.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Util/AtomM.lean b/Mathlib/Util/AtomM.lean
index dadcc738fee02..f4bb09ee3579b 100644
--- a/Mathlib/Util/AtomM.lean
+++ b/Mathlib/Util/AtomM.lean
@@ -66,6 +66,9 @@ If the atomic expression has *not* already been encountered, store it in the lis
 return the new index (and the stored form of the atom, which will be itself).
 
 In a normalizing tactic, the expression returned by `addAtom` should be considered the normal form. -/
-def AtomM.addAtomQ {u : Level} {α : Q(Type u)} (e : Q($α)) : AtomM (Nat × Q($α)) := AtomM.addAtom e
+def AtomM.addAtomQ {u : Level} {α : Q(Type u)} (e : Q($α)) :
+    AtomM (Nat × {e' : Q($α) // $e =Q $e'}) := do
+  let (n, e') ← AtomM.addAtom e
+  return (n, ⟨e, ⟨⟩⟩)
 
 end Mathlib.Tactic

From 525cf96dba0de3a3a2cfbffea051728553b285f7 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Tue, 19 Nov 2024 19:16:33 -0500
Subject: [PATCH 09/15] fixes

---
 Mathlib/Tactic/Module.lean     | 2 +-
 Mathlib/Tactic/Ring/Basic.lean | 6 +++---
 Mathlib/Util/AtomM.lean        | 5 +++--
 3 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Tactic/Module.lean b/Mathlib/Tactic/Module.lean
index fa5424c828c25..1ebbe4bd32677 100644
--- a/Mathlib/Tactic/Module.lean
+++ b/Mathlib/Tactic/Module.lean
@@ -464,7 +464,7 @@ partial def parse (iM : Q(AddCommMonoid $M)) (x : Q($M)) :
     pure ⟨0, q(Nat), q(Nat.instSemiring), q(AddCommGroup.toNatModule), [], q(NF.zero_eq_eval $M)⟩
   /- anything else should be treated as an atom -/
   | _ =>
-    let (k, x') ← AtomM.addAtomQ x
+    let (k, ⟨x', _⟩) ← AtomM.addAtomQ x
     pure ⟨0, q(Nat), q(Nat.instSemiring), q(AddCommGroup.toNatModule), [((q(1), x'), k)],
       (q(NF.atom_eq_eval $x'):)⟩
 
diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean
index 188d4b92dd43f..e1c25118d091d 100644
--- a/Mathlib/Tactic/Ring/Basic.lean
+++ b/Mathlib/Tactic/Ring/Basic.lean
@@ -513,7 +513,7 @@ partial def ExBase.evalNatCast {a : Q(ℕ)} (va : ExBase sℕ a) : AtomM (Result
   match va with
   | .atom _ => do
     let a' : Q($α) := q($a)
-    let (i, b') ← addAtomQ a'
+    let (i, ⟨b', _⟩) ← addAtomQ a'
     pure ⟨b', ExBase.atom i, (q(Eq.refl $b') : Expr)⟩
   | .sum va => do
     let ⟨_, vc, p⟩ ← va.evalNatCast
@@ -952,7 +952,7 @@ Evaluates an atom, an expression where `ring` can find no additional structure.
 def evalAtom (e : Q($α)) : AtomM (Result (ExSum sα) e) := do
   let r ← (← read).evalAtom e
   have e' : Q($α) := r.expr
-  let (i, a') ← addAtomQ e'
+  let (i, ⟨a', _⟩) ← addAtomQ e'
   let ve' := (ExBase.atom i (e := a')).toProd (ExProd.mkNat sℕ 1).2 |>.toSum
   pure ⟨_, ve', match r.proof? with
   | none => (q(atom_pf $e) : Expr)
@@ -978,7 +978,7 @@ variable (dα : Q(DivisionRing $α))
 /-- Applies `⁻¹` to a polynomial to get an atom. -/
 def evalInvAtom (a : Q($α)) : AtomM (Result (ExBase sα) q($a⁻¹)) := do
   let a' : Q($α) := q($a⁻¹)
-  let (i, b') ← addAtomQ a'
+  let (i, ⟨b', _⟩) ← addAtomQ a'
   pure ⟨b', ExBase.atom i, (q(Eq.refl $b') : Expr)⟩
 
 /-- Inverts a polynomial `va` to get a normalized result polynomial.
diff --git a/Mathlib/Util/AtomM.lean b/Mathlib/Util/AtomM.lean
index f4bb09ee3579b..1fdab502a7ba1 100644
--- a/Mathlib/Util/AtomM.lean
+++ b/Mathlib/Util/AtomM.lean
@@ -65,10 +65,11 @@ atom (which will be defeq at the specified transparency, but not necessarily syn
 If the atomic expression has *not* already been encountered, store it in the list of atoms, and
 return the new index (and the stored form of the atom, which will be itself).
 
-In a normalizing tactic, the expression returned by `addAtom` should be considered the normal form. -/
+In a normalizing tactic, the expression returned by `addAtom` should be considered the normal form.
+-/
 def AtomM.addAtomQ {u : Level} {α : Q(Type u)} (e : Q($α)) :
     AtomM (Nat × {e' : Q($α) // $e =Q $e'}) := do
   let (n, e') ← AtomM.addAtom e
-  return (n, ⟨e, ⟨⟩⟩)
+  return (n, ⟨e', ⟨⟩⟩)
 
 end Mathlib.Tactic

From efcaf10658b109275c51111d93fc92968aa68826 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 20 Nov 2024 00:44:58 +0000
Subject: [PATCH 10/15] tidy using addAtomQ

---
 Mathlib/Tactic/Ring/Basic.lean | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean
index e1c25118d091d..b5dacb13e9ab5 100644
--- a/Mathlib/Tactic/Ring/Basic.lean
+++ b/Mathlib/Tactic/Ring/Basic.lean
@@ -512,9 +512,8 @@ mutual
 partial def ExBase.evalNatCast {a : Q(ℕ)} (va : ExBase sℕ a) : AtomM (Result (ExBase sα) q($a)) :=
   match va with
   | .atom _ => do
-    let a' : Q($α) := q($a)
-    let (i, ⟨b', _⟩) ← addAtomQ a'
-    pure ⟨b', ExBase.atom i, (q(Eq.refl $b') : Expr)⟩
+    let (i, ⟨b', _⟩) ← addAtomQ q($a)
+    pure ⟨b', ExBase.atom i, q(Eq.refl $b')⟩
   | .sum va => do
     let ⟨_, vc, p⟩ ← va.evalNatCast
     pure ⟨_, .sum vc, p⟩
@@ -977,9 +976,8 @@ variable (dα : Q(DivisionRing $α))
 
 /-- Applies `⁻¹` to a polynomial to get an atom. -/
 def evalInvAtom (a : Q($α)) : AtomM (Result (ExBase sα) q($a⁻¹)) := do
-  let a' : Q($α) := q($a⁻¹)
-  let (i, ⟨b', _⟩) ← addAtomQ a'
-  pure ⟨b', ExBase.atom i, (q(Eq.refl $b') : Expr)⟩
+  let (i, ⟨b', _⟩) ← addAtomQ q($a⁻¹)
+  pure ⟨b', ExBase.atom i, q(Eq.refl $b')⟩
 
 /-- Inverts a polynomial `va` to get a normalized result polynomial.
 

From c5b729d5eda1f56ed2aca754cce6558108dce035 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Tue, 19 Nov 2024 20:35:40 -0500
Subject: [PATCH 11/15] Update Mathlib/Tactic/Module.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Tactic/Module.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/Module.lean b/Mathlib/Tactic/Module.lean
index 1ebbe4bd32677..e06d5ce2088c2 100644
--- a/Mathlib/Tactic/Module.lean
+++ b/Mathlib/Tactic/Module.lean
@@ -466,7 +466,7 @@ partial def parse (iM : Q(AddCommMonoid $M)) (x : Q($M)) :
   | _ =>
     let (k, ⟨x', _⟩) ← AtomM.addAtomQ x
     pure ⟨0, q(Nat), q(Nat.instSemiring), q(AddCommGroup.toNatModule), [((q(1), x'), k)],
-      (q(NF.atom_eq_eval $x'):)⟩
+      q(NF.atom_eq_eval $x')⟩
 
 /-- Given expressions `R` and `M` representing types such that `M`'s is a module over `R`'s, and
 given two terms `l₁`, `l₂` of type `qNF R M`, i.e. lists of `(Q($R) × Q($M)) × ℕ`s (two `Expr`s

From 45b7de9a8f78d601cfbd6f4ca85bee12097af57c Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 20 Nov 2024 22:00:29 +0000
Subject: [PATCH 12/15] make tests more robust

---
 MathlibTest/abel.lean | 13 +++++--------
 MathlibTest/ring.lean | 16 +++++-----------
 2 files changed, 10 insertions(+), 19 deletions(-)

diff --git a/MathlibTest/abel.lean b/MathlibTest/abel.lean
index 305faf161d664..2e1c131477ac1 100644
--- a/MathlibTest/abel.lean
+++ b/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
diff --git a/MathlibTest/ring.lean b/MathlibTest/ring.lean
index 36d7c2bce48d8..134826b325718 100644
--- a/MathlibTest/ring.lean
+++ b/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
 

From 9cd0c2b88e9ce7322d77097e263d50f93e3c2da5 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 20 Nov 2024 22:03:34 +0000
Subject: [PATCH 13/15] comment

---
 Mathlib/Util/AtomM.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Util/AtomM.lean b/Mathlib/Util/AtomM.lean
index 1fdab502a7ba1..bc85531a753a4 100644
--- a/Mathlib/Util/AtomM.lean
+++ b/Mathlib/Util/AtomM.lean
@@ -65,7 +65,9 @@ atom (which will be defeq at the specified transparency, but not necessarily syn
 If the atomic expression has *not* already been encountered, store it in the list of atoms, and
 return the new index (and the stored form of the atom, which will be itself).
 
-In a normalizing tactic, the expression returned by `addAtom` should be considered the normal form.
+In a normalizing tactic, the expression returned by `addAtomQ` should be considered the normal form.
+
+This is a strongly-typed version of `AtomM.addAtom` for code using `Qq`.
 -/
 def AtomM.addAtomQ {u : Level} {α : Q(Type u)} (e : Q($α)) :
     AtomM (Nat × {e' : Q($α) // $e =Q $e'}) := do

From e8749df6867be4a227e3306394665a0aded8ccbb Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed, 20 Nov 2024 21:40:01 -0500
Subject: [PATCH 14/15] different test style

---
 MathlibTest/abel.lean | 29 ++++++++++++++++++++---------
 MathlibTest/ring.lean | 42 +++++++++++++++++++++++++-----------------
 2 files changed, 45 insertions(+), 26 deletions(-)

diff --git a/MathlibTest/abel.lean b/MathlibTest/abel.lean
index 2e1c131477ac1..35980a7ec09dd 100644
--- a/MathlibTest/abel.lean
+++ b/MathlibTest/abel.lean
@@ -142,19 +142,30 @@ example [AddCommGroup α] (x y z : α) (h : False) (w : x - x = y + z) : False :
   guard_hyp w : 0 = y + z
   assumption
 
+section
 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.
+form for that atom which is consistent between expressions.
+
+We can't use `guard_hyp h :ₛ` here, as while it does tell apart `x` and `myId x`, it also complains
+about differing instance paths.
+-/
+/--
+info: α : Type ?u.68666
+a b : α
+x : ℤ
+R : ℤ → ℤ → Prop
+hR : Reflexive R
+h : R (2 • myId x) (2 • myId x)
+⊢ True
 -/
+#guard_msgs (info) in
 example (x : ℤ) (R : ℤ → ℤ → Prop) (hR : Reflexive R) : True := by
-  have : R (myId x + x) (x + myId x) := by
-    abel_nf
-    -- `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
+  have h : R (myId x + x) (x + myId x) := hR ..
+  abel_nf at h
+  trace_state
   trivial
+
+end
diff --git a/MathlibTest/ring.lean b/MathlibTest/ring.lean
index 134826b325718..8a0a07fea0178 100644
--- a/MathlibTest/ring.lean
+++ b/MathlibTest/ring.lean
@@ -84,23 +84,6 @@ example (x : ℝ) (hx : x ≠ 0) :
   field_simp
   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.
--/
-example (x : ℤ) (R : ℤ → ℤ → Prop) : True := by
-  have : R (myId x + x) (x + myId x) := by
-    ring_nf
-    -- `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
-
 -- As reported at
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ring_nf.20failing.20to.20fully.20normalize
 example (x : ℤ) (h : x - x + x = 0) : x = 0 := by
@@ -195,3 +178,28 @@ example {n : ℝ} (_hn : 0 ≤ n) : (n + 1 / 2) ^ 2 * (n + 1 + 1 / 3) ≤ (n + 1
   ring_nf
   trace_state
   exact test_sorry
+
+section
+abbrev myId (a : ℤ) : ℤ := a
+
+/-
+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.
+
+We can't use `guard_hyp h :ₛ` here, as while it does tell apart `x` and `myId x`, it also complains
+about differing instance paths.
+-/
+/--
+info: x : ℤ
+R : ℤ → ℤ → Prop
+h : R (myId x * 2) (myId x * 2)
+⊢ True
+-/
+#guard_msgs (info) in
+example (x : ℤ) (R : ℤ → ℤ → Prop) : True := by
+  have h : R (myId x + x) (x + myId x) := test_sorry
+  ring_nf at h
+  trace_state
+  trivial
+
+end

From 86eb01d0682c50ff67dd1f4871cb89369b205a27 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed, 20 Nov 2024 22:23:41 -0500
Subject: [PATCH 15/15] pp.mvars

---
 MathlibTest/abel.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/MathlibTest/abel.lean b/MathlibTest/abel.lean
index 35980a7ec09dd..f2235b46071cf 100644
--- a/MathlibTest/abel.lean
+++ b/MathlibTest/abel.lean
@@ -153,7 +153,7 @@ We can't use `guard_hyp h :ₛ` here, as while it does tell apart `x` and `myId
 about differing instance paths.
 -/
 /--
-info: α : Type ?u.68666
+info: α : Type _
 a b : α
 x : ℤ
 R : ℤ → ℤ → Prop
@@ -162,6 +162,7 @@ h : R (2 • myId x) (2 • myId x)
 ⊢ True
 -/
 #guard_msgs (info) in
+set_option pp.mvars false in
 example (x : ℤ) (R : ℤ → ℤ → Prop) (hR : Reflexive R) : True := by
   have h : R (myId x + x) (x + myId x) := hR ..
   abel_nf at h