awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r (↑ℬ : Set (Finset α))
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) B : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) A : Colex (Finset α))
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU
have inl : ∀
  (hBA :
    LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) B : Colex (Finset α))
      ((toColex : (a : Finset α) → Colex (Finset α)) (compress (A \ B) (B \ A) B) : Colex (Finset α)))
  (sizeA : #B = r) (hB : B ∉ ℬ) (hAB : compress (A \ B) (B \ A) B ≠ B) (hAB' : #A = #B) (hU : (A \ B).Nonempty)
  (hV : (B \ A).Nonempty) (disj : Disjoint (B \ A) (A \ B)) (hlt : (A \ B).max' hU < (B \ A).max' hV),
  (B \ A).max' hV < (A \ B).max' hU
Tactic: rw [← compress_sdiff_sdiff A B] at hAB hBA
Cleared hypotheses: hBA, sizeA, hB, hAB, hAB', hU, hV, disj, hlt
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r (↑ℬ : Set (Finset α))
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) B : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) A : Colex (Finset α))
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
⊢ False
have smaller : (B \ A).max' hV < (A \ B).max' hU
Tactic: have smaller : max' _ hV < max' _ hU := by
    obtain hlt | heq | hgt := lt_trichotomy (max' _ hU) (max' _ hV)
    · rw [← compress_sdiff_sdiff A B] at hAB hBA
      cases hBA.not_gt <| toColex_compress_lt_toColex hlt hAB
    · exact (disjoint_right.1 disj (max'_mem _ hU) <| heq.symm ▸ max'_mem _ _).elim
    · assumption
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r (↑ℬ : Set (Finset α))
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) B : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) A : Colex (Finset α))
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
smaller : (B \ A).max' hV < (A \ B).max' hU
⊢ False
have refine : B ∈ ℬ
Tactic: refine hB ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r (↑ℬ : Set (Finset α))
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA :
  LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) B : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) A : Colex (Finset α))
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
smaller : (B \ A).max' hV < (A \ B).max' hU
⊢ B ∈ ℬ
have rw : B ∈ 𝓒 (B \ A) (A \ B) ℬ
Tactic: rw [← (h₂ _ _ ⟨disj, card_sdiff_comm hAB'.symm, hV, hU, smaller⟩).eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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 : 𝓒 U V 𝒜 ≠ 𝒜
⊢ familyMeasure (𝓒 U V 𝒜) < familyMeasure 𝒜
have a₁ : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
Tactic: rw [compression] at a ⊢
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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 ∉ 𝒜} ≠ 𝒜
⊢ familyMeasure ({a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜}) < familyMeasure 𝒜
have q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
Tactic: have q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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
⊢ familyMeasure ({a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜}) < familyMeasure 𝒜
have uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
Tactic: have uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜 :=
    filter_union_filter_not_eq _ _
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 ∉ 𝒜} = 𝒜
⊢ {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
have contrapose! : ∀ (a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅), {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} = 𝒜
Tactic: contrapose! a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅
⊢ {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} = 𝒜
have rw : {a ∈ 𝒜 | compress U V a ∈ 𝒜} = 𝒜
Tactic: rw [filter_image, a, image_empty, union_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅
⊢ {a ∈ 𝒜 | compress U V a ∈ 𝒜} = 𝒜
have rwa : ∀ (uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ ∅ = 𝒜) (a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅), {a ∈ 𝒜 | compress U V a ∈ 𝒜} = 𝒜
Tactic: rwa [a, union_empty] at uA
Cleared hypotheses: uA, a
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
q : ∀ Q ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q
uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜} = 𝒜
a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅
rwa :
  ∀ (uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ ∅ = 𝒜) (a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅), {a ∈ 𝒜 | compress U V a ∈ 𝒜} = 𝒜
⊢ {a ∈ 𝒜 | compress U V a ∈ 𝒜} = 𝒜
have rwa₁ : ∀ (uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} = 𝒜) (a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅), {a ∈ 𝒜 | compress U V a ∈ 𝒜} = 𝒜
Tactic: rwa [a, union_empty] at uA
Cleared hypotheses: uA, a
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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 ∉ 𝒜} = 𝒜
⊢ familyMeasure ({a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜}) < familyMeasure 𝒜
have ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty
Tactic: have ne₂ : {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty := by
    contrapose! a
    rw [filter_image, a, image_empty, union_empty]
    rwa [a, union_empty] at uA
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ familyMeasure ({a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜}) < familyMeasure 𝒜
have rw : 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 ∈ A, HPow.hPow (α := ℕ) 2 (↑a : ℕ)
Tactic: rw [familyMeasure, familyMeasure, sum_union compress_disjoint]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 ∈ 𝒜, ∑ a ∈ A, HPow.hPow (α := ℕ) 2 (↑a : ℕ)
have rw : ∑ A ∈ {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, ∑ a ∈ A, HPow.hPow (α := ℕ) 2 (↑a : ℕ)
Tactic: rw [← uA]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ 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 ∈ A, HPow.hPow (α := ℕ) 2 (↑a : ℕ)
have conv_rhs : 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: conv_rhs => rw [← uA]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ 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 : ℕ)
have 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 : ℕ))
Tactic: rw [sum_union (disjoint_filter_filter_not _ _ _), add_lt_add_iff_left, filter_image,
    sum_image compress_injOn]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 : ℕ))
