awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
h : ∀ (lt : k < a), a ∈ insert j t
h₁ : ∀ (ha : k ∈ s), k ∈ insert j t
h₂ : ∀ (gt : a < k), a ∈ insert j t
⊢ a ∈ insert j t

Tactic:
rcases lt_trichotomy k a with (lt | rfl | gt)

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
h : a ∈ t
⊢ a ∈ insert j t

Tactic:
apply mem_insert_of_mem

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
h : a ∈ s.erase (s.min' hs)
⊢ a ∈ t

Tactic:
rw [z lt]
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ a ∈ s.erase (s.min' hs)

Tactic:
mem_erase_of_ne_of_mem (lt_of_le_of_lt ?_ lt).ne' ha

Premises used: lt_of_le_of_lt, Finset.mem_erase_of_ne_of_mem, LT.lt.ne'
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
h : s.min' hs ≤ k
⊢ a ∈ s.erase (s.min' hs)

Tactic:
refine mem_erase_of_ne_of_mem (lt_of_le_of_lt ?_ lt).ne' ha

Premises used: lt_of_le_of_lt, Finset.mem_erase_of_ne_of_mem, LT.lt.ne'
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
lt : k < a
⊢ s.min' hs ≤ k

Tactic:
apply min'_le _ _ (mem_of_mem_erase ‹_›)

Premises used: Finset.min'_le, Finset.mem_of_mem_erase
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
ha : k ∈ s
h : k ∈ insert k t
⊢ k ∈ insert j t

Tactic:
rw [r₁]
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
ha : k ∈ s
⊢ k ∈ insert k t

Tactic:
apply mem_insert_self

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < k
h : a ∈ t
⊢ a ∈ insert j t

Tactic:
apply mem_insert_of_mem

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < k
⊢ a < j

Tactic:
rw [← r₁] at gt
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
h : ∀ (this : a ∉ t), False
⊢ a ∈ t

Tactic:
by_contra
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this_1 : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
this : a ∉ t
apply : a ∈ tᶜ
⊢ False

Tactic:
apply (min'_le tᶜ _ _).not_gt gt

Premises used: Finset.min'_le, Compl.compl, LE.le.not_gt
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
cards' : #(s.erase (s.min' hs)) = #t
k : α
hks : k ∈ s.erase (s.min' hs)
hkt : k ∉ t
z : ∀ ⦃a : α⦄, k < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))
j : α := tᶜ.min' ⋯
hjk : j ≤ k
this_1 : j ∉ t
hcard : #s = #(insert j t)
r₁ : j = k
a : α
ha : a ∈ s
gt : a < j
this rwa rwa₁ rwa₂ rwa₃ : a ∉ t
⊢ a ∈ tᶜ

Tactic:
rwa [mem_compl]

Premises used: Finset.mem_compl
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Finite α
h₁ : IsInitSeg 𝒜 r
intro : ∀ (val : Fintype α), IsInitSeg (∂ 𝒜) (r - 1)
⊢ IsInitSeg (∂ 𝒜) (r - 1)

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Finite α
h₁ : IsInitSeg 𝒜 r
val : Fintype α
intro : ∀ (h₁ : IsInitSeg 𝒜 0), IsInitSeg (∂ 𝒜) (HSub.hSub (α := ℕ) 0 1)
intro₁ : ∀ (hr : r > 0), IsInitSeg (∂ 𝒜) (r - 1)
⊢ IsInitSeg (∂ 𝒜) (r - 1)

Tactic:
obtain rfl | hr := Nat.eq_zero_or_pos r

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
inst_1 : Finite α
val : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
rw : #s = 0
⊢ Membership.mem (γ := Finset (Finset α)) {∅} s

Tactic:
rw [mem_singleton, ← Finset.card_eq_zero]

Premises used: Finset.mem_singleton, Finset.card_eq_zero
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
inst_1 : Finite α
val : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ #s = 0

Tactic:
h₁.1 hs

Premises used: And.left
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
inst_1 : Finite α
val : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ #s = 0

Tactic:
exact h₁.1 hs

Premises used: And.left
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
inst_1 : Finite α
val : Fintype α
h₁ : IsInitSeg 𝒜 0
⊢ 𝒜 ⊆ {∅}

Tactic:
have : 𝒜 ⊆ {∅} := fun s hs ↦ by rw [mem_singleton, ← Finset.card_eq_zero]; exact h₁.1 hs
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
inst_1 : Finite α
val : Fintype α
h₁ : IsInitSeg 𝒜 0
this : 𝒜 ⊆ {∅}
⊢ ∂ 𝒜 ≤ ∂ {∅}

Tactic:
have := shadow_monotone this
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
inst_1 : Finite α
val : Fintype α
h₁ : IsInitSeg 𝒜 0
this_1 : 𝒜 ⊆ {∅}
this : ∂ 𝒜 ≤ ∂ {∅}
⊢ ∂ 𝒜 = ∅

Tactic:
simp only [subset_empty, le_eq_subset, shadow_singleton_empty] at this

Premises used: Finset.subset_empty, Finset.shadow_singleton_empty, Finset.le_eq_subset
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
inst_1 : Finite α
val : Fintype α
h₁ : IsInitSeg 𝒜 0
this_1 : 𝒜 ⊆ {∅}
this : ∂ 𝒜 = ∅
⊢ IsInitSeg (∂ 𝒜) (HSub.hSub (α := ℕ) 0 1)

Tactic:
simp [this]
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Finite α
h₁ : IsInitSeg 𝒜 r
val : Fintype α
hr : r > 0
intro : ∀ (h₁ : IsInitSeg.{u_1} (α := α) ∅ r), IsInitSeg.{u_1} (α := α) (∂ ∅) (r - 1)
intro₁ : ∀ (h𝒜 : 𝒜.Nonempty), IsInitSeg (∂ 𝒜) (r - 1)
⊢ IsInitSeg (∂ 𝒜) (r - 1)

Tactic:
obtain rfl | h𝒜 := 𝒜.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
r : ℕ
inst_1 : Finite α
val : Fintype α
hr : r > 0
h₁ : IsInitSeg.{u_1} (α := α) ∅ r
⊢ IsInitSeg.{u_1} (α := α) (∂ ∅) (r - 1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Finite α
h₁ : IsInitSeg 𝒜 r
val : Fintype α
hr : r > 0
h𝒜 : 𝒜.Nonempty
intro :
  ∀ (s : Finset α) (hr : #s > 0) (h𝒜 : (initSeg s).Nonempty) (h₁ : IsInitSeg (initSeg s) #s),
    IsInitSeg (∂ (initSeg s)) (#s - 1)
⊢ IsInitSeg (∂ 𝒜) (r - 1)

Tactic:
obtain ⟨s, rfl, rfl⟩ := h₁.exists_initSeg h𝒜

Premises used: Finset.Colex.IsInitSeg.exists_initSeg, rfl
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Finite α
val : Fintype α
s : Finset α
hr : #s > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) #s
intro : IsInitSeg (initSeg (s.erase (s.min' ⋯))) #(s.erase (s.min' ⋯))
rw : s.Nonempty
⊢ IsInitSeg (∂ (initSeg s)) (#s - 1)

Tactic:
rw [shadow_initSeg (card_pos.1 hr), ← card_erase_of_mem (min'_mem _ _)]

Premises used: Finset.min'_mem, Finset.card_erase_of_mem, Finset.Colex.shadow_initSeg, Iff.mp, Finset.card_pos
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Finite α
val : Fintype α
s : Finset α
hr : #s > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) #s
⊢ IsInitSeg (initSeg (s.erase (s.min' ⋯))) #(s.erase (s.min' ⋯))

Tactic:
isInitSeg_initSeg

Premises used: Finset.Colex.isInitSeg_initSeg
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : compress U V s ≠ s
⊢ (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s

Tactic:
rw [compress, ite_ne_right_iff] at hA

Premises used: UV.compress, ite_ne_right_iff
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
rw : ∃ w ∈ s \ ((s ⊔ U) \ V), {a ∈ (s ⊔ U) \ V | w < a} = {a ∈ s | w < a}
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (compress U V s) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))

Tactic:
rw [compress, if_pos hA.1, lt_iff_exists_filter_lt]

Premises used: Finset.Colex.lt_iff_exists_filter_lt, if_pos, And.left, UV.compress
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
simp_rw : ∃ w ∈ s, w ∉ (s ⊔ U) \ V ∧ ∀ ⦃a : α⦄, w < a → (a ∈ (s ⊔ U) \ V ↔ a ∈ s)
⊢ ∃ w ∈ s \ ((s ⊔ U) \ V), {a ∈ (s ⊔ U) \ V | w < a} = {a ∈ s | w < a}

Tactic:
simp_rw [mem_sdiff (s := s), filter_inj, and_assoc]

Premises used: Finset.mem_sdiff, and_assoc, Finset.filter_inj
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
⊢ ∃ w ∈ s, w ∉ (s ⊔ U) \ V ∧ ∀ ⦃a : α⦄, w < a → (a ∈ (s ⊔ U) \ V ↔ a ∈ s)

Tactic:
⟨_, hA.1.2 <| max'_mem _ hV, notMem_sdiff_of_mem_right <| max'_mem _ _, fun a ha ↦ ?_⟩

Premises used: Finset.max'_mem, Finset.notMem_sdiff_of_mem_right, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
refine : ∀ (a : α) (ha : V.max' hV < a), a ∈ (s ⊔ U) \ V ↔ a ∈ s
⊢ ∃ w ∈ s, w ∉ (s ⊔ U) \ V ∧ ∀ ⦃a : α⦄, w < a → (a ∈ (s ⊔ U) \ V ↔ a ∈ s)

Tactic:
refine ⟨_, hA.1.2 <| max'_mem _ hV, notMem_sdiff_of_mem_right <| max'_mem _ _, fun a ha ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
⊢ a ∉ V

Tactic:
have : a ∉ V := fun H ↦ ha.not_ge (le_max' _ _ H)
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s U V : Finset α
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
hA : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
a : α
ha : V.max' hV < a
this : a ∉ V
⊢ a ∉ U

Tactic:
have : a ∉ U := fun H ↦ ha.not_gt ((le_max' _ _ H).trans_lt h)
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₁ : UsefulCompression U V
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
⊢ Disjoint U V

Tactic:
obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁

Premises used: max_lt
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₁ : UsefulCompression U V
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
⊢ #U = #V

Tactic:
obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁

Premises used: max_lt
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₁ : UsefulCompression U V
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
⊢ U.Nonempty

Tactic:
obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁

Premises used: max_lt
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₁ : UsefulCompression U V
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
⊢ V.Nonempty

Tactic:
obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁

Premises used: max_lt
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₁ : UsefulCompression U V
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
⊢ U.max' hU < V.max' hV

Tactic:
obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁

Premises used: max_lt
-- 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
⊢ #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)

Tactic:
card_shadow_compression_le _ _ fun x Hx ↦ ⟨min' V hV, min'_mem _ _, ?_⟩

Premises used: Finset.min', UV.card_shadow_compression_le, Finset.min'_mem, And.intro, Exists.intro
-- 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
refine : ∀ (x : α) (Hx : x ∈ U), IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
⊢ #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)

Tactic:
refine card_shadow_compression_le _ _ fun x Hx ↦ ⟨min' V hV, min'_mem _ _, ?_⟩

Premises used: Finset.min', UV.card_shadow_compression_le, Finset.min'_mem, And.intro, Exists.intro
-- 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
inl : ∀ (hU' : succ 0 = #U), IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
inr : ∀ (hU' : succ 0 < #U), IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

Tactic:
obtain hU' | hU' := eq_or_lt_of_le (succ_le_iff.2 hU.card_pos)

Premises used: Iff.mpr, Finset.Nonempty.card_pos, eq_or_lt_of_le, Nat.succ_le_iff
-- 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
inl :
  ∀ (same_size : succ 0 = #V) (hU : U.Nonempty) (hV : V.Nonempty) (max_lt : U.max' hU < V.max' hV) (x : α) (Hx : x ∈ U)
    (hU' : succ 0 = #U), IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

Tactic:
rw [← hU'] at 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 : succ 0 = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = #U
rw : #(U.erase x) = 0
rw₁ : #U - 1 = 0
rw₂ rw₃ : succ 0 - 1 = 0
⊢ U.erase x = ∅

Tactic:
rw [← Finset.card_eq_zero, card_erase_of_mem Hx, ← hU']

Premises used: Finset.card_erase_of_mem, Finset.card_eq_zero
-- 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 : succ 0 = #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 = ∅

Tactic:
have : erase U x = ∅ := by rw [← Finset.card_eq_zero, card_erase_of_mem Hx, ← hU']
-- 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 : succ 0 = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = #U
this : U.erase x = ∅
rw : #(V.erase (V.min' hV)) = 0
rw₁ : #V - 1 = 0
rw₂ rw₃ : succ 0 - 1 = 0
⊢ V.erase (V.min' hV) = ∅

Tactic:
rw [← Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ← same_size]

Premises used: Finset.min'_mem, Finset.card_erase_of_mem, Finset.card_eq_zero
-- 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 : succ 0 = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = #U
this : U.erase x = ∅
⊢ V.erase (V.min' hV) = ∅

Tactic:
have : erase V (min' V hV) = ∅ := by
      rw [← Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ← 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 : succ 0 = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = #U
this_1 : U.erase x = ∅
this : V.erase (V.min' hV) = ∅
inl : IsCompressed ∅ ∅ 𝒜
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

Tactic:
rw [‹erase U x = ∅›, ‹erase V (min' V hV) = ∅›]

Premises used: Finset.min', Finset.erase
-- 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 : succ 0 = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = #U
this_1 : U.erase x = ∅
this : V.erase (V.min' hV) = ∅
⊢ IsCompressed ∅ ∅ 𝒜

Tactic:
isCompressed_self _ _

Premises used: UV.isCompressed_self
-- 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 : succ 0 = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 = #U
this_1 : U.erase x = ∅
this : V.erase (V.min' hV) = ∅
⊢ IsCompressed ∅ ∅ 𝒜

Tactic:
exact isCompressed_self _ _

Premises used: UV.isCompressed_self
-- 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
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

Tactic:
h₂ ⟨UVd.mono (erase_subset ..) (erase_subset ..), ?_, ?_, ?_, ?_⟩ (card_erase_lt_of_mem Hx)

Premises used: Finset.card_erase_lt_of_mem, And.intro, Exists.intro, Disjoint.mono, Finset.erase_subset
-- 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.erase (V.min' hV))
inr₁ : (U.erase x).Nonempty
inr₂ : (V.erase (V.min' hV)).Nonempty
inr₃ : (U.erase x).max' ⋯ < (V.erase (V.min' hV)).max' ⋯
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜

Tactic:
refine h₂ ⟨UVd.mono (erase_subset ..) (erase_subset ..), ?_, ?_, ?_, ?_⟩ (card_erase_lt_of_mem Hx)

Premises used: Finset.card_erase_lt_of_mem, And.intro, Exists.intro, Disjoint.mono, Finset.erase_subset