max with IsCoatom equal top iff

Stream: Is there code for X?

[Xavier Roblot]

Do we have something like this:

import Mathlib

example {α : Type*} {a b : α} [SemilatticeSup α] [OrderTop α] (ha : IsCoatom a) :
    a ⊔ b = ⊤ ↔ ¬ b ≤ a := by
  by_cases hb : b = ⊤
  · simpa [hb] using ha.1
  · exact ⟨fun h ↦ left_lt_sup.mp (h ▸ IsCoatom.lt_top ha), fun h ↦ ha.2 _ (left_lt_sup.mpr h)⟩