-- Mathlib/Combinatorics/SetFamily/KruskalKatona.lean
/-- The main Kruskal-Katona helper: use induction with our measure to keep compressing until
we can't any more, which gives a set family which is fully compressed and has the nice properties we
want. -/
private lemma kruskal_katona_helper {r : ℕ} (𝒜 : Finset (Finset (Fin n)))
    (h : (𝒜 : Set (Finset (Fin n))).Sized r) :
    ∃ ℬ : Finset (Finset (Fin n)), #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧
      (ℬ : Set (Finset (Fin n))).Sized r ∧ ∀ U V, UsefulCompression U V → IsCompressed U V ℬ

Proof state:
case inr.intro.mk.intro
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) 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 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
⊢ ∃ ℬ,
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

Tactic:
have h₂ : ∀ U₁ V₁, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜 := by
  rintro U₁ V₁ huseful hUcard
  by_contra h
  exact hUcard.not_le <| t ⟨U₁, V₁⟩ <| mem_filter.2 ⟨mem_univ _, huseful, h⟩

Result:
case inr.intro.mk.intro
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) 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 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
⊢ ∃ ℬ,
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

Proof state:
case inr
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) univ
husable : usable.Nonempty
⊢ ∃ ℬ,
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

Tactic:
obtain ⟨⟨U, V⟩, hUV, t⟩ := exists_min_image usable (fun t ↦ #t.1) husable

Result:
case inr.intro.mk.intro
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) univ
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ usable
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
⊢ ∃ ℬ,
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

Proof state:
case inl
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h✝ : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) univ
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
h : ¬IsCompressed U V 𝒜
⊢ False

Tactic:
exact husable ⟨U, V⟩ <| mem_filter.2 ⟨mem_univ _, hUV, h⟩

Result:
no goals

Proof state:
case inr.intro.mk.intro
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) 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 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
⊢ ∃ ℬ,
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

Tactic:
have p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜) := compression_improved _ hUV.2.1 h₂

Result:
case inr.intro.mk.intro
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) 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 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
h₂ : ∀ (U₁ V₁ : Finset (Fin n)), Finset.UV.UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
⊢ ∃ ℬ,
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), Finset.UV.UsefulCompression U V → IsCompressed U V ℬ

Proof state:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) 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 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
U₁ V₁ : Finset (Fin n)
huseful : Finset.UV.UsefulCompression U₁ V₁
hUcard : #U₁ < #U
⊢ IsCompressed U₁ V₁ 𝒜

Tactic:
by_contra h

Result:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h✝ : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) 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 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
U₁ V₁ : Finset (Fin n)
huseful : Finset.UV.UsefulCompression U₁ V₁
hUcard : #U₁ < #U
h : ¬IsCompressed U₁ V₁ 𝒜
⊢ False

Proof state:
case inl
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) univ
husable : usable = ∅
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
⊢ IsCompressed U V 𝒜

Tactic:
rw [eq_empty_iff_forall_not_mem] at husable

Result:
case inl
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) univ
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
⊢ IsCompressed U V 𝒜

Proof state:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h✝ : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) 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 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
U₁ V₁ : Finset (Fin n)
huseful : Finset.UV.UsefulCompression U₁ V₁
hUcard : #U₁ < #U
h : ¬IsCompressed U₁ V₁ 𝒜
⊢ False

Tactic:
exact hUcard.not_le <| t ⟨U₁, V₁⟩ <| mem_filter.2 ⟨mem_univ _, huseful, h⟩

Result:
no goals

Proof state:
case inl
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) univ
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
⊢ IsCompressed U V 𝒜

Tactic:
by_contra h

Result:
case inl
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h✝ : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) :=
  filter (fun t => Finset.UV.UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜) univ
husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : Finset.UV.UsefulCompression U V
h : ¬IsCompressed U V 𝒜
⊢ False