awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
hf₁ :
  ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet (↑(f' j) : Set (Finset α))
inr :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) * (HPow.hPow (α := ℕ) 2 (Fintype.card α) + #(s.biUnion f')) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) *
      (2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * Fintype.card.{u_2} (Finset α) + 2 * (#(s.biUnion f') * #(f' i)ᶜ) ≤
    2 * HPow.hPow (α := ℕ) 2 (Fintype.card α) *
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))

Tactic:
rw [mul_tsub, card_compl, Fintype.card_finset, mul_left_comm, mul_tsub,
    (hf₁ _ <| mem_cons_self _ _).2.1, two_mul, add_tsub_cancel_left, ← mul_tsub, ← mul_two,
    mul_assoc, ← add_mul, mul_comm]

Premises used: add_mul, Finset.card_compl, mul_assoc, two_mul, add_tsub_cancel_left, mul_left_comm, Fintype.card_finset, And.right, And.left, mul_comm, Finset.mem_cons_self, mul_two, mul_tsub
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
hf₁ :
  ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet (↑(f' j) : Set (Finset α))
inr :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) + #(s.biUnion f') ≤
    2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * (HPow.hPow (α := ℕ) 2 (Fintype.card α) + #(s.biUnion f')) ≤
    HPow.hPow (α := ℕ) 2 (Fintype.card α) *
      (2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi))))

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
hf₁ :
  ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet (↑(f' j) : Set (Finset α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) + #(s.biUnion f') ≤
    2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))

Tactic:
(add_le_add_right
    (ih _ (fun i hi ↦ (hf₁ _ <| subset_cons _ hi).2.2)
    ((card_le_card <| subset_cons _).trans hs)) _).trans ?_

Premises used: Finset.card_le_card, Finset.subset_cons, add_le_add_right, And.right, LE.le.trans
-- Module: Mathlib.Combinatorics.SetFamily.Kleitman
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)) (hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting) (hs : #s ≤ Fintype.card α),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1) : Set (Finset α)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun (j : ι) ↦
    if hj : j ∈ cons i s hi then
      Exists.choose (p := fun (t : Finset (Finset α)) ↦
        f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) ⋯
    else ∅
hf₁ :
  ∀ j ∈ cons i s hi,
    f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet (↑(f' j) : Set (Finset α))
inr :
  HPow.hPow (α := ℕ) 2 (Fintype.card α) +
      (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)) ≤
    2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) + #(s.biUnion f') ≤
    2 * (HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #(cons i s hi)))

Tactic:
refine (add_le_add_right
    (ih _ (fun i hi ↦ (hf₁ _ <| subset_cons _ hi).2.2)
    ((card_le_card <| subset_cons _).trans hs)) _).trans ?_

Premises used: Finset.card_le_card, Finset.subset_cons, add_le_add_right, And.right, LE.le.trans
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
h : ∀ (t : Finset α), t ∈ ∂ (initSeg s) ↔ t ∈ initSeg (s.erase (s.min' hs))
⊢ ∂ (initSeg s) = initSeg (s.erase (s.min' hs))

Tactic:
ext t
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
h :
  (∃ 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 α))) ↔
    #(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 α))
⊢ t ∈ ∂ (initSeg s) ↔ t ∈ initSeg (s.erase (s.min' hs))

Tactic:
simp only [mem_shadow_iff_insert_mem, mem_initSeg]

Premises used: Finset.Colex.mem_initSeg, Finset.mem_shadow_iff_insert_mem
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
h :
  (∃ 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 α))) →
    #(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 α))
h₁ :
  #(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 α))
⊢ (∃ 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 α))) ↔
    #(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 α))

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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.erase (s.min' hs)) = #t
h₁ :
  LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (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 α))

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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
h₃ h₄ : #t = #t
⊢ #(s.erase (s.min' hs)) = #t

Tactic:
rw [card_erase_of_mem (min'_mem _ _), hst, card_insert_of_notMem ha, add_tsub_cancel_right]

Premises used: Finset.min'_mem, Finset.card_erase_of_mem, Finset.card_insert_of_notMem, add_tsub_cancel_right
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 α))
⊢ LE.le (α := Colex (Finset α)) ((toColex : (a : Finset α) → Colex (Finset α)) t : Colex (Finset α))
    ((toColex : (a : Finset α) → Colex (Finset α)) (s.erase (s.min' hs)) : Colex (Finset α))

Tactic:
simpa [ha] using erase_le_erase_min' hts hst.ge (mem_insert_self _ _)

Premises used: Eq.ge, Finset.mem_insert_self, Finset.Colex.erase_le_erase_min'
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
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))
⊢ #(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 α))

Tactic:
simp_rw [le_iff_eq_or_lt, lt_iff_exists_filter_lt, mem_sdiff, filter_inj, and_assoc]

Premises used: le_iff_eq_or_lt, Finset.Colex.lt_iff_exists_filter_lt, Finset.mem_sdiff, and_assoc, Finset.filter_inj
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
Goal:
α : Type u_1
inst : LinearOrder α
s : Finset α
inst_1 : Fintype α
hs : s.Nonempty
t : Finset α
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))
⊢ #(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 only [toColex_inj, and_imp]

Premises used: and_imp, toColex_inj
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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))

