funext $ λ x, rfl

Stream: general

[Kenny Lau]

conjecture: everything that can be proven using funext $ λ x, rfl can be proven using rfl

[Mario Carneiro]

that's correct (modulo funny business regarding algorithmic equality not really being definitional equality)

[Kenny Lau]

could you expand on your parentheses

[Mario Carneiro]

Sometimes lean doesn't know when to eta expand stuff

[Kenny Lau]

could you provide an example

[Mario Carneiro]

def foo : true = true → plift true := @eq.rec Prop true (λ p, plift true) ⟨trivial⟩ true
def bar : true = true → plift true := @eq.rec Prop true (λ p, plift p) ⟨trivial⟩ true
example : foo = bar := funext $ λ x, rfl
example : foo = bar := rfl

[Kenny Lau]

ah, that funny rec business

[Patrick Massot]

Mario, aren't you sleeping?

[Kenny Lau]

LOL

[Kevin Buzzard]

I found myself writing this yesterday:

[Kevin Buzzard]

Hid :=  λ U OU,funext (λ x,subtype.eq rfl),
Hcomp :=  λ U V W OU OV OW HUV HVW,funext (λ x, subtype.eq rfl)

[Kevin Buzzard]

and I couldn't move the rfl

[Kenny Lau]

subtype.eq rfl cannot be replaced by rfl

[Kevin Buzzard]

and I could understand why subtype.eq wasn't a simp lemma

[Kenny Lau]

well it's just congr

[Kevin Buzzard]

because it's a1.val = a2.val → a1 = a2

[Kevin Buzzard]

which doesn't look great for simp

[Kevin Buzzard]

but then I found

[Kevin Buzzard]

subtype.mk_eq_mk

[Kevin Buzzard]

which is an iff and is marked as a simp lemma

[Kevin Buzzard]

so I was hopeful that by simp would work, but I couldn't get it to