awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
rw :
  LT.lt (α := ℕ) (∑ x ∈ 𝒜 with compress U V x ∉ 𝒜, ∑ a ∈ compress U V x, HPow.hPow (α := ℕ) 2 (↑a : ℕ))
    (∑ x ∈ 𝒜 with compress U V x ∉ 𝒜, ∑ a ∈ x, HPow.hPow (α := ℕ) 2 (↑a : ℕ))
⊢ HAdd.hAdd (α := ℕ) (∑ x ∈ 𝒜 with compress U V x ∈ 𝒜, ∑ a ∈ x, HPow.hPow (α := ℕ) 2 (↑a : ℕ))
      (∑ x ∈ image (compress U V) 𝒜 with x ∉ 𝒜, ∑ a ∈ x, HPow.hPow (α := ℕ) 2 (↑a : ℕ)) <
    ∑ A ∈ {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, ∑ a ∈ A, HPow.hPow (α := ℕ) 2 (↑a : ℕ)

Tactic:
rw [sum_union (disjoint_filter_filter_not _ _ _), add_lt_add_iff_left, filter_image,
    sum_image compress_injOn]

Premises used: UV.compress_injOn, Finset.sum_union, Finset.disjoint_filter_filter_not, Finset.sum_image, Finset.filter_image, add_lt_add_iff_left
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
⊢ LT.lt (α := ℕ) (∑ x ∈ 𝒜 with compress U V x ∉ 𝒜, ∑ a ∈ compress U V x, HPow.hPow (α := ℕ) 2 (↑a : ℕ))
    (∑ x ∈ 𝒜 with compress U V x ∉ 𝒜, ∑ a ∈ x, HPow.hPow (α := ℕ) 2 (↑a : ℕ))

Tactic:
sum_lt_sum_of_nonempty ne₂ fun A hA ↦ ?_

Premises used: Finset.sum_lt_sum_of_nonempty
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
refine :
  ∀ (A : Finset (Fin n)) (hA : A ∈ {a ∈ 𝒜 | compress U V a ∉ 𝒜}),
    LT.lt (α := ℕ) (∑ a ∈ compress U V A, HPow.hPow (α := ℕ) 2 (↑a : ℕ)) (∑ a ∈ A, HPow.hPow (α := ℕ) 2 (↑a : ℕ))
⊢ LT.lt (α := ℕ) (∑ x ∈ 𝒜 with compress U V x ∉ 𝒜, ∑ a ∈ compress U V x, HPow.hPow (α := ℕ) 2 (↑a : ℕ))
    (∑ x ∈ 𝒜 with compress U V x ∉ 𝒜, ∑ a ∈ x, HPow.hPow (α := ℕ) 2 (↑a : ℕ))

Tactic:
refine sum_lt_sum_of_nonempty ne₂ fun A hA ↦ ?_

Premises used: Finset.sum_lt_sum_of_nonempty
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
A : Finset (Fin n)
hA : A ∈ {a ∈ 𝒜 | compress U V a ∉ 𝒜}
simp_rw :
  LT.lt (α := ℕ) (∑ x ∈ image Fin.val (compress U V A), HPow.hPow (α := ℕ) 2 x)
    (∑ x ∈ image Fin.val A, HPow.hPow (α := ℕ) 2 x)
⊢ LT.lt (α := ℕ) (∑ a ∈ compress U V A, HPow.hPow (α := ℕ) 2 (↑a : ℕ)) (∑ a ∈ A, HPow.hPow (α := ℕ) 2 (↑a : ℕ))

Tactic:
simp_rw [← sum_image Fin.val_injective.injOn]

Premises used: Function.Injective.injOn, Fin.val_injective, Finset.sum_image
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
A : Finset (Fin n)
hA : A ∈ {a ∈ 𝒜 | compress U V a ∉ 𝒜}
rw :
  LT.lt (α := Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) (compress U V A) : Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) A : Colex (Finset (Fin n)))
⊢ LT.lt (α := ℕ) (∑ x ∈ image Fin.val (compress U V A), HPow.hPow (α := ℕ) 2 x)
    (∑ x ∈ image Fin.val A, HPow.hPow (α := ℕ) 2 x)

Tactic:
rw [geomSum_lt_geomSum_iff_toColex_lt_toColex le_rfl,
    toColex_image_lt_toColex_image Fin.val_strictMono]

Premises used: Finset.geomSum_lt_geomSum_iff_toColex_lt_toColex, le_rfl, Finset.Colex.toColex_image_lt_toColex_image, Fin.val_strictMono
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
A : Finset (Fin n)
hA : A ∈ {a ∈ 𝒜 | compress U V a ∉ 𝒜}
⊢ LT.lt (α := Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) (compress U V A) : Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) A : Colex (Finset (Fin n)))

Tactic:
toColex_compress_lt_toColex h <| q _ hA

