awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
refine : ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t), 2 * #s = Fintype.card α
refine₁ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t),
    s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯ = Finset.univ
refine₂ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t), (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α) = univ
refine₃ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α), a ∈ (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α)
refine₄ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α), a ∈ (↑s : Set α) ∨ aᶜ ∈ (↑s : Set α)
refine₅ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), False
refine₆ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), (↑(insert a s) : Set α).Intersecting
refine₇ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), (insert a (↑s : Set α)).Intersecting
⊢ (∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) ↔ 2 * #s = Fintype.card α
have refine₈ : ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α) (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)),
  a ≠ ⊥
Tactic: classical
    refine ⟨fun h ↦ ?_, fun h t ht hst ↦ Finset.eq_of_subset_of_card_le hst <|
      Nat.le_of_mul_le_mul_left (ht.card_le.trans_eq h.symm) Nat.two_pos⟩
    suffices s.disjUnion (s.map ⟨compl, compl_injective⟩) hs.disjoint_map_compl = Finset.univ by
      rw [Fintype.card, ← this, Nat.two_mul, card_disjUnion, card_map]
    rw [← coe_eq_univ, disjUnion_eq_union, coe_union, coe_map, Function.Embedding.coeFn_mk,
      image_eq_preimage_of_inverse compl_compl compl_compl]
    refine eq_univ_of_forall fun a => ?_
    simp_rw [mem_union, mem_preimage]
    by_contra! ha
    refine s.ne_insert_of_notMem _ ha.1 (h _ ?_ <| s.subset_insert _)
    rw [coe_insert]
    refine hs.insert ?_ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb
    rintro rfl
    have := h {⊤} (by rw [coe_singleton]; exact intersecting_singleton.2 top_ne_bot)
    rw [compl_bot] at ha
    rw [coe_eq_empty.1 ((hs.isUpperSet' h).top_notMem.1 ha.2)] at this
    exact Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
refine : ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t), 2 * #s = Fintype.card α
refine₁ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t),
    s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯ = Finset.univ
refine₂ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t), (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α) = univ
refine₃ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α), a ∈ (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α)
refine₄ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α), a ∈ (↑s : Set α) ∨ aᶜ ∈ (↑s : Set α)
refine₅ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), False
refine₆ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), (↑(insert a s) : Set α).Intersecting
refine₇ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), (insert a (↑s : Set α)).Intersecting
refine₈ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), a ≠ ⊥
⊢ (∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) ↔ 2 * #s = Fintype.card α
have refine₉ : ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (ha : ⊥ ∉ (↑s : Set α) ∧ ⊥ᶜ ∉ (↑s : Set α)), False
Tactic: classical
    refine ⟨fun h ↦ ?_, fun h t ht hst ↦ Finset.eq_of_subset_of_card_le hst <|
      Nat.le_of_mul_le_mul_left (ht.card_le.trans_eq h.symm) Nat.two_pos⟩
    suffices s.disjUnion (s.map ⟨compl, compl_injective⟩) hs.disjoint_map_compl = Finset.univ by
      rw [Fintype.card, ← this, Nat.two_mul, card_disjUnion, card_map]
    rw [← coe_eq_univ, disjUnion_eq_union, coe_union, coe_map, Function.Embedding.coeFn_mk,
      image_eq_preimage_of_inverse compl_compl compl_compl]
    refine eq_univ_of_forall fun a => ?_
    simp_rw [mem_union, mem_preimage]
    by_contra! ha
    refine s.ne_insert_of_notMem _ ha.1 (h _ ?_ <| s.subset_insert _)
    rw [coe_insert]
    refine hs.insert ?_ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb
    rintro rfl
    have := h {⊤} (by rw [coe_singleton]; exact intersecting_singleton.2 top_ne_bot)
    rw [compl_bot] at ha
    rw [coe_eq_empty.1 ((hs.isUpperSet' h).top_notMem.1 ha.2)] at this
    exact Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
refine : ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t), 2 * #s = Fintype.card α
refine₁ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t),
    s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯ = Finset.univ
refine₂ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t), (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α) = univ
refine₃ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α), a ∈ (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α)
refine₄ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α), a ∈ (↑s : Set α) ∨ aᶜ ∈ (↑s : Set α)
refine₅ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), False
refine₆ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), (↑(insert a s) : Set α).Intersecting
refine₇ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), (insert a (↑s : Set α)).Intersecting
refine₈ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), a ≠ ⊥
refine₉ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (ha : ⊥ ∉ (↑s : Set α) ∧ ⊥ᶜ ∉ (↑s : Set α)), False
⊢ (∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) ↔ 2 * #s = Fintype.card α
have refine₁₀ : ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (ha : ⊥ ∉ (↑s : Set α) ∧ ⊥ᶜ ∉ (↑s : Set α))
  (this : s ⊆ {⊤} → s = {⊤}), False
