awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ (↑s : Set α)
⊢ b ∈ (↑(insert b s) : Set α)

Tactic:
exact mem_insert_self _ _

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ (↑s : Set α)
rw : (insert b (↑s : Set α)).Intersecting
⊢ (↑(insert b s) : Set α).Intersecting

Tactic:
rw [coe_insert]

Premises used: Finset.coe_insert
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ (↑s : Set α)
⊢ (insert b (↑s : Set α)).Intersecting

Tactic:
hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab

Premises used: Set.Intersecting.ne_bot, mt, Disjoint.mono_left, eq_bot_mono, Set.Intersecting.insert
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ (↑s : Set α)
⊢ (insert b (↑s : Set α)).Intersecting

Tactic:
exact
      hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab

Premises used: Set.Intersecting.ne_bot, mt, Disjoint.mono_left, eq_bot_mono, Set.Intersecting.insert
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
rintro : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), b ∈ (↑s : Set α)
rintro₁ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), b ∈ (↑(insert b s) : Set α)
rintro₂ rintro₃ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), (↑(insert b s) : Set α).Intersecting
rintro₄ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ (↑s : Set α)), (insert b (↑s : Set α)).Intersecting
⊢ IsUpperSet (↑s : Set α)

Tactic:
classical
    rintro a b hab ha
    rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
    · exact mem_insert_self _ _
    rw [coe_insert]
    exact
      hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab

Premises used: Finset.mem_insert_self, Finset.coe_insert
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
𝒜 : Set (Set α)
h𝒜 : 𝒜.Intersecting
s t : Set α
hs : s ∈ 𝒜
ht : t ∈ 𝒜
⊢ ∃ a ∈ s, a ∈ t

Tactic:
not_disjoint_iff.1 <| h𝒜 hs ht

Premises used: Set.not_disjoint_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 : Set (Finset α)
h𝒜 : 𝒜.Intersecting
s t : Finset α
hs : s ∈ 𝒜
ht : t ∈ 𝒜
⊢ ∃ a ∈ s, a ∈ t

Tactic:
not_disjoint_iff.1 <| disjoint_coe.not.2 <| h𝒜 hs ht

Premises used: Iff.mpr, Finset.disjoint_coe, Iff.not, Set.not_disjoint_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Set α
hs : s.Intersecting
a : α
ha : a ∈ s
⊢ aᶜ ∉ s

Tactic:
fun h => hs ha h disjoint_compl_right

Premises used: disjoint_compl_right, Not
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Set α
hs : s.Intersecting
a : α
ha : aᶜ ∈ s
⊢ a ∉ s

Tactic:
fun h => hs ha h disjoint_compl_left

