gcongr attribute for folded relations

Stream: mathlib4

[Rida Hamadani]

Currently, it is not possible to add the @[gcongr] attribute to lemmas which are of the form f x ∼ f y when the relation is folded, for example this fails:

import Mathlib

@[gcongr]
lemma f_mono {α : Type} {f : α → α} [Preorder α] : Monotone f := by
  sorry

Same applies to similar Props, such as Antitone, StrictMono, etc
I think it would be nice to be able to add this tag to such statements. What do you think?

[Johan Commelin]

Cc @Heather Macbeth @Mario Carneiro

[Mario Carneiro]

I think this is not a good idea, because the relation in question could be implication, in which case this can lead to a lot of ambiguity

[Yaël Dillies]

For now, I've been adding protected versions of these lemmas in the GCongr namespace

[Rida Hamadani]

I wonder if if it would be a good idea to make gcongr resolve the ambiguity for hardcoded Props, the ones that we use a lot in mathlib, like Monotone for example.