rw [compress, ite_ne_right_iff] at hA
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : compress U V s ≠ s
⊢ { ofColex := compress U V s } < { ofColex := s }
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
⊢ { ofColex := compress U V s } < { ofColex := s }