-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
Are Are₁ :
  ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
inl :
  let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
  ∀ (husable : usable = ∅),
    ∃ (ℬ : Finset (Finset (Fin n))),
      #(∂ ℬ) ≤ #(∂ 𝒜) ∧
        #𝒜 = #ℬ ∧
          Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
inr inr₁ :
  let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
  ∀ (husable : usable.Nonempty),
    ∃ (ℬ : Finset (Finset (Fin n))),
      #(∂ ℬ) ≤ #(∂ 𝒜) ∧
        #𝒜 = #ℬ ∧
          Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
inr₂ :
  let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
  ∀ (husable : usable.Nonempty) (U V : Finset (Fin n)) (hUV : (U, V) ∈ usable) (t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1),
    ∃ (ℬ : Finset (Finset (Fin n))),
      #(∂ ℬ) ≤ #(∂ 𝒜) ∧
        #𝒜 = #ℬ ∧
          Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
inr₃ :
  let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
  ∀ (husable : usable.Nonempty) (U V : Finset (Fin n))
    (hUV :
      Membership.mem (γ := Finset (Finset (Fin n) × Finset (Fin n))) univ (U, V) ∧
        UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜)
    (t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1),
    ∃ (ℬ : Finset (Finset (Fin n))),
      #(∂ ℬ) ≤ #(∂ 𝒜) ∧
        #𝒜 = #ℬ ∧
          Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
inr₄ :
  let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
  ∀ (husable : usable.Nonempty) (U V : Finset (Fin n))
    (hUV :
      Membership.mem (γ := Finset (Finset (Fin n) × Finset (Fin n))) univ (U, V) ∧
        UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜)
    (t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1)
    (h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜),
    ∃ (ℬ : Finset (Finset (Fin n))),
      #(∂ ℬ) ≤ #(∂ 𝒜) ∧
        #𝒜 = #ℬ ∧
          Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
inr₅ :
  let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
  ∀ (husable : usable.Nonempty) (U V : Finset (Fin n))
    (hUV :
      Membership.mem (γ := Finset (Finset (Fin n) × Finset (Fin n))) univ (U, V) ∧
        UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜)
    (t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1)
    (h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜)
    (p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)),
    ∃ (ℬ : Finset (Finset (Fin n))),
      #(∂ ℬ) ≤ #(∂ 𝒜) ∧
        #𝒜 = #ℬ ∧
          Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
inr₆ :
  let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
  ∀ (husable : usable.Nonempty) (U V : Finset (Fin n))
    (hUV :
      Membership.mem (γ := Finset (Finset (Fin n) × Finset (Fin n))) univ (U, V) ∧
        UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜)
    (t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1)
    (h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜)
    (p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)) (hUV' : #(U, V).1 = #(U, V).2) (hu : (U, V).1.Nonempty) (hv : (U, V).2.Nonempty)
    (hmax : (U, V).1.max' hu < (U, V).2.max' hv),
    ∃ (ℬ : Finset (Finset (Fin n))),
      #(∂ ℬ) ≤ #(∂ 𝒜) ∧
        #𝒜 = #ℬ ∧
          Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
inr₇ :
  let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
  ∀ (husable : usable.Nonempty) (U V : Finset (Fin n))
    (hUV :
      Membership.mem (γ := Finset (Finset (Fin n) × Finset (Fin n))) univ (U, V) ∧
        UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜)
    (t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1)
    (h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜)
    (p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)) (hUV' : #(U, V).1 = #(U, V).2) (hu : (U, V).1.Nonempty) (hv : (U, V).2.Nonempty)
    (hmax : (U, V).1.max' hu < (U, V).2.max' hv) (this : familyMeasure (𝓒 (U, V).1 (U, V).2 𝒜) < familyMeasure 𝒜),
    ∃ (ℬ : Finset (Finset (Fin n))),
      #(∂ ℬ) ≤ #(∂ 𝒜) ∧
        #𝒜 = #ℬ ∧
          Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
inr₈ :
  let usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t : Finset (Fin n) × Finset (Fin n) | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜};
  ∀ (husable : usable.Nonempty) (U V : Finset (Fin n))
    (hUV :
      Membership.mem (γ := Finset (Finset (Fin n) × Finset (Fin n))) univ (U, V) ∧
        UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜)
    (t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1)
    (h₂ : ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜)
    (p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)) (hUV' : #(U, V).1 = #(U, V).2) (hu : (U, V).1.Nonempty) (hv : (U, V).2.Nonempty)
    (hmax : (U, V).1.max' hu < (U, V).2.max' hv) (this : familyMeasure (𝓒 (U, V).1 (U, V).2 𝒜) < familyMeasure 𝒜)
    (t : Finset (Finset (Fin n))) (q1 : #(∂ t) ≤ #(∂ (𝓒 U V 𝒜))) (q2 : #(𝓒 U V 𝒜) = #t)
    (q3 : Set.Sized r (↑t : Set (Finset (Fin n))))
    (q4 : ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V t),
    ∃ (ℬ : Finset (Finset (Fin n))),
      #(∂ ℬ) ≤ #(∂ 𝒜) ∧
        #𝒜 = #ℬ ∧
          Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

Tactic:
classical
  -- Are there any compressions we can make now?
  set usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
    {t | UsefulCompression t.1 t.2 ∧ ¬ IsCompressed t.1 t.2 𝒜}
  obtain husable | husable := usable.eq_empty_or_nonempty
  -- No. Then where we are is the required set family.
  · refine ⟨𝒜, le_rfl, rfl, h, fun U V hUV ↦ ?_⟩
    rw [eq_empty_iff_forall_notMem] at husable
    by_contra h
    exact husable ⟨U, V⟩ <| mem_filter.2 ⟨mem_univ _, hUV, h⟩
  -- Yes. Then apply the smallest compression, then keep going
  obtain ⟨⟨U, V⟩, hUV, t⟩ := exists_min_image usable (fun t ↦ #t.1) husable
  rw [mem_filter] at hUV
  have h₂ : ∀ U₁ V₁, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜 := by
    rintro U₁ V₁ huseful hUcard
    by_contra h
    exact hUcard.not_ge <| t ⟨U₁, V₁⟩ <| mem_filter.2 ⟨mem_univ _, huseful, h⟩
  have p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜) := compression_improved _ hUV.2.1 h₂
  obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1
  have := familyMeasure_compression_lt_familyMeasure hmax hUV.2.2
  obtain ⟨t, q1, q2, q3, q4⟩ := UV.kruskal_katona_helper (𝓒 U V 𝒜) (h.uvCompression hUV')
  exact ⟨t, q1.trans p1, (card_compression _ _ _).symm.trans q2, q3, q4⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset, Finset.eq_empty_iff_forall_notMem, And.intro, Finset.mem_filter, Prod, Fin