abbrev and fun_prop

Stream: mathlib4

[Sébastien Gouëzel]

I thought that abbrev was supposed to be transparent for most things, but it turns out it is not the case for fun_prop:

import Mathlib
variable {α : Type*} [MeasurableSpace α]
lemma foo : Measurable (id : α → α) := by fun_prop -- works
abbrev my_id (α : Type*) [MeasurableSpace α] : α → α := id
lemma bar : Measurable (my_id α) := by fun_prop -- fails

Is that something that can/should be fixed? @Tomas Skrivan , what do you think?

[Tomas Skrivan]

Yes this should be fixed, transparency is something I struggle with all the time.

[Jireh Loreaux]

probably just missing a whnfR somewhere.

[Tomas Skrivan]

Fixed in #16512

[Tomas Skrivan]

Ugh a test broke, I know what is going on but it will take some time to fix it.

[Tomas Skrivan]

The fix passes CI now :)

[Tomas Skrivan]

While we are at fixing fun_prop. Can I get attention/review to #16371 which fixes some issues with let bindings and free variables.