awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))) (hℬ : IsLowerSet (↑ℬ : Set (Finset α)))
    (h𝒜s : ∀ t ∈ 𝒜, t ⊆ s) (hℬs : ∀ t ∈ ℬ, t ⊆ s), #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜s : ∀ t ∈ 𝒜, t ⊆ Insert.insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ Insert.insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ Insert.insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ Insert.insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
insert :
  HPow.hPow (α := ℕ) 2 #s *
      (#(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ)) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
insert₁ :
  HPow.hPow (α := ℕ) 2 #s *
      (#(Finset.memberSubfamily a (𝒜 ∩ ℬ)) + #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ)) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
insert₂ :
  HPow.hPow (α := ℕ) 2 #s * (#(Finset.memberSubfamily a (𝒜 ∩ ℬ)) + #(Finset.nonMemberSubfamily a (𝒜 ∩ ℬ))) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
insert₃ insert₄ : HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ) = HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)
⊢ HPow.hPow (α := ℕ) 2 #s * #(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
      HPow.hPow (α := ℕ) 2 #s * #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ) =
    HPow.hPow (α := ℕ) 2 #s * #(𝒜 ∩ ℬ)

Tactic:
rw [← mul_add, ← memberSubfamily_inter, ← nonMemberSubfamily_inter,
    card_memberSubfamily_add_card_nonMemberSubfamily]

Premises used: Finset.card_memberSubfamily_add_card_nonMemberSubfamily, Finset.nonMemberSubfamily_inter, Finset.memberSubfamily_inter, mul_add
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ)

Tactic:
h𝒜.le_card_inter_finset' hℬ (fun _ _ => subset_univ _) fun _ _ => subset_univ _

Premises used: IsLowerSet.le_card_inter_finset', Fintype.card, Finset.subset_univ
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsUpperSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
⊢ IsLowerSet (↑𝒜ᶜ : Set (Finset α))

Tactic:
rw [← isLowerSet_compl, ← coe_compl] at h𝒜

