unfold working differently in Lean 4

Stream: mathlib4

[Thomas Murrills]

In Lean 3, there's a call to unfold of the form unfold btw at ⊢ h that turns the tactic state

α : Type ?,
_inst_1 : preorder α,
a b c : α,
h : btw a b c
⊢ btw b c a

into the state

α : Type ?,
_inst_1 : preorder α,
a b c : α,
h : a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b
⊢ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b ∨ a ≤ b ∧ b ≤ c

(It's not important what the details are; if people like I can minimize it, though.)

But in Lean 4, the ported version (unfold Btw at h⊢) turns the state

α: Type ?u.4043
inst✝: Preorder α
a b c: α
h: Btw a b c
⊢ Btw b c a

into the more complex

α: Type ?u.4043
inst✝: Preorder α
a b c: α
h: { Btw := fun a b c ↦ a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b }.1 a b c
⊢ { Btw := fun a b c ↦ a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b }.1 b c a

I can recover the Lean 3 version, but I need to apply simp after the unfold (dsimp doesn't work, even though I might naively expect it to—after all, we're just using projections and applying functions, things I would have thought would be definitional).

So it's not really a problem per se, but: is it a sign of something gone awry? Just in case, I thought I'd bring it up.

[Thomas Murrills]

Actually, just made an MWE anyway: :upside_down:

class Foo where foo : Prop
class Bar extends Foo where bar : foo
def baz : Bar where
  foo := True
  bar := by unfold Foo.foo -- unsolved goals

Tactic state at the end:

⊢ { foo := True }.1

Contrast with Lean 3:

class Foo := (foo : Prop)
class Bar extends Foo := (bar : foo)
def baz : Bar := { foo := true, bar := by unfold Foo.foo } -- works

[Thomas Murrills]

Note: if we absorb bar into Foo to avoid an extends, we don't even need to unfold in Lean 4:

class Foo where
  foo : Prop
  bar : foo

def Baz : Foo where
  foo := True
  bar := by trivial

[Thomas Murrills]

(maybe this should be moved to the #lean4 stream, now that I think about it.)