awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
inr : #(U.erase x) = #V - 1
inr₁ : #U - 1 = #V - 1
inr₂ inr₃ : #V - 1 = #V - 1
⊢ #(U.erase x) = #(V.erase (V.min' hV))

Tactic:
rw [card_erase_of_mem (min'_mem _ _), card_erase_of_mem Hx, same_size]

Premises used: Finset.min'_mem, Finset.card_erase_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
inr : 0 < #(U.erase x)
inr₁ : 0 < #U - 1
inr₂ inr₃ inr₄ inr₅ : 1 < #U
⊢ (U.erase x).Nonempty

Tactic:
rwa [← card_pos, card_erase_of_mem Hx, tsub_pos_iff_lt]

Premises used: tsub_pos_iff_lt, Finset.card_erase_of_mem, Finset.card_pos
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
inr : 0 < #(V.erase (V.min' hV))
inr₁ : 0 < #V - 1
inr₂ : 0 < #U - 1
inr₃ inr₄ inr₅ inr₆ : 1 < #U
⊢ (V.erase (V.min' hV)).Nonempty

Tactic:
rwa [← Finset.card_pos, card_erase_of_mem (min'_mem _ _), ← same_size, tsub_pos_iff_lt]

Premises used: tsub_pos_iff_lt, Finset.min'_mem, Finset.card_erase_of_mem, Finset.card_pos
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
rwa rwa₁ rwa₂ rwa₃ : 1 < #U
⊢ 1 < #V

Tactic:
rwa [← same_size]
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ (U.erase x).max' ⋯ < (V.erase (V.min' hV)).max' ⋯

Tactic:
exact (Finset.max'_subset _ <| erase_subset _ _).trans_lt (max_lt.trans_le <| le_max' _ _ <|
      mem_erase.2 ⟨(min'_lt_max'_of_card _ (by rwa [← same_size])).ne', max'_mem _ _⟩)

Premises used: Iff.mpr, Finset.max'_mem, Finset.max'_subset, LT.lt.ne', Finset.mem_erase, Finset.min'_lt_max'_of_card, LT.lt.trans_le, Finset.le_max', And.intro, LE.le.trans_lt, Finset.erase_subset
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ℬ
⊢ IsInitSeg ℬ r

Tactic:
⟨h₁, ?_⟩

Premises used: And.intro, Finset.Colex.IsInitSeg
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ℬ
refine :
  ∀ ⦃s t : Finset α⦄,
    s ∈ ℬ →
      LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
            ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) ∧
          #t = r →
        t ∈ ℬ
⊢ IsInitSeg ℬ r

Tactic:
refine ⟨h₁, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
by_contra : ∀ (hB : B ∉ ℬ), False
⊢ B ∈ ℬ

Tactic:
by_contra hB
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ∉ ℬ
⊢ A ≠ B

Tactic:
have hAB : A ≠ B := ne_of_mem_of_not_mem hA hB
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
⊢ #A = #B

Tactic:
have hAB' : #A = #B := (h₁ hA).trans sizeA.symm
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
⊢ (A \ B).Nonempty

Tactic:
have hU : (A \ B).Nonempty := sdiff_nonempty.2 fun h ↦ hAB <| eq_of_subset_of_card_le h hAB'.ge
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
⊢ (B \ A).Nonempty

Tactic:
have hV : (B \ A).Nonempty :=
    sdiff_nonempty.2 fun h ↦ hAB.symm <| eq_of_subset_of_card_le h hAB'.le
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
⊢ Disjoint (B \ A) (A \ B)

Tactic:
have disj : Disjoint (B \ A) (A \ B) := disjoint_sdiff.mono_left sdiff_subset
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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)
inl : ∀ (hlt : (A \ B).max' hU < (B \ A).max' hV), (B \ A).max' hV < (A \ B).max' hU
inr : ∀ (heq : (A \ B).max' hU = (B \ A).max' hV), (B \ A).max' hV < (A \ B).max' hU
inr₁ : ∀ (hgt : (B \ A).max' hV < (A \ B).max' hU), (B \ A).max' hV < (A \ B).max' hU
⊢ (B \ A).max' hV < (A \ B).max' hU

Tactic:
obtain hlt | heq | hgt := lt_trichotomy (max' _ hU) (max' _ hV)

Premises used: Finset.max', lt_trichotomy
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
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
⊢ (B \ A).max' hV < (A \ B).max' hU

Tactic:
rw [← compress_sdiff_sdiff A B] at hAB hBA

Premises used: UV.compress_sdiff_sdiff
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 α)) (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:
cases hBA.not_gt <| toColex_compress_lt_toColex hlt hAB

Premises used: Finset.UV.toColex_compress_lt_toColex, LT.lt.not_gt
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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)
heq : (A \ B).max' hU = (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

