`ac_rfl` unable to solve a goal using commutativity

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The ac_rfl tactic cannot solve a seemingly obvious goal by using commutativity provided by the Std.Commutative instance in the hypothesis.

Steps to Reproduce

theorem Option.merge_comm {α : Type} (f : α → α → α) [h : Std.Commutative f] (a b : Option α) :
  Option.merge f a b = Option.merge f b a := by
  cases a <;> cases b <;> simp [Option.merge]
  ac_rfl

Expected behavior: ac_rfl solves the goal

Actual behavior: ac_rfl fails, reporting tactic 'rfl' failed, equality lhs ... is not definitionally equal to rhs ...

Versions

Lean 4.19.0-nightly-2025-03-04
Target: x86_64-unknown-linux-gnu

Additional Information

ac_rfl works as intended on the associativity proof goal below.

theorem Option.merge_assoc {α : Type} (f : α → α → α) [Std.Associative f] (a b c : Option α) :
  Option.merge f (Option.merge f a b) c = Option.merge f a (Option.merge f b c) := by
  cases a <;> cases b <;> cases c <;> simp [Option.merge]
  ac_rfl

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal Option.merge_comm reproduction and inspect the ac_rfl tactic behavior when commutativity comes from Std.Commutative. Compare it with the provided Option.merge_assoc case, then run the reproduction against the reported Lean nightly version. Done means ac_rfl solves the commutative goal while preserving the associativity behavior.