awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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 ∈ (s ⊔ U) \ V ↔ a ∈ s
have this : a ∉ V
Tactic: have : a ∉ V := fun H ↦ ha.not_ge (le_max' _ _ H)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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 ∈ (s ⊔ U) \ V ↔ a ∈ s
have this₁ : a ∉ U
Tactic: have : a ∉ U := fun H ↦ ha.not_gt ((le_max' _ _ H).trans_lt h)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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₁ 𝒜
⊢ #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
have UVd : Disjoint U V
Tactic: obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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 𝒜)) ≤ #(∂ 𝒜)
have same_size : #U = #V
Tactic: obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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 V 𝒜)) ≤ #(∂ 𝒜)
have hU : U.Nonempty
Tactic: obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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
⊢ #(∂ (𝓒 U V 𝒜)) ≤ #(∂ 𝒜)
have hV : V.Nonempty
Tactic: obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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 V 𝒜)) ≤ #(∂ 𝒜)
have max_lt : U.max' hU < V.max' hV
Tactic: obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 𝒜)) ≤ #(∂ 𝒜)
have refine : ∀ (x : α) (Hx : x ∈ U), IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
Tactic: refine card_shadow_compression_le _ _ fun x Hx ↦ ⟨min' V hV, min'_mem _ _, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
have inl : ∀ (hU' : succ 0 = #U), 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)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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)) 𝒜
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
have inr : ∀ (hU' : succ 0 < #U), 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)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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)) 𝒜
have 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)) 𝒜
Tactic: rw [← hU'] at same_size
Cleared hypotheses: same_size, hU, hV, max_lt, x, Hx, hU'
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 = ∅
have rw : #(U.erase x) = 0
Tactic: rw [← Finset.card_eq_zero, card_erase_of_mem Hx, ← hU']
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ U.erase x = ∅
have rw₁ : #U - 1 = 0
Tactic: rw [← Finset.card_eq_zero, card_erase_of_mem Hx, ← hU']
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ U.erase x = ∅
have rw₂ : succ 0 - 1 = 0
Tactic: rw [← Finset.card_eq_zero, card_erase_of_mem Hx, ← hU']
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
have this : U.erase x = ∅
Tactic: have : erase U x = ∅ := by rw [← Finset.card_eq_zero, card_erase_of_mem Hx, ← hU']
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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) = ∅
have rw : #(V.erase (V.min' hV)) = 0
Tactic: rw [← Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ← same_size]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ V.erase (V.min' hV) = ∅
have rw₁ : #V - 1 = 0
Tactic: rw [← Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ← same_size]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ V.erase (V.min' hV) = ∅
have rw₂ : succ 0 - 1 = 0
Tactic: rw [← Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ← same_size]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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 = ∅
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
have this₁ : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 (U.erase x) (V.erase (V.min' hV)) 𝒜
have inl : IsCompressed ∅ ∅ 𝒜
Tactic: rw [‹erase U x = ∅›, ‹erase V (min' V hV) = ∅›]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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)) 𝒜
have inr : #(U.erase x) = #(V.erase (V.min' hV))
Tactic: refine h₂ ⟨UVd.mono (erase_subset ..) (erase_subset ..), ?_, ?_, ?_, ?_⟩ (card_erase_lt_of_mem Hx)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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))
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
have inr₁ : (U.erase x).Nonempty
Tactic: refine h₂ ⟨UVd.mono (erase_subset ..) (erase_subset ..), ?_, ?_, ?_, ?_⟩ (card_erase_lt_of_mem Hx)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
have inr₂ : (V.erase (V.min' hV)).Nonempty
Tactic: refine h₂ ⟨UVd.mono (erase_subset ..) (erase_subset ..), ?_, ?_, ?_, ?_⟩ (card_erase_lt_of_mem Hx)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ IsCompressed (U.erase x) (V.erase (V.min' hV)) 𝒜
have inr₃ : (U.erase x).max' sorry < (V.erase (V.min' hV)).max' sorry
Tactic: refine h₂ ⟨UVd.mono (erase_subset ..) (erase_subset ..), ?_, ?_, ?_, ?_⟩ (card_erase_lt_of_mem Hx)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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) = #(V.erase (V.min' hV))
have inr : #(U.erase x) = #V - 1
Tactic: rw [card_erase_of_mem (min'_mem _ _), card_erase_of_mem Hx, same_size]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ #(U.erase x) = #(V.erase (V.min' hV))
have inr₁ : #U - 1 = #V - 1
Tactic: rw [card_erase_of_mem (min'_mem _ _), card_erase_of_mem Hx, same_size]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ #(U.erase x) = #(V.erase (V.min' hV))
have inr₂ : #V - 1 = #V - 1
Tactic: rw [card_erase_of_mem (min'_mem _ _), card_erase_of_mem Hx, same_size]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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).Nonempty
have inr : 0 < #(U.erase x)
Tactic: rwa [← card_pos, card_erase_of_mem Hx, tsub_pos_iff_lt]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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)
⊢ (U.erase x).Nonempty
have inr₁ : 0 < #U - 1
Tactic: rwa [← card_pos, card_erase_of_mem Hx, tsub_pos_iff_lt]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ (V.erase (V.min' hV)).Nonempty
have inr : 0 < #(V.erase (V.min' hV))
Tactic: rwa [← Finset.card_pos, card_erase_of_mem (min'_mem _ _), ← same_size, tsub_pos_iff_lt]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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))
⊢ (V.erase (V.min' hV)).Nonempty
have inr₁ : 0 < #V - 1
Tactic: rwa [← Finset.card_pos, card_erase_of_mem (min'_mem _ _), ← same_size, tsub_pos_iff_lt]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ (V.erase (V.min' hV)).Nonempty
have inr₂ : 0 < #U - 1
Tactic: rwa [← Finset.card_pos, card_erase_of_mem (min'_mem _ _), ← same_size, tsub_pos_iff_lt]
-- 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 ℬ
⊢ IsInitSeg ℬ r
have 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 ∈ ℬ
Tactic: refine ⟨h₁, ?_⟩
-- 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
⊢ B ∈ ℬ
have by_contra : ∀ (hB : B ∉ ℬ), False
Tactic: by_contra hB
-- 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 ∉ ℬ
⊢ False
have hAB : A ≠ B
Tactic: have hAB : A ≠ B := ne_of_mem_of_not_mem hA hB
-- 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
⊢ False
have hAB' : #A = #B
Tactic: have hAB' : #A = #B := (h₁ hA).trans sizeA.symm
-- 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
⊢ False
have hU : (A \ B).Nonempty
Tactic: have hU : (A \ B).Nonempty := sdiff_nonempty.2 fun h ↦ hAB <| eq_of_subset_of_card_le h hAB'.ge
-- 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
⊢ False
have hV : (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
-- 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
⊢ False
have disj : Disjoint (B \ A) (A \ B)
Tactic: have disj : Disjoint (B \ A) (A \ B) := disjoint_sdiff.mono_left sdiff_subset
-- 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)
⊢ (B \ A).max' hV < (A \ B).max' hU
have inl : ∀ (hlt : (A \ B).max' hU < (B \ A).max' hV), (B \ A).max' hV < (A \ B).max' hU
Tactic: obtain hlt | heq | hgt := lt_trichotomy (max' _ hU) (max' _ hV)
-- 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)
inl : ∀ (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
have inr : ∀ (heq : (A \ B).max' hU = (B \ A).max' hV), (B \ A).max' hV < (A \ B).max' hU
Tactic: obtain hlt | heq | hgt := lt_trichotomy (max' _ hU) (max' _ hV)
-- 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)
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
⊢ (B \ A).max' hV < (A \ B).max' hU
have inr₁ : ∀ (hgt : (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)