Heuristically searching for incorrect theorem names

Stream: mathlib4

[Emilie (Shad Amethyst)]

Following the issue spotted by @Enrico Borba, I tried to see if I could detect those kind of issues automatically, namely instances of a theorem name mentionning something that is neither in its arguments nor in its return type.
I first tried to parse the code manually, to extract a list of theorems and their arguments, but it turns out that we already have this, through https://leanprover-community.github.io/mathlib4_docs/ :)
My code is temporarily hosted here. You can also find the output of my code, though it is quite noisy because of the reasons listed below.

So, there are several things I uncovered that way:

• there are a lot of places in mathlib that use ≥ instead of ≤
• inv seems to have more meanings that I can count: it's used to refer to symm, comp, to multiplicative inverses, to refer to cancellation, etc. The more meanings inv has, the less it means anything, so maybe something should be done about it
• since types are erased in the docs, theorems like docs#AddCircle.norm_neg_period or docs#ZMod.isSquare_neg_one_mul visually look tautological
• pos also has ambiguous meaning: in some places it means 0 < x, but in other places like docs#MeasureTheory.integral_norm_eq_pos_sub_neg it's used to refer to 0 ≤ x. It also means "is true", like in docs#iInf_pos
• and, as expected, there is a handful of theorems whose name mention things that their return types and arguments don't contain. There are too many of them to fit here, and I am certainly missing a lot, but here are a few interesting ones:
  • docs#HasDerivWithinAt.liminf_right_slope_le — uses both Ioi and <
  • docs#PNat.pos_of_div_pos — should be pos_of_dvd_pos
  • docs#Zsqrtd.nonneg_smul — should be nonneg_mul
  • docs#nhds_basis_zero_abs_sub_lt — I don't know where the sub comes from
  • docs#Right.pow_neg, docs#Left.pow_neg — should be nsmul_neg, there are a lot of similar issues in that file
  • docs#IsClosed.Icc_subset_of_forall_exists_gt — looks quite odd, the y ∈ Set.Ioi x is not simp-normal, and gt here refers to Set.Ioc
  • docs#IsPrimitiveRoot.pow_sub_one_eq — I'm not sure why Nat.pred is used here
  • docs#HasDerivWithinAt.limsup_slope_le — should be limsup_slope_lt, several other lemmas in this file have this issue
  • docs#Monotone.convex_lt and docs#Monotone.convex_gt — the opposite issue, the first one should be convex_le, and the second one seems to be an exact copy of the former

[Ruben Van de Velde]

What's the issue with Complex.not_lt_zero_iff?

[Emilie (Shad Amethyst)]

Hmm, you're right, the order has a different meaning than what I thought

[Kevin Buzzard]

But most of these are great! Thanks a lot!

[Enrico Borba]

This looks like a fantastic effort!

Emilie (Shad Amethyst) said:

since types are erased in the docs, theorems like docs#AddCircle.norm_neg_period or docs#ZMod.isSquare_neg_one_mul visually look tautological

Autoparam erasure also makes theorems like docs#MeasureTheory.integrableOn_def harder to read, (I can't tell what measure Integrable f is over.