refine' h₂ ⟨UVd.mono (erase_subset _ _) (erase_subset _ _), _, _, _, _⟩ (card_erase_lt_of_mem Hx)
case intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
case intro.intro.intro.intro.inr.refine'_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ (U.erase x).card = (V.erase (V.min' hV)).card

case intro.intro.intro.intro.inr.refine'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ (U.erase x).Nonempty

case intro.intro.intro.intro.inr.refine'_3
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ (V.erase (V.min' hV)).Nonempty

case intro.intro.intro.intro.inr.refine'_4
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n : ℕ
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : U.card = V.card
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < U.card
⊢ (U.erase x).max' ?intro.intro.intro.intro.inr.refine'_2 <
    (V.erase (V.min' hV)).max' ?intro.intro.intro.intro.inr.refine'_3