obtain hlt | heq | hgt := lt_trichotomy (max' _ hU) (max' _ hV)
α : 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 := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
⊢ (B \ A).max' hV < (A \ B).max' hU
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 := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ 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

case inr.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 := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
heq : (A \ B).max' hU = (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

case inr.inr
α : 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 := A }
sizeA : B.card = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : A.card = B.card
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hgt : (B \ A).max' hV < (A \ B).max' hU
⊢ (B \ A).max' hV < (A \ B).max' hU