intro A ih h
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r : ℕ
𝒜 : Finset (Finset (Fin n))
⊢ ∀ (x : Finset (Finset (Fin n))),
    (∀ (y : Finset (Finset (Fin n))),
        InvImage (fun x x_1 => x < x_1) Finset.UV.familyMeasure y x →
          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 ℬ) →
      Set.Sized r ↑x →
        ∃ ℬ,
          (∂ ℬ).card ≤ (∂ x).card ∧
            x.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 : ℕ
𝒜 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
⊢ ∃ ℬ,
    (∂ ℬ).card ≤ (∂ A).card ∧
      A.card = ℬ.card ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