awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
h : #s - 1 = #t
h₁ : #(insert a t) - 1 = #t
⊢ #(s.erase (s.min' hs)) = #t
have h₂ : #t + 1 - 1 = #t
Tactic: rw [card_erase_of_mem (min'_mem _ _), hst, card_insert_of_notMem ha, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
h : #s - 1 = #t
h₁ : #(insert a t) - 1 = #t
h₂ : #t + 1 - 1 = #t
⊢ #(s.erase (s.min' hs)) = #t
have h₃ : #t = #t
Tactic: rw [card_erase_of_mem (min'_mem _ _), hst, card_insert_of_notMem ha, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t ∧
      LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α)) →
    ∃ a ∉ t,
      #s = #(insert a t) ∧
        LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
          ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
have h : #(s.erase (s.min' hs)) = #t ∧
    (Eq (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
        ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α)) ∨
      ∃ w ∈ s.erase (s.min' hs), w ∉ t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
  ∃ a ∉ t,
    #s = #(insert a t) ∧
      (Eq (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
          ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) ∨
        ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Tactic: simp_rw [le_iff_eq_or_lt, lt_iff_exists_filter_lt, mem_sdiff, filter_inj, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t ∧
      (Eq (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
          ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α)) ∨
        ∃ w ∈ s.erase (s.min' hs), w ∉ t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
    ∃ a ∉ t,
      #s = #(insert a t) ∧
        (Eq (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (insert a t) : Colex (Finset α))
            ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α)) ∨
          ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
have h : #(s.erase (s.min' hs)) = #t →
  (t = s.erase (s.min' hs) ∨ ∃ w ∈ s.erase (s.min' hs), w ∉ t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
    ∃ a ∉ t,
      #s = #(insert a t) ∧
        (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Tactic: simp only [toColex_inj, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
cards' : #(s.erase (s.min' hs)) = #(s.erase (s.min' hs))
⊢ ∃ a ∉ s.erase (s.min' hs),
    #s = #(insert a (s.erase (s.min' hs))) ∧
      (insert a (s.erase (s.min' hs)) = s ∨
        ∃ w ∈ s,
          w ∉ insert a (s.erase (s.min' hs)) ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a (s.erase (s.min' hs)) ↔ a_1 ∈ s))
have h : #s = #(insert (s.min' hs) (s.erase (s.min' hs))) ∧
  (insert (s.min' hs) (s.erase (s.min' hs)) = s ∨
    ∃ w ∈ s,
      w ∉ insert (s.min' hs) (s.erase (s.min' hs)) ∧
        ∀ ⦃a : α⦄, w < a → (a ∈ insert (s.min' hs) (s.erase (s.min' hs)) ↔ a ∈ s))
Tactic: refine ⟨min' s hs, notMem_erase _ _, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
cards' : #(s.erase (s.min' hs)) = #(s.erase (s.min' hs))
⊢ #s = #(insert (s.min' hs) (s.erase (s.min' hs))) ∧
    (insert (s.min' hs) (s.erase (s.min' hs)) = s ∨
      ∃ w ∈ s,
        w ∉ insert (s.min' hs) (s.erase (s.min' hs)) ∧
          ∀ ⦃a : α⦄, w < a → (a ∈ insert (s.min' hs) (s.erase (s.min' hs)) ↔ a ∈ s))
