Add note to help search similar thms

Stream: mathlib4

[Yi.Yuan]

here are two similar theorems (Int.le_induction_down) and (Nat.decreasingInduction'). Having different names for these two is not very convenient when searching for theorems. Should I add a note under Nat.decreasingInduction that says 'The version for Int, see Int.le_induction_down'?"

[Aaron Liu]

or maybe rename one of them

[Yi.Yuan]

If so, #27443 is my PR. Could someone please help review it?

[Yi.Yuan]

Aaron Liu said:

or maybe rename one of them

So, how can I find all the places where these theorems have appeared in mathlib?

[Aaron Liu]

deprecate one of the names and look at the build warnings

[Yi.Yuan]

So maybe I should change Int.le_induction_down to Int.decreasingInduction

[Eric Wieser]

The naming difference is because one is for Prop and the other Sort

[Yi.Yuan]

However, they are quite similar to each other.

[Aaron Liu]

Maybe we should generalize docs#Int.le_induction_down to be for Sort*

[Ruben Van de Velde]

Yes, that seems sensible