have p1 : (∂ (𝓒 U V A)).card ≤ (∂ A).card := compression_improved _ hUV.2.1 h₂
case inr.intro.mk.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
case inr.intro.mk.intro
α : Type u_1
inst✝ : LinearOrder α
s U✝ V✝ : Finset α
n r : ℕ
𝒜 A : Finset (Finset (Fin n))
ih :
  ∀ (y : Finset (Finset (Fin n))),
    InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y A →
      Set.Sized r ↑y →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ y).card ∧
            y.card = ℬ.card ∧
              Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ
h : Set.Sized r ↑A
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 A) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ Finset.UV.UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 A
t : ∀ x' ∈ usable, (U, V).1.card ≤ x'.1.card
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → U₁.card < U.card → IsCompressed U₁ V₁ A
p1 : (∂ (𝓒 U V A)).card ≤ (∂ A).card
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