have h : #s = #s ∧ (s = s ∨ ∃ w ∈ s, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ s))
Tactic: rw [insert_erase (min'_mem _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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' ⋯
⊢ ∃ a ∉ t,
    #s = #(insert a t) ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
have hjk : j ≤ k
Tactic: have hjk : j ≤ k := min'_le _ _ (mem_compl.2 ‹k ∉ t›)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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
⊢ ∃ a ∉ t,
    #s = #(insert a t) ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
have this : j ∉ t
Tactic: have : j ∉ t := mem_compl.1 (min'_mem _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ #s = #(insert j t)
have rw : #s = #t + 1
Tactic: rw [card_insert_of_notMem ‹j ∉ t›, ← ‹_ = #t›, card_erase_add_one (min'_mem _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
rw : #s = #t + 1
⊢ #s = #(insert j t)
have rw₁ : #s = #(s.erase (s.min' hs)) + 1
Tactic: rw [card_insert_of_notMem ‹j ∉ t›, ← ‹_ = #t›, card_erase_add_one (min'_mem _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
rw : #s = #t + 1
rw₁ : #s = #(s.erase (s.min' hs)) + 1
⊢ #s = #(insert j t)
have rw₂ : #s = #s
Tactic: rw [card_insert_of_notMem ‹j ∉ t›, ← ‹_ = #t›, card_erase_add_one (min'_mem _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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
⊢ ∃ a ∉ t,
    #s = #(insert a t) ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
have hcard : #s = #(insert j t)
Tactic: have hcard : #s = #(insert j t) := by
    rw [card_insert_of_notMem ‹j ∉ t›, ← ‹_ = #t›, card_erase_add_one (min'_mem _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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)
⊢ ∃ a ∉ t,
    #s = #(insert a t) ∧
      (insert a t = s ∨ ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
have h : insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
Tactic: refine ⟨j, ‹_›, hcard, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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)
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
have h : ∀ (hjk : j < k), insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
Tactic: obtain hjk | r₁ := hjk.lt_or_eq
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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)
h : ∀ (hjk : j < k), insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
have h₁ : ∀ (r₁ : j = k), insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
Tactic: obtain hjk | r₁ := hjk.lt_or_eq
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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_1 : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
hjk : j < k
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
have h : ∀ (x : α) (hx : k < x), x ∈ insert j t ↔ x ∈ s
Tactic: refine Or.inr ⟨k, mem_of_mem_erase ‹_›, fun hk ↦ hkt <| mem_of_mem_insert_of_ne hk hjk.ne',
      fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
have h : ∀ (a : α) (ha : a ∈ s), a ∈ insert j t
Tactic: refine Or.inl (eq_of_subset_of_card_le (fun a ha ↦ ?_) hcard.ge).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ a ∈ insert j t
have h : ∀ (lt : k < a), a ∈ insert j t
Tactic: rcases lt_trichotomy k a with (lt | rfl | gt)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ a ∈ insert j t
have h₁ : ∀ (ha : k ∈ s), k ∈ insert j t
Tactic: rcases lt_trichotomy k a with (lt | rfl | gt)
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ a ∈ insert j t
have h₂ : ∀ (gt : a < k), a ∈ insert j t
Tactic: rcases lt_trichotomy k a with (lt | rfl | gt)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 ∈ insert j t
have h : a ∈ t
Tactic: apply mem_insert_of_mem
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 ∈ t
have h : a ∈ s.erase (s.min' hs)
Tactic: rw [z lt]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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)
have h : s.min' hs ≤ k
Tactic: refine mem_erase_of_ne_of_mem (lt_of_le_of_lt ?_ lt).ne' ha
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 j t
have h : k ∈ insert k t
Tactic: rw [r₁]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 ∈ insert j t
have h : a ∈ t
Tactic: apply mem_insert_of_mem
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
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 ∈ t
have gt₁ : a < j
Tactic: rw [← r₁] at gt
Cleared hypotheses: gt
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ a ∈ t
have h : ∀ (this : a ∉ t), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ False
have apply : a ∈ tᶜ
Tactic: apply (min'_le tᶜ _ _).not_gt gt
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Finite α
h₁ : IsInitSeg 𝒜 r
⊢ IsInitSeg (∂ 𝒜) (r - 1)
have intro : ∀ (val : Fintype α), IsInitSeg (∂ 𝒜) (r - 1)
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Finite α
h₁ : IsInitSeg 𝒜 r
val : Fintype α
⊢ IsInitSeg (∂ 𝒜) (r - 1)
have intro : ∀ (h₁ : IsInitSeg 𝒜 0), IsInitSeg (∂ 𝒜) (HSub.hSub (α := ℕ) 0 1)
Tactic: obtain rfl | hr := Nat.eq_zero_or_pos r
Cleared hypotheses: r, h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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)
⊢ IsInitSeg (∂ 𝒜) (r - 1)
have intro₁ : ∀ (hr : r > 0), IsInitSeg (∂ 𝒜) (r - 1)
Tactic: obtain rfl | hr := Nat.eq_zero_or_pos r
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
inst_1 : Finite α
val : Fintype α
h₁ : IsInitSeg 𝒜 0
s : Finset α
hs : s ∈ 𝒜
⊢ Membership.mem (γ := Finset (Finset α)) {∅} s
have rw : #s = 0
Tactic: rw [mem_singleton, ← Finset.card_eq_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
inst_1 : Finite α
val : Fintype α
h₁ : IsInitSeg 𝒜 0
⊢ IsInitSeg (∂ 𝒜) (HSub.hSub (α := ℕ) 0 1)
have this : 𝒜 ⊆ {∅}
Tactic: have : 𝒜 ⊆ {∅} := fun s hs ↦ by rw [mem_singleton, ← Finset.card_eq_zero]; exact h₁.1 hs
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
inst_1 : Finite α
val : Fintype α
h₁ : IsInitSeg 𝒜 0
this : 𝒜 ⊆ {∅}
⊢ IsInitSeg (∂ 𝒜) (HSub.hSub (α := ℕ) 0 1)
have this₁ : ∂ 𝒜 ≤ ∂ {∅}
Tactic: have := shadow_monotone this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
inst_1 : Finite α
val : Fintype α
h₁ : IsInitSeg 𝒜 0
this_1 : 𝒜 ⊆ {∅}
this : ∂ 𝒜 ≤ ∂ {∅}
⊢ IsInitSeg (∂ 𝒜) (HSub.hSub (α := ℕ) 0 1)
have this₁ : ∂ 𝒜 = ∅
Tactic: simp only [subset_empty, le_eq_subset, shadow_singleton_empty] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Finite α
h₁ : IsInitSeg 𝒜 r
val : Fintype α
hr : r > 0
⊢ IsInitSeg (∂ 𝒜) (r - 1)
have intro : ∀ (h₁ : IsInitSeg.{u_1} (α := α) ∅ r), IsInitSeg.{u_1} (α := α) (∂ ∅) (r - 1)
Tactic: obtain rfl | h𝒜 := 𝒜.eq_empty_or_nonempty
Cleared hypotheses: 𝒜, h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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)
⊢ IsInitSeg (∂ 𝒜) (r - 1)
have intro₁ : ∀ (h𝒜 : 𝒜.Nonempty), IsInitSeg (∂ 𝒜) (r - 1)
Tactic: obtain rfl | h𝒜 := 𝒜.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
Goal:
α : Type u_1
inst : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst_1 : Finite α
h₁ : IsInitSeg 𝒜 r
val : Fintype α
hr : r > 0
h𝒜 : 𝒜.Nonempty
⊢ IsInitSeg (∂ 𝒜) (r - 1)
have intro : ∀ (s : Finset α) (hr : #s > 0) (h𝒜 : (initSeg s).Nonempty) (h₁ : IsInitSeg (initSeg s) #s),
  IsInitSeg (∂ (initSeg s)) (#s - 1)
Tactic: obtain ⟨s, rfl, rfl⟩ := h₁.exists_initSeg h𝒜
Cleared hypotheses: 𝒜, r, h₁, hr, h𝒜
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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)) (#s - 1)
have intro : IsInitSeg (initSeg (s.erase (s.min' sorry))) #(s.erase (s.min' sorry))
Tactic: rw [shadow_initSeg (card_pos.1 hr), ← card_erase_of_mem (min'_mem _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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' ⋯))
⊢ IsInitSeg (∂ (initSeg s)) (#s - 1)
have rw : s.Nonempty
Tactic: rw [shadow_initSeg (card_pos.1 hr), ← card_erase_of_mem (min'_mem _ _)]
-- 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 : compress U V s ≠ s
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (compress U V s) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
have hA₁ : (Disjoint U s ∧ V ≤ s) ∧ (s ⊔ U) \ V ≠ s
Tactic: rw [compress, ite_ne_right_iff] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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
⊢ LT.lt (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) (compress U V s) : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) s : Colex (Finset α))
have rw : ∃ w ∈ s \ ((s ⊔ U) \ V), {a ∈ (s ⊔ U) \ V | w < a} = {a ∈ s | w < a}
Tactic: rw [compress, if_pos hA.1, lt_iff_exists_filter_lt]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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 \ ((s ⊔ U) \ V), {a ∈ (s ⊔ U) \ V | w < a} = {a ∈ s | w < a}
have simp_rw : ∃ w ∈ s, w ∉ (s ⊔ U) \ V ∧ ∀ ⦃a : α⦄, w < a → (a ∈ (s ⊔ U) \ V ↔ a ∈ s)
Tactic: simp_rw [mem_sdiff (s := s), filter_inj, and_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.KruskalKatona (goal)
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)
have refine : ∀ (a : α) (ha : V.max' hV < 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 ↦ ?_⟩