ac_rfl and defeq atoms

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

ac_rfl sometimes fails when terms are defeq but not equal, which causes unintuitive failures

Steps to Reproduce

Here is an example extracted from actual use in mathlib (https://github.com/leanprover-community/mathlib4/pull/6389#discussion_r1286317448), in this example we are in a situation that can arise mid-proof due to other proof steps using different instances to produce defeq terms.
Here we have to prove a * a + n * a = n * a + a * a, but where the multiplication operations filled in my tc synthesis are defeq but not equal as expressions.
As a result it seems ac_rfl doesn't put the terms in the "right" order. As ac_rfl finishes with rfl it seems reasonable to match terms up to defeq.
The mathlib ring tactic handles this example OK if we move to a full CommRing, but the example here is more general.

import Lean
class Zero (α : Type u) where
  zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
  zero := 0

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

class MulZeroClass (M₀ : Type _) extends Mul M₀, Zero M₀ where
  zero_mul : ∀ a : M₀, 0 * a = 0
  mul_zero : ∀ a : M₀, a * 0 = 0

class AddSemigroup (G : Type u) extends Add G where
  add_assoc : ∀ a b c : G, a + b + c = a + (b + c)

class Semigroup (G : Type u) extends Mul G where
  mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

class CommSemigroup (G : Type u) extends Semigroup G where
  mul_comm : ∀ a b : G, a * b = b * a

class AddCommSemigroup (G : Type u) extends AddSemigroup G where
  add_comm : ∀ a b : G, a + b = b + a

class SemigroupWithZero (S₀ : Type _) extends Semigroup S₀, MulZeroClass S₀

class MulOneClass (M : Type u) extends One M, Mul M where
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a

class AddZeroClass (M : Type u) extends Zero M, Add M where
  zero_add : ∀ a : M, 0 + a = a
  add_zero : ∀ a : M, a + 0 = a

class MulZeroOneClass (M₀ : Type u) extends MulOneClass M₀, MulZeroClass M₀

class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where

class AddCommMonoid (M : Type u) extends AddMonoid M, AddCommSemigroup M

class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
  sub a b := a + -b
  sub_eq_add_neg : ∀ a b : G, a - b = a + -b := by intros; rfl

class AddGroup (A : Type u) extends SubNegMonoid A where
  add_left_neg : ∀ a : A, -a + a = 0

class AddMonoidWithOne (R : Type u) extends AddMonoid R, One R where

class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, MulZeroClass α

class AddCommMonoidWithOne (R : Type _) extends AddMonoidWithOne R, AddCommMonoid R

class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α

variable [NonUnitalSemiring R]

instance : Lean.IsCommutative (. + . : R → R → R) := sorry
instance : Lean.IsAssociative (. + . : R → R → R) := sorry

theorem works (n a : R) : 
  @HMul.hMul _ _ _ (@instHMul R (@Semigroup.toMul R _)) a a + n * a
 =
  @HMul.hMul _ _ _ (@instHMul R _) n a + a * a := by
    ac_rfl

theorem fails (n a : R) : 
  @HMul.hMul _ _ _ (@instHMul R (@Semigroup.toMul R _)) a a + n * a
 =
  @HMul.hMul _ _ _ (@instHMul R (@Semigroup.toMul R _)) n a + a * a := by
    ac_rfl

Expected behavior: ac_rfl completes the proof

Actual behavior: ac_rfl does not fill the goal

Start at the ac_rfl entry point and run the supplied works and fails examples to reproduce the difference between equal and defeq atoms. The work is done when ac_rfl completes the fails theorem while preserving the successful case.