/- The `docBlame` linter reports:
DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
-- Mathlib.Order.RelIso.Basic
#check RelHom.toFun.{u_1, u_2} /- definition missing documentation string -/
#check RelHom.map_rel'.{u_1, u_2} /- definition missing documentation string -/
#check term_→r_ /- definition missing documentation string -/
#check RelHomClass.map_rel.{u_1, u_2, u_3} /- definition missing documentation string -/
#check RelEmbedding.map_rel_iff'.{u_1, u_2} /- definition missing documentation string -/
#check term_↪r_ /- definition missing documentation string -/
#check RelIso.map_rel_iff'.{u_1, u_2} /- definition missing documentation string -/
#check term_≃r_ /- definition missing documentation string -/

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.Order.RelIso.Basic
#check RelEmbedding.inj.{u_2, u_1} /- simp can prove this:
  by simp only [EmbeddingLike.apply_eq_iff_eq]
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].
 -/
#check RelIso.eq_iff_eq.{u_2, u_1} /- simp can prove this:
  by simp only [EmbeddingLike.apply_eq_iff_eq]
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].
 -/

/- The `synTaut` linter reports:
THE FOLLOWING DECLARATIONS ARE SYNTACTIC TAUTOLOGIES. This usually means that they are of the form `∀ a b ... z, e₁ = e₂` where `e₁` and `e₂` are identical expressions. We call declarations of this form syntactic tautologies. Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving basic facts using `rfl`, when elaboration results in a different term than the user intended. You should check that the declaration really says what you think it does. -/
-- Mathlib.Order.RelIso.Basic
#check RelEmbedding.to_rel_hom_eq_coe.{u_2, u_1} /- LHS equals RHS syntactically -/
#check RelEmbedding.coe_fn_to_embedding.{u_2, u_1} /- LHS equals RHS syntactically -/
#check RelIso.to_rel_embedding_eq_coe.{u_2, u_1} /- LHS equals RHS syntactically -/
#check RelIso.coe_coe_fn.{u_2, u_1} /- LHS equals RHS syntactically -/