does rfl know about function extensionality?

Stream: mathlib4

[Emily Riehl]

I think about proofs of equality between functions in MLTT as having two steps: (i) first apply function extensionality and (ii) then prove a pointwise equality.

But there are several proofs that I thought would require funext that seem to be solvable now just by rfl. Is rfl more powerful than it used to be? Can someone explain what is going on?

For example, in mathlib we have

@[simp, grind =]
theorem curry_uncurry (f : α → β → φ) : curry (uncurry f) = f :=
  rfl

@[simp, grind =]
theorem uncurry_curry (f : α × β → φ) : uncurry (curry f) = f :=
  funext fun ⟨_a, _b⟩ => rfl

but I think now rfl solves the second goal without the funext.

[Kyle Miller]

This is relying on a feature that's in Lean 4 that wasn't in Lean 3, eta reduction for structures. In the following, (c.1, c.2) is definitionally equal to c:

theorem uncurry_curry (f : α × β → φ) : uncurry (curry f) = f :=
  calc
    uncurry (curry f) = uncurry (fun a b => f (a, b)) := rfl -- unfold `curry`
    _ = fun c => (fun a b => f (a, b)) c.1 c.2 := rfl -- unfold `uncurry`
    _ = fun c => f (c.1, c.2) := rfl -- beta reduce
    _ = fun c => f c := rfl -- eta reduce for `Prod`
    _ = f := rfl -- eta reduce for fun

[Emily Riehl]

I see! You explained this perfectly. Thank you.