revert h
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ 𝒜).card ∧
      𝒜.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 : Finset (Finset (Fin n))
⊢ Set.Sized r ↑𝒜 →
    ∃ ℬ,
      (∂ ℬ).card ≤ (∂ 𝒜).card ∧
        𝒜.card = ℬ.card ∧
          Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