dsimp unfolds definition in post-phase, not pre-phase

I stumbled over a discrepancy in how dsimp and simp unfold declarations: simp applies them before simplifying arguments, dsimp after:

def x := 0
def y := 0

def const (x : α) (_ : β) : α  := x

set_option trace.Meta.Tactic.simp.rewrite true

/--
info: [Meta.Tactic.simp.rewrite] unfold const, const x y ==> x
[Meta.Tactic.simp.rewrite] unfold x, x ==> 0
[Meta.Tactic.simp.rewrite] eq_self:1000, 0 = 0 ==> True
-/
#guard_msgs in
example : const x y = 0 := by simp [const, x, y]

/--
info: [Meta.Tactic.simp.rewrite] unfold x, x ==> 0
[Meta.Tactic.simp.rewrite] unfold y, y ==> 0
[Meta.Tactic.simp.rewrite] unfold const, const 0 0 ==> 0
-/
#guard_msgs in
example : const x y = 0 := by dsimp [const, x, y]

/--
info: [Meta.Tactic.simp.rewrite] unfold x, x ==> 0
[Meta.Tactic.simp.rewrite] unfold y, y ==> 0
[Meta.Tactic.simp.rewrite] unfold const, const 0 0 ==> 0
-/
#guard_msgs in
example : const x y = 0 := by dsimp [↓ const, x, y]

/--
info: [Meta.Tactic.simp.rewrite] ↓ const.eq_def:1000, const x y ==> x
[Meta.Tactic.simp.rewrite] unfold x, x ==> 0
-/
#guard_msgs in
example : const x y = 0 := by dsimp [↓ const.eq_def, x, y]

I don’t see a big problem with this per se, but it’s a discrepancy that may cause (performance) surprises. Related to #6960 in that sense.

Version

Lean 4.18.0-nightly-2025-02-05

Reproduce the reported examples in Lean 4.18.0-nightly-2025-02-05, using the simp trace and #guard_msgs checks shown in the issue. Compare the unfolding order for simp, dsimp, and the ↓ forms, then inspect the dsimp and simp tactic entry points. The intended ordering or performance outcome still needs clarification before defining done.