A linter to prevent `x = x` lemmas

Stream: general

[Eric Wieser]

I just noticed that we have a simp lemma with matching LHS and RHS, docs#submodule.quotient.mk_eq_mk. Presumably simp just ignores this at the moment. How hard would it be to teach the simp linter to reject this?

[Gabriel Ebner]

I would insert a call to is_simp_eq around here: https://github.com/leanprover-community/mathlib/blob/132328c4dd48da87adca5d408ca54f315282b719/src/tactic/lint/simp.lean#L89

[Eric Wieser]

Another one: docs#continuous_map.id_coe

[Eric Wieser]

(found in #8180)