rw [← hU'] at same_size
case intro.intro.intro.intro.inl
α : 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.inl
α : 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 : succ 0 = 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)) 𝒜