Tactic: classical
    refine ⟨fun h ↦ ?_, fun h t ht hst ↦ Finset.eq_of_subset_of_card_le hst <|
      Nat.le_of_mul_le_mul_left (ht.card_le.trans_eq h.symm) Nat.two_pos⟩
    suffices s.disjUnion (s.map ⟨compl, compl_injective⟩) hs.disjoint_map_compl = Finset.univ by
      rw [Fintype.card, ← this, Nat.two_mul, card_disjUnion, card_map]
    rw [← coe_eq_univ, disjUnion_eq_union, coe_union, coe_map, Function.Embedding.coeFn_mk,
      image_eq_preimage_of_inverse compl_compl compl_compl]
    refine eq_univ_of_forall fun a => ?_
    simp_rw [mem_union, mem_preimage]
    by_contra! ha
    refine s.ne_insert_of_notMem _ ha.1 (h _ ?_ <| s.subset_insert _)
    rw [coe_insert]
    refine hs.insert ?_ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb
    rintro rfl
    have := h {⊤} (by rw [coe_singleton]; exact intersecting_singleton.2 top_ne_bot)
    rw [compl_bot] at ha
    rw [coe_eq_empty.1 ((hs.isUpperSet' h).top_notMem.1 ha.2)] at this
    exact Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
refine : ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t), 2 * #s = Fintype.card α
refine₁ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t),
    s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯ = Finset.univ
refine₂ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t), (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α) = univ
refine₃ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α), a ∈ (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α)
refine₄ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α), a ∈ (↑s : Set α) ∨ aᶜ ∈ (↑s : Set α)
refine₅ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), False
refine₆ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), (↑(insert a s) : Set α).Intersecting
refine₇ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), (insert a (↑s : Set α)).Intersecting
refine₈ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (a : α)
    (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), a ≠ ⊥
refine₉ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (ha : ⊥ ∉ (↑s : Set α) ∧ ⊥ᶜ ∉ (↑s : Set α)), False
refine₁₀ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (ha : ⊥ ∉ (↑s : Set α) ∧ ⊥ᶜ ∉ (↑s : Set α))
    (this : s ⊆ {⊤} → s = {⊤}), False
⊢ (∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) ↔ 2 * #s = Fintype.card α
have refine₁₁ : ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (ha : ⊥ ∉ (↑s : Set α) ∧ ⊤ ∉ (↑s : Set α))
  (this : s ⊆ {⊤} → s = {⊤}), False
