Can't tag a lemma with `fun_prop`

Stream: general

[Etienne Marion]

Hi! Why can't the following lemma be tagged with fun_prop?

import Mathlib

@[fun_prop, measurability]
lemma measurable_uncurry {ι κ X : Type*} [MeasurableSpace X] :
    Measurable (@Function.uncurry ι κ X) := by
  refine measurable_pi_lambda _ fun p ↦ ?_
  simp only [Function.uncurry]
  fun_prop

[Etienne Marion]

It's weird because I can tag this one:

import Mathlib

@[fun_prop, measurability]
lemma measurable_uncurry {ι κ X : Type*} [MeasurableSpace X] :
    Measurable (@Function.uncurry ι κ X) := by
  refine measurable_pi_lambda _ fun p ↦ ?_
  simp only [Function.uncurry]
  fun_prop

@[fun_prop, measurability]
lemma measurable_equivCurry_symm {ι κ X : Type*} [MeasurableSpace X] :
    Measurable (Equiv.curry ι κ X).symm := measurable_uncurry

but the two functions are actually the same!

[Ruben Van de Velde]

The error is "function in invalid form Function.uncurry"

[Tomas Skrivan]

Functions Function.comp/uncurry, id, HasUncurry.uncurry and considered reducible in fun_prop. Therefore your statement is effectively the same as writing Mesurable (fun f xy => f xy.1 xy.2) and fun_prop should infer this already from other rules.

[Etienne Marion]

Oh you're right, thanks! I had tried fun_prop for (Equiv.curry ι κ X).symm but I didn't do it for Function.uncurry for some reason.