Premises used: Set.Mem, setOf, Finset.UV.toColex_compress_lt_toColex
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
A : Finset (Fin n)
hA : A ∈ {a ∈ 𝒜 | compress U V a ∉ 𝒜}
⊢ LT.lt (α := Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) (compress U V A) : Colex (Finset (Fin n)))
    ((toColex : (a : Finset (Fin n)) → Colex (Finset (Fin n))) A : Colex (Finset (Fin n)))

Tactic:
exact toColex_compress_lt_toColex h <| q _ hA

Premises used: Finset.UV.toColex_compress_lt_toColex
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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 𝒜}
inl :
  ∀ (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 :
  ∀ (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 ℬ
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

Tactic:
obtain husable | husable := usable.eq_empty_or_nonempty

Premises used: Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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 ℬ

Tactic:
⟨𝒜, le_rfl, rfl, h, fun U V hUV ↦ ?_⟩

Premises used: le_rfl, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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 = ∅
inl : ∀ (U V : Finset (Fin n)) (hUV : 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:
refine ⟨𝒜, le_rfl, rfl, h, fun U V hUV ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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 = ∅
U V : Finset (Fin n)
hUV : UsefulCompression U V
inl :
  ∀ (husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable) (U V : Finset (Fin n))
    (hUV : UsefulCompression U V), IsCompressed U V 𝒜
⊢ IsCompressed U V 𝒜

Tactic:
rw [eq_empty_iff_forall_notMem] at husable

Premises used: Finset.eq_empty_iff_forall_notMem
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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 : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : UsefulCompression U V
inl : ∀ (h : ¬IsCompressed U V 𝒜), False
⊢ IsCompressed U V 𝒜

Tactic:
by_contra h
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h_1 : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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 : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : UsefulCompression U V
h : ¬IsCompressed U V 𝒜
⊢ False

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

Premises used: Iff.mpr, Finset.mem_univ, Prod.mk, And.intro, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h_1 : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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 : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable
U V : Finset (Fin n)
hUV : UsefulCompression U V
h : ¬IsCompressed U V 𝒜
⊢ False

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

Premises used: Iff.mpr, Finset.mem_univ, Prod.mk, And.intro, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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
inr :
  ∀ (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 ℬ
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

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

Premises used: Prod.fst, Finset.exists_min_image, Finset.card
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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
⊢ 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 𝒜

Tactic:
rw [mem_filter] at hUV

Premises used: Finset.mem_filter
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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
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 𝒜
⊢ ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1

Tactic:
rw [mem_filter] at hUV

Premises used: Finset.mem_filter
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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
U₁ V₁ : Finset (Fin n)
huseful : UsefulCompression U₁ V₁
hUcard : #U₁ < #U
by_contra : ∀ (h : ¬IsCompressed U₁ V₁ 𝒜), False
⊢ IsCompressed U₁ V₁ 𝒜

Tactic:
by_contra h
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h_1 : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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
U₁ V₁ : Finset (Fin n)
huseful : UsefulCompression U₁ V₁
hUcard : #U₁ < #U
h : ¬IsCompressed U₁ V₁ 𝒜
⊢ False

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

Premises used: Iff.mpr, Finset.mem_univ, Prod.mk, And.intro, Finset.mem_filter, LT.lt.not_ge
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h_1 : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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
U₁ V₁ : Finset (Fin n)
huseful : UsefulCompression U₁ V₁
hUcard : #U₁ < #U
h : ¬IsCompressed U₁ V₁ 𝒜
⊢ False

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

Premises used: Iff.mpr, Finset.mem_univ, Prod.mk, And.intro, Finset.mem_filter, LT.lt.not_ge
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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
⊢ ∀ (U₁ V₁ : Finset (Fin n)), UsefulCompression U₁ V₁ → #U₁ < #U → 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_ge <| t ⟨U₁, V₁⟩ <| mem_filter.2 ⟨mem_univ _, huseful, h⟩
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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₁ 𝒜
⊢ #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)

Tactic:
have p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜) := compression_improved _ hUV.2.1 h₂
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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 𝒜)) ≤ #(∂ 𝒜)
⊢ #(U, V).1 = #(U, V).2

Tactic:
obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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
⊢ (U, V).1.Nonempty

Tactic:
obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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
⊢ (U, V).2.Nonempty

Tactic:
obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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
⊢ (U, V).1.max' hu < (U, V).2.max' hv

Tactic:
obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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
⊢ familyMeasure (𝓒 (U, V).1 (U, V).2 𝒜) < familyMeasure 𝒜

Tactic:
have := familyMeasure_compression_lt_familyMeasure hmax hUV.2.2
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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 𝒜
inr :
  ∀ (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:
obtain ⟨t, q1, q2, q3, q4⟩ := UV.kruskal_katona_helper (𝓒 U V 𝒜) (h.uvCompression hUV')

Premises used: UV.compression, Set.Sized.uvCompression
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r (↑𝒜 : Set (Finset (Fin n)))
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_1 : ∀ 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 ℬ

Tactic:
⟨t, q1.trans p1, (card_compression _ _ _).symm.trans q2, q3, q4⟩

Premises used: And.intro, Exists.intro, LE.le.trans, Eq.symm, UV.card_compression, Eq.trans