missing @fun_prop?

Stream: mathlib4

[Kevin Buzzard]

import Mathlib

variable (M : Type*) [TopologicalSpace M]

abbrev f :  M × M → M × Mᵐᵒᵖ := Prod.map id MulOpposite.op

example : Continuous (f M) := by continuity
example : Continuous (f M) := by fun_prop -- fails?!

attribute [fun_prop] MulOpposite.continuous_op

example : Continuous (f M) := by fun_prop -- works

Does this just mean "I should just make a PR giving MulOpposite.continuous_op(and ..._unop) the fun_prop attribute" or are things more complicated than this? I've never used fun_prop before. I see continuous_id is tagged continuity but not fun_prop for example, so I'm a bit confused.

[Ruben Van de Velde]

I think you can just add it

[Etienne Marion]

There are regularly PRs which add the fun_prop tag to some lemma which misses it.

[Kevin Buzzard]

#26406 . Why doesn't continuous_id get the fun_prop tag? Presumably fun_prop is seeing through id?

[Floris van Doorn]

continuous_id' has the @[fun_prop] tag, and that is sufficient for fun_prop. Similarly, because docs#Continuous.cexp is @[fun_prop], docs#Complex.continuous_exp doesn't need to be. (the other way around is also fine, IIRC)