Tactic:
(disjoint_right.1 disj (max'_mem _ hU) <| heq.symm ▸ max'_mem _ _).elim

Premises used: Finset.max'_mem, False.elim, Eq.rec, Iff.mp, Finset.disjoint_right, Eq.symm
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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)
heq : (A \ B).max' hU = (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

Tactic:
exact (disjoint_right.1 disj (max'_mem _ hU) <| heq.symm ▸ max'_mem _ _).elim

Premises used: Finset.max'_mem, False.elim, Eq.rec, Iff.mp, Finset.disjoint_right, Eq.symm
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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)
hgt : (B \ A).max' hV < (A \ B).max' hU
⊢ (B \ A).max' hV < (A \ B).max' hU

Tactic:
assumption
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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)
⊢ (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
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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

Tactic:
hB ?_
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
refine : B ∈ ℬ
⊢ False

Tactic:
refine hB ?_
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
rw : B ∈ 𝓒 (B \ A) (A \ B) ℬ
⊢ B ∈ ℬ

Tactic:
rw [← (h₂ _ _ ⟨disj, card_sdiff_comm hAB'.symm, hV, hU, smaller⟩).eq]

Premises used: UV.IsCompressed.eq, And.intro, Exists.intro, Finset.card_sdiff_comm, Eq.symm
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ∈ 𝓒 (B \ A) (A \ B) ℬ

Tactic:
mem_compression.2 (Or.inr ⟨hB, A, hA, compress_sdiff_sdiff _ _⟩)

Premises used: Iff.mpr, UV.compress_sdiff_sdiff, And.intro, Exists.intro, UV.mem_compression, Or.inr
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 ∈ 𝓒 (B \ A) (A \ B) ℬ

Tactic:
exact mem_compression.2 (Or.inr ⟨hB, A, hA, compress_sdiff_sdiff _ _⟩)

Premises used: Iff.mpr, UV.compress_sdiff_sdiff, And.intro, Exists.intro, UV.mem_compression, Or.inr
-- 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 : 𝓒 U V 𝒜 ≠ 𝒜
⊢ {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜

Tactic:
rw [compression] at a ⊢

Premises used: UV.compression
-- 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 ∈ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, compress U V Q ≠ Q

Tactic:
grind
-- 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 ∈ {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
-- 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
⊢ {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 _ _
-- 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 ∉ 𝒜} = 𝒜
contrapose! :
  ∀ (a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅), {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} = 𝒜
⊢ {A ∈ 𝒜 | compress U V A ∉ 𝒜}.Nonempty

Tactic:
contrapose! a
-- 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))
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 ∉ 𝒜} = ∅
rw : {a ∈ 𝒜 | compress U V a ∈ 𝒜} = 𝒜
⊢ {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} = 𝒜

Tactic:
rw [filter_image, a, image_empty, union_empty]

Premises used: Finset.image_empty, Finset.union_empty, Finset.filter_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))
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 ∈ 𝒜} = 𝒜
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (uA : {A ∈ 𝒜 | compress U V A ∈ 𝒜} = 𝒜) (a : {A ∈ 𝒜 | compress U V A ∉ 𝒜} = ∅), {a ∈ 𝒜 | compress U V a ∈ 𝒜} = 𝒜
⊢ {a ∈ 𝒜 | compress U V a ∈ 𝒜} = 𝒜

Tactic:
rwa [a, union_empty] at uA

Premises used: Finset.union_empty
-- 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 ∉ 𝒜} = 𝒜
⊢ {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
-- 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 :
  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 : ℕ)
⊢ familyMeasure ({a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜}) < familyMeasure 𝒜

Tactic:
rw [familyMeasure, familyMeasure, sum_union compress_disjoint]

Premises used: Finset.sum_union, UV.compress_disjoint, _private.0.Finset.UV.familyMeasure
-- 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 : ∑ A ∈ {A ∈ 𝒜 | compress U V A ∈ 𝒜} ∪ {A ∈ 𝒜 | compress U V A ∉ 𝒜}, ∑ a ∈ A, HPow.hPow (α := ℕ) 2 (↑a : ℕ)
| ∑ A ∈ 𝒜, ∑ a ∈ A, HPow.hPow (α := ℕ) 2 (↑a : ℕ)

Tactic:
rw [← uA]
-- 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
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 : ℕ)
⊢ 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:
conv_rhs => rw [← uA]