Preferred proof style for PR (`fun_prop` or explicit proof)

Stream: mathlib4

[Louis Liu]

Hi! I have a small style question for mathlib PRs. If I can close a goal using either fun_prop (disch := assumption) or an explicit proof like exact hf.comp_mul_left hct, then which is the preferred style here (or does it depend on the context) for a mathlib PR? Thanks!

[Michael Rothgang]

My opinion is that tactics are good, and so is avoiding explicit lemma names (when reasonable). In particular:

• if fun_prop were appreciably slow, I would avoid it (this is sometimes an issue with other tactics; it should not occur with fun_prop)
• if the explicit proof is "a bit long", I always prefer the tactic. In your example, I think that's worth it already. For a proof of almost a full line or more, it's no question to me.
• If you don't need to provide a discharger to fun_prop (sometimes you do, often you don't), omitting that makes the proof shorter again :-)

[Louis Liu]

@Michael Rothgang got it, thank you so much!

[Ruben Van de Velde]

Though I'm not sure I'd say that's policy - in this case the proof is trivial enough that either is fine and I'd lean somewhat towards the explicit proof