obtain rfl | hab := eq_or_ne a b
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∈ s
hb : b ∈ s
⊢ { ofColex := s.erase a } ≤ { ofColex := s.erase b } ↔ b ≤ a
case inl
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a : α
inst✝ : DecidableEq α
ha hb : a ∈ s
⊢ { ofColex := s.erase a } ≤ { ofColex := s.erase a } ↔ a ≤ a

case inr
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
⊢ { ofColex := s.erase a } ≤ { ofColex := s.erase b } ↔ b ≤ a