cases hBA.not_lt $ toColex_compress_lt_toColex hlt hAB
case inl
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : { ofColex := B } < { ofColex := compress (A \ B) (B \ A) B }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : compress (A \ B) (B \ A) B ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU
no goals