Premises used: Finset.coe_compl, isLowerSet_compl
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsUpperSet (↑𝒜 : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
h𝒜₁ : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
⊢ IsLowerSet (↑ℬ : Set (Finset α))

Tactic:
rw [← isLowerSet_compl, ← coe_compl] at h𝒜

Premises used: Finset.coe_compl, isLowerSet_compl
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
⊢ #𝒜ᶜ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)

Tactic:
have := h𝒜.le_card_inter_finset hℬ
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsLowerSet (↑ℬ : Set (Finset α))
this : #𝒜ᶜ * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)
rwa :
  ∀ (this : (Fintype.card.{u_1} (Finset α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₁ :
  ∀ (this : (HPow.hPow (α := ℕ) 2 (Fintype.card α) - #𝒜) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₂ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ)),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₃ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₄ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * (#ℬ - #(𝒜ᶜ ∩ ℬ)) ≤ #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₅ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(ℬ \ (𝒜ᶜ ∩ ℬ)) ≤ #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₆ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(ℬ \ 𝒜ᶜ) ≤ #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₇ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(ℬ ⊓ 𝒜) ≤ #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
rwa₈ rwa₉ rwa₁₀ rwa₁₁ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ⊓ ℬ) ≤ #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Tactic:
rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this

Premises used: Finset.inter_subset_right, Finset.card_compl, Finset.card_sdiff_of_subset, inf_comm, Fintype.card_finset, Finset.sdiff_inter_self_right, sdiff_compl, tsub_le_iff_tsub_le, tsub_mul, mul_tsub
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsUpperSet (↑ℬ : Set (Finset α))
rw : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(ℬ ∩ 𝒜) ≤ #ℬ * #𝒜
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Tactic:
rw [inter_comm, mul_comm #𝒜]

Premises used: Finset.inter_comm, mul_comm, Finset.card
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsUpperSet (↑ℬ : Set (Finset α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(ℬ ∩ 𝒜) ≤ #ℬ * #𝒜

Tactic:
hℬ.card_inter_le_finset h𝒜

Premises used: IsUpperSet.card_inter_le_finset
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜 : Set (Finset α))
hℬ : IsUpperSet (↑ℬ : Set (Finset α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(ℬ ∩ 𝒜) ≤ #ℬ * #𝒜

Tactic:
exact hℬ.card_inter_le_finset h𝒜

Premises used: IsUpperSet.card_inter_le_finset
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsUpperSet (↑𝒜 : Set (Finset α))
hℬ : IsUpperSet (↑ℬ : Set (Finset α))
⊢ IsLowerSet (↑𝒜ᶜ : Set (Finset α))

Tactic:
rw [← isLowerSet_compl, ← coe_compl] at h𝒜

Premises used: Finset.coe_compl, isLowerSet_compl
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsUpperSet (↑𝒜 : Set (Finset α))
hℬ : IsUpperSet (↑ℬ : Set (Finset α))
h𝒜₁ : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
⊢ IsUpperSet (↑ℬ : Set (Finset α))

Tactic:
rw [← isLowerSet_compl, ← coe_compl] at h𝒜

Premises used: Finset.coe_compl, isLowerSet_compl
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsUpperSet (↑ℬ : Set (Finset α))
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜ᶜ * #ℬ

Tactic:
have := h𝒜.card_inter_le_finset hℬ
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsUpperSet (↑ℬ : Set (Finset α))
this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜ᶜ * #ℬ
h₁ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ),
    HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ
h₂ :
  ∀ (this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ),
    #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜 ∩ ℬ)

Tactic:
rwa [card_compl, Fintype.card_finset, tsub_mul, le_tsub_iff_le_tsub, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this

Premises used: Finset.inter_subset_right, Finset.card_compl, Finset.card_sdiff_of_subset, le_tsub_iff_le_tsub, inf_comm, Fintype.card_finset, Finset.sdiff_inter_self_right, sdiff_compl, tsub_mul, mul_tsub
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsUpperSet (↑ℬ : Set (Finset α))
this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ
h₁ h₂ : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ
⊢ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ

Tactic:
grw [inter_subset_right]

Premises used: Finset.inter_subset_right
-- Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman
Goal:
α : Type u_1
inst : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst_1 : Fintype α
h𝒜 : IsLowerSet (↑𝒜ᶜ : Set (Finset α))
hℬ : IsUpperSet (↑ℬ : Set (Finset α))
this : HPow.hPow (α := ℕ) 2 (Fintype.card α) * #(𝒜ᶜ ∩ ℬ) ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ - #𝒜 * #ℬ
h₂ : #𝒜 * #ℬ ≤ Fintype.card.{u_1} (Finset α) * #ℬ
h₃ h₄ : Fintype.card.{u_1} (Finset α) * #ℬ ≤ Fintype.card.{u_1} (Finset α) * #ℬ
⊢ #𝒜 * #ℬ ≤ HPow.hPow (α := ℕ) 2 (Fintype.card α) * #ℬ

Tactic:
grw [← Fintype.card_finset, card_le_univ]

Premises used: Fintype.card_finset, Finset.card_le_univ
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s t : Set α
h : t ⊆ s
hs : s.Intersecting
⊢ t.Intersecting

Tactic:
fun _a ha _b hb =>
  hs (h ha) (h hb)

Premises used: Set.Intersecting
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
⊢ ⊥ ∉ s

Tactic:
fun h => hs h h disjoint_bot_left

Premises used: disjoint_bot_left, Not
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
a : α
hs : s.Intersecting
ha : a ∈ s
⊢ a ≠ ⊥

Tactic:
ne_of_mem_of_not_mem ha hs.bot_notMem

Premises used: ne_of_mem_of_not_mem, Set.Intersecting.bot_notMem
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
⊢ Intersecting.{u_1} (α := α) ∅

Tactic:
fun _ => False.elim

Premises used: Set.Mem, Set.Intersecting, False.elim
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
a : α
⊢ Intersecting (α := α) {a} ↔ a ≠ ⊥

Tactic:
simp [Intersecting]

Premises used: Set.Intersecting
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
inl inl₁ inl₂ inl₃ : ¬c = ⊥
⊢ ¬Disjoint c c

Tactic:
rwa [disjoint_self]

Premises used: disjoint_self
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
b : α
ha : b ≠ ⊥
h : ∀ b_1 ∈ s, ¬Disjoint b b_1
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

Tactic:
h _ hc
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
b : α
ha : b ≠ ⊥
h : ∀ b_1 ∈ s, ¬Disjoint b b_1
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

Tactic:
exact h _ hc
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
b : α
hb : b ∈ s
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint b c

Tactic:
fun H => h _ hb H.symm

Premises used: Disjoint.symm, Not
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
b : α
hb : b ∈ s
c : α
ha : c ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint c b
⊢ ¬Disjoint b c

Tactic:
exact fun H => h _ hb H.symm
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
a : α
hs : s.Intersecting
ha : a ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

Tactic:
hs hb hc
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
a : α
hs : s.Intersecting
ha : a ≠ ⊥
h : ∀ b ∈ s, ¬Disjoint a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

Tactic:
exact hs hb hc
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
a : α
⊢ (insert a s).Intersecting ↔ s.Intersecting ∧ a ≠ ⊥ ∧ ∀ b ∈ s, ¬Disjoint a b

Tactic:
⟨fun h =>
    ⟨h.mono <| subset_insert _ _, h.ne_bot <| mem_insert _ _, fun _b hb =>
      h (mem_insert _ _) <| mem_insert_of_mem _ hb⟩,
    fun h => h.1.insert h.2.1 h.2.2⟩

Premises used: Set.Intersecting.ne_bot, Set.mem_insert_of_mem, And.right, And.left, And.intro, Iff.intro, Set.mem_insert, Set.Intersecting.mono, Set.subset_insert, Set.Intersecting.insert
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
⊢ s.Intersecting ↔ (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}

Tactic:
⟨fun h => ⟨fun a ha b hb _ => h ha hb, ?_⟩, fun h a ha b hb hab => ?_⟩

Premises used: And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
refine_1 : ∀ (h : s.Intersecting), s ≠ {⊥}
refine_2 :
  ∀ (h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s)
    (hab : Disjoint a b), False
⊢ s.Intersecting ↔ (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}

Tactic:
refine ⟨fun h => ⟨fun a ha b hb _ => h ha hb, ?_⟩, fun h a ha b hb hab => ?_⟩
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
h : Intersecting (α := α) {⊥}
⊢ False

Tactic:
intersecting_singleton.1 h rfl

Premises used: Iff.mp, Set.intersecting_singleton, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
h : Intersecting (α := α) {⊥}
⊢ False

Tactic:
exact intersecting_singleton.1 h rfl

Premises used: Iff.mp, Set.intersecting_singleton, rfl
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
⊢ a = b

Tactic:
have := h.1.eq ha hb (Classical.not_not.2 hab)
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
this : a = b
⊢ b = ⊥

Tactic:
rw [this, disjoint_self] at hab

Premises used: disjoint_self
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
this : a = b
hab₁ : b = ⊥
⊢ a = b

Tactic:
rw [this, disjoint_self] at hab

Premises used: disjoint_self
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : b = ⊥
this : a = b
⊢ ⊥ ∈ s

Tactic:
rw [hab] at hb
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : b = ⊥
this : a = b
hb₁ : ⊥ ∈ s
⊢ b = ⊥

Tactic:
rw [hab] at hb
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : b = ⊥
this : a = b
hb₁ : ⊥ ∈ s
hab₁ : b = ⊥
⊢ a = b

Tactic:
rw [hab] at hb
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : ⊥ ∈ s
hab : b = ⊥
this : a = b
⊢ False

Tactic:
h.2
      (eq_singleton_iff_unique_mem.2
        ⟨hb, fun c hc => not_ne_iff.1 fun H => h.1 hb hc H.symm disjoint_bot_left⟩)

Premises used: Iff.mpr, disjoint_bot_left, Ne.symm, not_ne_iff, And.right, And.left, And.intro, Iff.mp, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
h : (s.Pairwise fun (a b : α) ↦ ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : ⊥ ∈ s
hab : b = ⊥
this : a = b
⊢ False

Tactic:
exact
    h.2
      (eq_singleton_iff_unique_mem.2
        ⟨hb, fun c hc => not_ne_iff.1 fun H => h.1 hb hc H.symm disjoint_bot_left⟩)

Premises used: Iff.mpr, disjoint_bot_left, Ne.symm, not_ne_iff, And.right, And.left, And.intro, Iff.mp, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Subsingleton
⊢ s.Intersecting ↔ s ≠ {⊥}

Tactic:
intersecting_iff_pairwise_not_disjoint.trans <| and_iff_right <| hs.pairwise _

Premises used: and_iff_right, Set.Subsingleton.pairwise, Set.intersecting_iff_pairwise_not_disjoint, Iff.trans
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : Subsingleton α
s : Set α
⊢ s.Intersecting ↔ s = ∅

Tactic:
subsingleton_of_subsingleton.intersecting.trans
      ⟨not_imp_comm.2 fun h => subsingleton_of_subsingleton.eq_singleton_of_mem ?_, ?_⟩

Premises used: Iff.mpr, not_imp_comm, Set.Subsingleton.eq_singleton_of_mem, Set.subsingleton_of_subsingleton, Set.Subsingleton.intersecting, Iff.intro, Iff.trans
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : Subsingleton α
s : Set α
refine_1 : ∀ (h : ¬s = ∅), ⊥ ∈ s
refine_2 : s = ∅ → s ≠ {⊥}
⊢ s.Intersecting ↔ s = ∅

Tactic:
refine
    subsingleton_of_subsingleton.intersecting.trans
      ⟨not_imp_comm.2 fun h => subsingleton_of_subsingleton.eq_singleton_of_mem ?_, ?_⟩

Premises used: Iff.mpr, not_imp_comm, Set.Subsingleton.eq_singleton_of_mem, Set.subsingleton_of_subsingleton, Set.Subsingleton.intersecting, Iff.intro, Iff.trans
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : Subsingleton α
s : Set α
h : ¬s = ∅
refine_1 : ∀ (a : α) (ha : a ∈ s), ⊥ ∈ s
⊢ ⊥ ∈ s

Tactic:
obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 h

Premises used: Iff.mpr, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : Subsingleton α
s : Set α
h : ¬s = ∅
a : α
ha refine_1 refine_1₁ refine_1₂ refine_1₃ : a ∈ s
⊢ ⊥ ∈ s

Tactic:
rwa [Subsingleton.elim ⊥ a]

Premises used: Bot.bot, Subsingleton.elim
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : Subsingleton α
⊢ Ne (α := Set α) ∅ {⊥}

Tactic:
(Set.singleton_nonempty _).ne_empty.symm

Premises used: Set.singleton_nonempty, Set.Nonempty.ne_empty, Ne.symm
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
inst_2 : Subsingleton α
⊢ Ne (α := Set α) ∅ {⊥}

Tactic:
exact (Set.singleton_nonempty _).ne_empty.symm

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

Tactic:
rw [h (Insert.insert b s) _ (subset_insert _ _)]

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

Tactic:
mem_insert _ _

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

Tactic:
exact mem_insert _ _

Premises used: Set.mem_insert
-- Module: Mathlib.Combinatorics.SetFamily.Intersecting
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ (insert b s).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 : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ (insert b s).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 : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
rintro : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ s), b ∈ s
rintro₁ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ s), b ∈ insert b s
rintro₂ rintro₃ : ∀ ⦃a b : α⦄ (hab : a ≤ b) (ha : a ∈ s), (insert b s).Intersecting
⊢ IsUpperSet s

Tactic:
classical
    rintro a b hab ha
    rw [h (Insert.insert b s) _ (subset_insert _ _)]
    · exact mem_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: Set.mem_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 α)
rw : b ∈ (↑(insert b s) : Set α)
rw₁ : (↑(insert b s) : Set α).Intersecting
⊢ b ∈ (↑s : Set α)

Tactic:
rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]

Premises used: Insert.insert, Finset.subset_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 α)
⊢ b ∈ (↑(insert b s) : Set α)

Tactic:
mem_insert_self _ _

Premises used: Finset.mem_insert_self