`rw` selects the wrong equation, leading to impossible goals

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

Consider this code:

inductive Expr where
  | Num : Int32 → Expr
  | Plus : Expr → Expr → Expr

open Expr

def opt : Expr → Expr
  | Plus (Num 0) e => opt e
  | Plus e (Num 0) => opt e
  | Plus e₁ e₂ => Plus (opt e₁) (opt e₂)
  | other => other
  
#print eqns opt

theorem l : ∀ e, opt (Plus (Num 0) e) = opt e := by
  intro e
  rw [opt]

Here are the equations generated for opt:

theorem opt.eq_1 : ∀ (e : Expr), opt ((Num { toUInt32 := { toBitVec := 0#32 } }).Plus e) = opt e
theorem opt.eq_2 : ∀ (e : Expr),
  (e = Num { toUInt32 := { toBitVec := 0#32 } } → False) →
    opt (e.Plus (Num { toUInt32 := { toBitVec := 0#32 } })) = opt e
theorem opt.eq_3 : ∀ (e₁ e₂ : Expr),
  (e₁ = Num { toUInt32 := { toBitVec := 0#32 } } → False) →
    (e₂ = Num { toUInt32 := { toBitVec := 0#32 } } → False) → opt (e₁.Plus e₂) = (opt e₁).Plus (opt e₂)
theorem opt.eq_4 : ∀ (x : Expr),
  (∀ (e : Expr), x = (Num { toUInt32 := { toBitVec := 0#32 } }).Plus e → False) →
    (∀ (e : Expr), x = e.Plus (Num { toUInt32 := { toBitVec := 0#32 } }) → False) →
      (∀ (e₁ e₂ : Expr), x = e₁.Plus e₂ → False) → opt x = x

Now, in the theorem, rw, working syntactically, decides not to apply eq_1 or eq_2, opting instead for eq_3, creating two additional goals to show that the first two equations are not applicable, but of course one of these goals is actually unprovable because the first equation is applicable.

erw [opt] does the right thing, as does apply opt.eq_1.

It's pretty clear that this is undesirable behavior and confusing for new users. It's less clear what needs to be fixed here:

• should the generated equations match the syntax used by the user when specifying the equations more closely (which might make this a duplicate of #5282)?
• does rw need to be changed?
• should Int32 be changed to not leak its implementation?
• is this a problem with nat literals?

Context

As reported on Zulip.

Expected behavior: rw [opt] applies the first equation, closing the goal.

Actual behavior: rw [opt] creates multiple confusing goals, two of which are unprovable.

Versions

4.21.0-nightly-2025-05-23 on live.lean-lang.org

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 Expr/opt reproducer in the issue and inspect the generated opt.eq_1 through opt.eq_4 equations. Compare rw [opt] with erw [opt] and apply opt.eq_1 on the Lean nightly test case. Done means rw [opt] selects the applicable first equation and closes the theorem without unprovable side goals.