Premises used: disjoint_compl_left, Not
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Finset α
hs : (↑s : Set α).Intersecting
rw : ∀ ⦃a : α⦄, a ∈ s → a ∉ map { toFun := compl, inj' := ⋯ : α ↪ α } s
⊢ Disjoint s (map { toFun := compl, inj' := ⋯ } s)

Tactic:
rw [Finset.disjoint_left]

Premises used: Finset.disjoint_left
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Finset α
hs : (↑s : Set α).Intersecting
x : α
hx : x ∈ s
hxc : x ∈ map { toFun := compl, inj' := ⋯ : α ↪ α } s
obtain :
  ∀ (x : α) (hx' : x ∈ s) (hx : Membership.mem (α := α) s (({ toFun := compl, inj' := ⋯ } : (a : α) → α) x : α))
    (hxc :
      Membership.mem (α := α) (map { toFun := compl, inj' := ⋯ : α ↪ α } s)
        (({ toFun := compl, inj' := ⋯ } : (a : α) → α) x : α)),
    False
⊢ False

Tactic:
obtain ⟨x, hx', rfl⟩ := mem_map.mp hxc

Premises used: Iff.mp, Finset.mem_map, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Finset α
hs : (↑s : Set α).Intersecting
x : α
hx' : x ∈ s
hx : Membership.mem (α := α) s (({ toFun := compl, inj' := ⋯ } : (a : α) → α) x : α)
hxc :
  Membership.mem (α := α) (map { toFun := compl, inj' := ⋯ : α ↪ α } s)
    (({ toFun := compl, inj' := ⋯ } : (a : α) → α) x : α)
⊢ False

Tactic:
hs.compl_notMem hx' hx

Premises used: Set.Intersecting.compl_notMem
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Finset α
hs : (↑s : Set α).Intersecting
x : α
hx' : x ∈ s
hx : Membership.mem (α := α) s (({ toFun := compl, inj' := ⋯ } : (a : α) → α) x : α)
hxc :
  Membership.mem (α := α) (map { toFun := compl, inj' := ⋯ : α ↪ α } s)
    (({ toFun := compl, inj' := ⋯ } : (a : α) → α) x : α)
⊢ False

Tactic:
exact hs.compl_notMem hx' hx

Premises used: Set.Intersecting.compl_notMem
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
⊢ 2 * #s ≤ Fintype.card α

Tactic:
(s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' ?_

Premises used: LE.le.trans_eq', Set.Intersecting.disjoint_map_compl, Finset.disjUnion, Finset.card_le_univ
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
refine : #(s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯) = 2 * #s
⊢ 2 * #s ≤ Fintype.card α

Tactic:
refine (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' ?_

Premises used: LE.le.trans_eq', Set.Intersecting.disjoint_map_compl, Finset.disjUnion, Finset.card_le_univ
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
rw : #(s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯) = #s + #s
rw₁ : #s + #(map { toFun := compl, inj' := ⋯ : α ↪ α } s) = #s + #s
rw₂ rw₃ : #s + #s = #s + #s
⊢ #(s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯) = 2 * #s

Tactic:
rw [Nat.two_mul, card_disjUnion, card_map]

Premises used: Finset.card_map, Finset.card_disjUnion, Nat.two_mul
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
refine : #(s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯) = 2 * #s
⊢ 2 * #s ≤ Fintype.card α

Tactic:
classical
    refine (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' ?_
    rw [Nat.two_mul, card_disjUnion, card_map]

Premises used: Finset.card_map, LE.le.trans_eq', Set.Intersecting.disjoint_map_compl, Finset.disjUnion, Finset.card_le_univ, Finset.card_disjUnion, Nat.two_mul
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
⊢ (∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) ↔ 2 * #s = Fintype.card α

Tactic:
⟨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⟩

Premises used: LE.le.trans_eq, Nat.two_pos, Nat.le_of_mul_le_mul_left, Iff.intro, Finset.eq_of_subset_of_card_le, Eq.symm, Set.Intersecting.card_le
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
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 α
⊢ (∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) ↔ 2 * #s = Fintype.card α

Tactic:
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⟩
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
this : s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯ = Finset.univ
rw : 2 * #s = card.{u_1} (α := α) Finset.univ
rw₁ : 2 * #s = #(s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯)
rw₂ : #s + #s = #(s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯)
rw₃ : #s + #s = #s + #(map { toFun := compl, inj' := ⋯ : α ↪ α } s)
rw₄ rw₅ : #s + #s = #s + #s
⊢ 2 * #s = Fintype.card α

Tactic:
rw [Fintype.card, ← this, Nat.two_mul, card_disjUnion, card_map]

Premises used: Finset.card_map, Fintype.card, Finset.card_disjUnion, Nat.two_mul
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
suffices : s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯ = Finset.univ
⊢ 2 * #s = Fintype.card α

Tactic:
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]
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
rw : (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α) = univ
⊢ s.disjUnion (map { toFun := compl, inj' := ⋯ : α ↪ α } s) ⋯ = Finset.univ

Tactic:
rw [← coe_eq_univ, disjUnion_eq_union, coe_union, coe_map, Function.Embedding.coeFn_mk,
      image_eq_preimage_of_inverse compl_compl compl_compl]

Premises used: compl_compl, Finset.coe_eq_univ, Set.image_eq_preimage_of_inverse, Function.Embedding.coeFn_mk, Finset.coe_map, Finset.disjUnion_eq_union, Finset.coe_union
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
⊢ (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α) = univ

Tactic:
eq_univ_of_forall fun a => ?_

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
refine : ∀ (a : α), a ∈ (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α)
⊢ (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α) = univ

Tactic:
refine eq_univ_of_forall fun a => ?_

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a : α
simp_rw : a ∈ (↑s : Set α) ∨ aᶜ ∈ (↑s : Set α)
⊢ a ∈ (↑s : Set α) ∪ compl ⁻¹' (↑s : Set α)

Tactic:
simp_rw [mem_union, mem_preimage]

Premises used: Set.mem_union, Set.mem_preimage
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a : α
by_contra! : ∀ (ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)), False
⊢ a ∈ (↑s : Set α) ∨ aᶜ ∈ (↑s : Set α)

Tactic:
by_contra! ha
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)
⊢ False

Tactic:
s.ne_insert_of_notMem _ ha.1 (h _ ?_ <| s.subset_insert _)

Premises used: Finset.ne_insert_of_notMem, And.left, Finset.subset_insert
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)
refine : (↑(insert a s) : Set α).Intersecting
⊢ False

Tactic:
refine s.ne_insert_of_notMem _ ha.1 (h _ ?_ <| s.subset_insert _)

Premises used: Finset.ne_insert_of_notMem, And.left, Finset.subset_insert
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)
rw : (insert a (↑s : Set α)).Intersecting
⊢ (↑(insert a s) : Set α).Intersecting

Tactic:
rw [coe_insert]

Premises used: Finset.coe_insert
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)
⊢ (insert a (↑s : Set α)).Intersecting

Tactic:
hs.insert ?_ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb

Premises used: Set.Intersecting.isUpperSet', And.right, Disjoint.le_compl_left, Set.Intersecting.insert
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ (↑s : Set α) ∧ aᶜ ∉ (↑s : Set α)
refine : a ≠ ⊥
⊢ (insert a (↑s : Set α)).Intersecting

Tactic:
refine hs.insert ?_ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb

Premises used: Set.Intersecting.isUpperSet', And.right, Disjoint.le_compl_left, Set.Intersecting.insert
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
ha : ⊥ ∉ (↑s : Set α) ∧ ⊥ᶜ ∉ (↑s : Set α)
rw : Intersecting (α := α) {⊤}
⊢ (↑{⊤} : Set α).Intersecting

Tactic:
rw [coe_singleton]

Premises used: Finset.coe_singleton
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
ha : ⊥ ∉ (↑s : Set α) ∧ ⊥ᶜ ∉ (↑s : Set α)
⊢ Intersecting (α := α) {⊤}

Tactic:
intersecting_singleton.2 top_ne_bot

Premises used: Iff.mpr, top_ne_bot, Set.intersecting_singleton
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
ha : ⊥ ∉ (↑s : Set α) ∧ ⊥ᶜ ∉ (↑s : Set α)
⊢ Intersecting (α := α) {⊤}

Tactic:
exact intersecting_singleton.2 top_ne_bot

Premises used: Iff.mpr, top_ne_bot, Set.intersecting_singleton
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
ha : ⊥ ∉ (↑s : Set α) ∧ ⊥ᶜ ∉ (↑s : Set α)
⊢ s ⊆ {⊤} → s = {⊤}

Tactic:
have := h {⊤} (by rw [coe_singleton]; exact intersecting_singleton.2 top_ne_bot)
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
ha : ⊥ ∉ (↑s : Set α) ∧ ⊥ᶜ ∉ (↑s : Set α)
this : s ⊆ {⊤} → s = {⊤}
⊢ ⊥ ∉ (↑s : Set α) ∧ ⊤ ∉ (↑s : Set α)

Tactic:
rw [compl_bot] at ha

Premises used: compl_bot
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
ha : ⊥ ∉ (↑s : Set α) ∧ ⊥ᶜ ∉ (↑s : Set α)
this : s ⊆ {⊤} → s = {⊤}
ha₁ : ⊥ ∉ (↑s : Set α) ∧ ⊤ ∉ (↑s : Set α)
⊢ s ⊆ {⊤} → s = {⊤}

Tactic:
rw [compl_bot] at ha

Premises used: compl_bot
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
ha : ⊥ ∉ (↑s : Set α) ∧ ⊤ ∉ (↑s : Set α)
this : s ⊆ {⊤} → s = {⊤}
⊢ Subset (α := Finset α) ∅ {⊤} → Eq (α := Finset α) ∅ {⊤}

Tactic:
rw [coe_eq_empty.1 ((hs.isUpperSet' h).top_notMem.1 ha.2)] at this

Premises used: Finset.coe_eq_empty, Set.Intersecting.isUpperSet', IsUpperSet.top_notMem, And.right, Iff.mp
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
ha : ⊥ ∉ (↑s : Set α) ∧ ⊤ ∉ (↑s : Set α)
this : Subset (α := Finset α) ∅ {⊤} → Eq (α := Finset α) ∅ {⊤}
⊢ False

Tactic:
Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm

Premises used: Finset.singleton_ne_empty, Finset.empty_subset, Eq.symm
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t
ha : ⊥ ∉ (↑s : Set α) ∧ ⊤ ∉ (↑s : Set α)
this : Subset (α := Finset α) ∅ {⊤} → Eq (α := Finset α) ∅ {⊤}
⊢ False

Tactic:
exact Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm

Premises used: Finset.singleton_ne_empty, Finset.empty_subset, Eq.symm
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
⊢ 2 * #s ≤ Fintype.card α

Tactic:
have := hs.card_le
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
this : 2 * #s ≤ Fintype.card α
⊢ #s ≤ Fintype.card α / 2

Tactic:
rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le Nat.two_pos] at this

Premises used: Nat.two_pos, Nat.mul_comm, Nat.le_div_iff_mul_le
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
hs : (↑s : Set α).Intersecting
this : #s ≤ Fintype.card α / 2
revert :
  ∀ (hs : (↑s : Set α).Intersecting), ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting
⊢ ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting

Tactic:
revert hs
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
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

Tactic:
s.strongDownwardInductionOn ?_ this

Premises used: Finset.strongDownwardInductionOn
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : BooleanAlgebra α
inst_1 : Nontrivial α
inst_2 : Fintype α
s : Finset α
this : #s ≤ Fintype.card α / 2
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
⊢ ∀ (hs : (↑s : Set α).Intersecting), ∃ (t : Finset α), s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t : Set α).Intersecting

Tactic:
refine s.strongDownwardInductionOn ?_ this
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
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
neg :
  ∀ (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

Tactic:
by_cases! h : ∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
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

Tactic:
⟨s, Subset.rfl, hs.is_max_iff_card_eq.1 h, hs⟩

Premises used: Set.Intersecting.is_max_iff_card_eq, Set.Subset.rfl, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
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

Tactic:
exact ⟨s, Subset.rfl, hs.is_max_iff_card_eq.1 h, hs⟩
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
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
neg :
  ∀ (t : Finset α) (ht : (↑t : Set α).Intersecting) (hst : 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

Tactic:
obtain ⟨t, ht, hst⟩ := h