fun_prop attribute for Complex.log lemmas?

Stream: mathlib4

[Michael Stoll]

In #18923 I locally add the fun_prop attribute to DifferentiableAt.clog in order to simplify a proof. @Ruben Van de Velde then asked whether it would make sense to add the attribute immediately to the definition in file#Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv . If so, I assume one should add the attribute to all (except the first two) declarations in this file. My question here is whether people think this makes sense: all these lemmas have the side condition x ∈ slitPlane or f x ∈ slitPlane, which fun_prop cannot automatically discharge. On the plus side, fun_prop will tell you exactly this, and so one can fix it by establishing the side condition via have and then do something like fun_prop (disch := assumption) (this is what I do in #18923). Opinions? @Tomas Skrivan

[Yaël Dillies]

I think tagging all those lemmas makes perfect sense?

[Michael Stoll]

(I'd like to decouple this question from the PR since I need the PR in to continue with the material needed for PNT etc.)

[Ruben Van de Velde]

I'm okay with keeping the attribute where it is for this PR as long as you do follow up

[Michael Stoll]

I'll wait for more people to chime in here, and when a consensus emerges that adding the attribute is what we want, I'll make a PR.

[David Loeffler]

I'm not sure if there's any good argument for not using the fun_prop attribute (unless having too many lemmas with this tag creates performance issues?).

Note that some lemmas have fun_prop attribute applied where they're defined, and some others get decorated with this attribute elsewhere, in files under Mathlib/Tactic/FunProp; I'm not quite sure why this is. (I would not be surprised if there are some lemmas getting tagged twice.)

[Riccardo Brasca]

fun_prop is rather recent, I think this is just an historical accident.

[Riccardo Brasca]

Anyway #18923 LGTM

[Michael Stoll]

#19032 adds the fun_prop attribute (where allowed).