how does this rfl work

Stream: new members

[Kenny Lau]

theorem what (x : PUnit) : x = PUnit.unit := rfl

This looks like magic to me

[Aaron Liu]

x is eta expanded to a structure with no fields

[Kenny Lau]

theorem the (x : α × β) : x = (x.1, x.2) := rfl

right, so like this as well?

[Kenny Lau]

I mean, i'm not complaining that we got auto eta expansion

[Kenny Lau]

what's the range of that eta expansion? does it work with rw and simp as well? or only rfl?

[Aaron Liu]

Yes, Prod is a structure with two fields, and PUnit is a structure with no fields

[Aaron Liu]

Kenny Lau said:

what's the range of that eta expansion? does it work with rw and simp as well? or only rfl?

It's a definitional equality, so it works whenever defeq is tested

[Kevin Buzzard]

Welcome to Lean 4 Kenny :-)