Diamond in `UpperSet`

Stream: mathlib4

[Aaron Liu]

docs#SetLike.instPartialOrder has the potential to cause problems in docs#UpperSet, whose order is reversed (to be like filters)

import Mathlib

universe u
variable {α : Type u} [LE α]

theorem oops {s t : UpperSet α} : SetLike.instPartialOrder.le s t ↔ t ≤ s :=
  SetLike.coe_subset_coe.symm.trans UpperSet.coe_subset_coe

/-- info: oops.{u} {α : Type u} [LE α] {s t : UpperSet α} : s ≤ t ↔ t ≤ s -/
#guard_msgs in
#check oops

[Yaël Dillies]

Yes, we are aware of that. I've been thinking on and off about moving the problematic instance to an OrderedSetLike, which UpperSet wouldn't have an instance of