have 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 : ℕ))
Tactic: refine sum_lt_sum_of_nonempty ne₂ fun A hA ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 (α := ℕ) (∑ a ∈ compress U V A, HPow.hPow (α := ℕ) 2 (↑a : ℕ)) (∑ a ∈ A, HPow.hPow (α := ℕ) 2 (↑a : ℕ))
have 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)
Tactic: simp_rw [← sum_image Fin.val_injective.injOn]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 (α := ℕ) (∑ x ∈ image Fin.val (compress U V A), HPow.hPow (α := ℕ) 2 x)
    (∑ x ∈ image Fin.val A, HPow.hPow (α := ℕ) 2 x)
have 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)))
Tactic: rw [geomSum_lt_geomSum_iff_toColex_lt_toColex le_rfl,
    toColex_image_lt_toColex_image Fin.val_strictMono]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 𝒜}
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have 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 ℬ
Tactic: obtain husable | husable := usable.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 ℬ
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have 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 ℬ
Tactic: obtain husable | husable := usable.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 ℬ
have inl : ∀ (U V : Finset (Fin n)) (hUV : UsefulCompression U V), IsCompressed U V 𝒜
Tactic: refine ⟨𝒜, le_rfl, rfl, h, fun U V hUV ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ IsCompressed U V 𝒜
have inl : ∀ (husable : ∀ (x : Finset (Fin n) × Finset (Fin n)), x ∉ usable) (U V : Finset (Fin n)) (hUV : UsefulCompression U V),
  IsCompressed U V 𝒜
Tactic: rw [eq_empty_iff_forall_notMem] at husable
Cleared hypotheses: husable, U, V, hUV
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ IsCompressed U V 𝒜
have inl : ∀ (h : ¬IsCompressed U V 𝒜), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have 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 ℬ
Tactic: obtain ⟨⟨U, V⟩, hUV, t⟩ := exists_min_image usable (fun t ↦ #t.1) husable
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have 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 𝒜
Tactic: rw [mem_filter] at hUV
Cleared hypotheses: hUV, t
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ IsCompressed U₁ V₁ 𝒜
have by_contra : ∀ (h : ¬IsCompressed U₁ V₁ 𝒜), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have h₂ : ∀ (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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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₁ 𝒜
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
Tactic: have p1 : #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜) := compression_improved _ hUV.2.1 h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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 𝒜)) ≤ #(∂ 𝒜)
⊢ ∃ (ℬ : Finset (Finset (Fin n))),
    #(∂ ℬ) ≤ #(∂ 𝒜) ∧
      #𝒜 = #ℬ ∧
        Set.Sized r (↑ℬ : Set (Finset (Fin n))) ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
have hUV' : #(U, V).1 = #(U, V).2
Tactic: obtain ⟨-, hUV', hu, hv, hmax⟩ := hUV.2.1