Tactic: classical
    refine ⟨fun h ↦ ?_, fun h t ht hst ↦ Finset.eq_of_subset_of_card_le hst <|
      Nat.le_of_mul_le_mul_left (ht.card_le.trans_eq h.symm) Nat.two_pos⟩
    suffices s.disjUnion (s.map ⟨compl, compl_injective⟩) hs.disjoint_map_compl = Finset.univ by
      rw [Fintype.card, ← this, Nat.two_mul, card_disjUnion, card_map]
    rw [← coe_eq_univ, disjUnion_eq_union, coe_union, coe_map, Function.Embedding.coeFn_mk,
      image_eq_preimage_of_inverse compl_compl compl_compl]
    refine eq_univ_of_forall fun a => ?_
    simp_rw [mem_union, mem_preimage]
    by_contra! ha
    refine s.ne_insert_of_notMem _ ha.1 (h _ ?_ <| s.subset_insert _)
    rw [coe_insert]
    refine hs.insert ?_ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb
    rintro rfl
    have := h {⊤} (by rw [coe_singleton]; exact intersecting_singleton.2 top_ne_bot)
    rw [compl_bot] at ha
    rw [coe_eq_empty.1 ((hs.isUpperSet' h).top_notMem.1 ha.2)] at this
    exact Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (hypothesis)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
⊢ ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
have this : 2 * #s ≤ Fintype.card α
Tactic: have := hs.card_le
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (hypothesis)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
this : 2 * #s ≤ Fintype.card α
⊢ ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
have this₁ : #s ≤ Fintype.card α / 2
Tactic: rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le Nat.two_pos] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
this : #s ≤ Fintype.card α / 2
⊢ ∀ (hs : (↑s : Set α).Intersecting), ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
have refine : ∀ (t₁ : Finset α),
  (∀ {t₂ : Finset α},
      #t₂ ≤ Fintype.card α / 2 →
        t₁ ⊂ t₂ →
          ∀ (hs : (↑t₂ : Set α).Intersecting),
            ∃ (t : Finset α), t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting) →
    #t₁ ≤ Fintype.card α / 2 →
      ∀ (hs : (↑t₁ : Set α).Intersecting),
        ∃ (t : Finset α), t₁ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
Tactic: refine s.strongDownwardInductionOn ?_ this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s_1 : Finset α
this : #s_1 ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ →
        ∀ (hs : (↑t₂ : Set α).Intersecting),
          ∃ (t : Finset α), t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s : Set α).Intersecting
⊢ ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
have pos : ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t),
  ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
Tactic: by_cases! h : ∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s_1 : Finset α
this : #s_1 ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ →
        ∀ (hs : (↑t₂ : Set α).Intersecting),
          ∃ (t : Finset α), t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s : Set α).Intersecting
pos :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t),
    ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
⊢ ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
have neg : ∀ (h : ∃ (t : Finset α), (↑t : Set α).Intersecting ∧ s ⊆ t ∧ s ≠ t),
  ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
Tactic: by_cases! h : ∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s_1 : Finset α
this : #s_1 ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ →
        ∀ (hs : (↑t₂ : Set α).Intersecting),
          ∃ (t : Finset α), t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s : Set α).Intersecting
h : ∃ (t : Finset α), (↑t : Set α).Intersecting ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
have neg : ∀ (t : Finset α) (ht : (↑t : Set α).Intersecting) (hst : s ⊆ t ∧ s ≠ t),
  ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
Tactic: obtain ⟨t, ht, hst⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s_1 : Finset α
this : #s_1 ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ →
        ∀ (hs : (↑t₂ : Set α).Intersecting),
          ∃ (t : Finset α), t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s : Set α).Intersecting
t : Finset α
ht : (↑t : Set α).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
have neg : #t ≤ Fintype.card α / 2
Tactic: refine (ih ?_ (_root_.ssubset_iff_subset_ne.2 hst) ht).imp fun u => And.imp_left hst.1.trans
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s_1 : Finset α
this : #s_1 ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ →
        ∀ (hs : (↑t₂ : Set α).Intersecting),
          ∃ (t : Finset α), t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s : Set α).Intersecting
