have hcard : card ℬ = card 𝒞 := t.symm.trans h₂
case h.e'_3.h.e'_2.h.e'_3
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
⊢ 𝒞 = ℬ
case h.e'_3.h.e'_2.h.e'_3
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
h₁ : Set.Sized r ↑𝒜
h₂ : 𝒜.card = 𝒞.card
h₃ : IsInitSeg 𝒞 r
ℬ : Finset (Finset (Fin n))
card_le : (∂ ℬ).card ≤ (∂ 𝒜).card
t : 𝒜.card = ℬ.card
hℬ : Set.Sized r ↑ℬ
fully_comp : ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
hcard : ℬ.card = 𝒞.card
⊢ 𝒞 = ℬ