Tactic:
⟨min' s hs, notMem_erase _ _, ?_⟩

Premises used: Finset.min', And.intro, Exists.intro, Finset.notMem_erase
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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))
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))
⊢ ∃ 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))

Tactic:
refine ⟨min' s hs, notMem_erase _ _, ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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))
h : #s = #s ∧ (s = s ∨ ∃ w ∈ s, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ s))
⊢ #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:
rw [insert_erase (min'_mem _ _)]

Premises used: Finset.min'_mem, Finset.insert_erase
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 = #s ∧ (s = s ∨ ∃ w ∈ s, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ s))

Tactic:
⟨rfl, Or.inl rfl⟩

Premises used: And.intro, Or.inl, rfl
-- Module: Mathlib.Combinatorics.SetFamily.KruskalKatona
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 = #s ∧ (s = s ∨ ∃ w ∈ s, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ s))

Tactic:
exact ⟨rfl, Or.inl rfl⟩
-- 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' ⋯
⊢ j ≤ k

Tactic:
have hjk : j ≤ k := min'_le _ _ (mem_compl.2 ‹k ∉ t›)
-- 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
⊢ j ∉ t

Tactic:
have : j ∉ t := mem_compl.1 (min'_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
rw : #s = #t + 1
rw₁ : #s = #(s.erase (s.min' hs)) + 1
rw₂ rw₃ : #s = #s
⊢ #s = #(insert j t)

Tactic:
rw [card_insert_of_notMem ‹j ∉ t›, ← ‹_ = #t›, card_erase_add_one (min'_mem _ _)]

Premises used: Finset.card_erase_add_one, Finset.min'_mem, Finset.card_insert_of_notMem
-- 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
⊢ #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 _ _)]
-- 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)
⊢ ∃ 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:
⟨j, ‹_›, hcard, ?_⟩

Premises used: And.intro, Exists.intro
-- 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)
h : insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
⊢ ∃ 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:
refine ⟨j, ‹_›, hcard, ?_⟩
-- 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)
h : ∀ (hjk : j < k), insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)
h₁ : ∀ (r₁ : 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)

Tactic:
obtain hjk | r₁ := hjk.lt_or_eq

Premises used: LE.le.lt_or_eq
-- 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_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)

Tactic:
Or.inr ⟨k, mem_of_mem_erase ‹_›, fun hk ↦ hkt <| mem_of_mem_insert_of_ne hk hjk.ne',
      fun x hx ↦ ?_⟩

Premises used: LT.lt.ne', Finset.mem_of_mem_erase, And.intro, Exists.intro, Finset.mem_of_mem_insert_of_ne, Or.inr
-- 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_1 : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
hjk : j < k
h : ∀ (x : α) (hx : k < x), x ∈ insert j t ↔ x ∈ s
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ 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 ↦ ?_⟩

Premises used: Or.inr
-- 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_1 : j ≤ k
this : j ∉ t
hcard : #s = #(insert j t)
hjk : j < k
x : α
hx : k < x
⊢ x ∈ insert j t ↔ x ∈ s

Tactic:
simpa only [mem_insert, z hx, (hjk.trans hx).ne', mem_erase, Ne, false_or,
      and_iff_right_iff_imp] using fun _ ↦ ((min'_le _ _ <| mem_of_mem_erase hks).trans_lt hx).ne'

Premises used: Finset.min'_le, Finset.mem_insert, Ne, false_or, LT.lt.ne', Finset.mem_erase, Finset.mem_of_mem_erase, and_iff_right_iff_imp, LT.lt.trans, LE.le.trans_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
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)

Tactic:
Or.inl (eq_of_subset_of_card_le (fun a ha ↦ ?_) hcard.ge).symm

Premises used: Eq.ge, Or.inl, Finset.eq_of_subset_of_card_le, Eq.symm
-- 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
h : ∀ (a : α) (ha : a ∈ s), a ∈ insert j t
⊢ insert j t = s ∨ ∃ w ∈ s, w ∉ insert j t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ insert j t ↔ a ∈ s)

Tactic:
refine Or.inl (eq_of_subset_of_card_le (fun a ha ↦ ?_) hcard.ge).symm

Premises used: Eq.ge, Or.inl, Finset.eq_of_subset_of_card_le, Eq.symm