t : Finset α
ht : (↑t : Set α).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ #t ≤ Fintype.card α / 2
have neg : 2 * #t ≤ Fintype.card α
Tactic: rw [Nat.le_div_iff_mul_le Nat.two_pos, Nat.mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
L L' : Set ℕ
α : Type u_1
inst : DecidableEq α
𝒜 : Set (Finset α)
h : L ⊆ L'
hL : L.IsIntersectingOf 𝒜
⊢ L'.IsIntersectingOf 𝒜
have tauto : ∀ ⦃x : Finset α⦄, x ∈ 𝒜 → ∀ ⦃y : Finset α⦄, y ∈ 𝒜 → x ≠ y → (fun (s t : Finset α) ↦ #(s ∩ t) ∈ L') x y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Intersecting (goal)
Goal:
L : Set ℕ
α : Type u_1
inst : DecidableEq α
⊢ IsIntersectingOf.{u_1} (α := α) L ∅
have tauto : ∀ ⦃x : Finset α⦄,
  Membership.mem (γ := Set (Finset α)) ∅ x →
    ∀ ⦃y : Finset α⦄, Membership.mem (γ := Set (Finset α)) ∅ y → x ≠ y → (fun (s t : Finset α) ↦ #(s ∩ t) ∈ L) x y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
⊢ #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
have have : ∀ (this : DecidableEq ι),
  #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
Tactic: have : DecidableEq ι := by
    classical
    infer_instance
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
⊢ #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
have inl : ∀ (hs : Fintype.card α ≤ #s),
  #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
Tactic: obtain hs | hs := le_total (Fintype.card α) #s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
inl :
  ∀ (hs : Fintype.card α ≤ #s),
    #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
⊢ #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
have inr : ∀ (hs : #s ≤ Fintype.card α),
  #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
Tactic: obtain hs | hs := le_total (Fintype.card α) #s
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - HPow.hPow (α := ℕ) 2 (Fintype.card α - #s)
have inl : #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
Tactic: rw [tsub_eq_zero_of_le hs, pow_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ #(s.biUnion f) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
have inl : card (α := Finset α) {⊥}ᶜ = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
Tactic: refine (card_le_card <| biUnion_subset.2 fun i hi a ha ↦
      mem_compl.2 <| notMem_singleton.2 <| (hf _ hi).ne_bot ha).trans_eq ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
⊢ card (α := Finset α) {⊥}ᶜ = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
have inl : Fintype.card.{u_2} (Finset α) - card (α := Finset α) {⊥} = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
Tactic: rw [card_compl, Fintype.card_finset, card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
inl : Fintype.card.{u_2} (Finset α) - card (α := Finset α) {⊥} = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
⊢ card (α := Finset α) {⊥}ᶜ = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
have inl₁ : HPow.hPow (α := ℕ) 2 (Fintype.card α) - card (α := Finset α) {⊥} = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
Tactic: rw [card_compl, Fintype.card_finset, card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i) : Set (Finset α)).Intersecting
this : DecidableEq ι
hs : Fintype.card α ≤ #s
inl : Fintype.card.{u_2} (Finset α) - card (α := Finset α) {⊥} = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
inl₁ : HPow.hPow (α := ℕ) 2 (Fintype.card α) - card (α := Finset α) {⊥} = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
⊢ card (α := Finset α) {⊥}ᶜ = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
have inl₂ : HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1 = HPow.hPow (α := ℕ) 2 (Fintype.card α) - 1
Tactic: rw [card_compl, Fintype.card_finset, card_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.Kleitman (goal)
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 ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆ f' j ∧ 2 * #(f' j) = HPow.hPow (α := ℕ) 2 (Fintype.card α) ∧ (↑(f' j) : Set (Finset α)).Intersecting
have simp_rw : f j ⊆
    Exists.choose (p := fun (t : Finset (Finset α)) ↦
      f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) sorry ∧
  2 *
        card.{u_2} (α := Finset α)
          (Exists.choose (p := fun (t : Finset (Finset α)) ↦
            f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) sorry) =
      Fintype.card.{u_2} (Finset α) ∧
    (↑(Exists.choose (p := fun (t : Finset (Finset α)) ↦
            f j ⊆ t ∧ 2 * #t = Fintype.card.{u_2} (Finset α) ∧ (↑t : Set (Finset α)).Intersecting) sorry) :
        Set (Finset α)).Intersecting
Tactic: simp_rw [f', dif_pos hj, ← Fintype.card_finset]