OrderTop.ext_top

Stream: mathlib4

[Ruben Van de Velde]

In mathlib4#697, I have

theorem OrderTop.ext_top {α} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α}
    (B : OrderTop α) (H : ∀ x y : α, (haveI := hA; x ≤ y) ↔ x ≤ y) :
    (haveI := A; ⊤ : α) = ⊤ := by

which triggers the linter:

/- 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. -/
#check @OrderTop.ext_top /- LHS equals RHS syntactically -/

/- The `unusedArguments` linter reports:
UNUSED ARGUMENTS. -/
#check @OrderTop.ext_top /- argument 3 A : OrderTop α -/

Thoughts on how to deal with this are most welcome.

(Looking into it, I noticed this theorem was only used to prove order_top.ext in mathlib3, and I didn't need it in mathlib4, so the easiest solution may be to just drop it.)

[Floris van Doorn]

Given that it is a syntactic tautology, it seems safe to remove it.

[Ruben Van de Velde]

Well, that's the thing - is it actually meant to say something substantial, and did it get translated into something trivial accidentally?

[Yaël Dillies]

I suspect it got translated to something trivial accidentally

[Scott Morrison]

In the statement, instead of using haveI, write something starting with @ and use the intended instance.