[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
⊢ Intersecting {a} ↔ a ≠ ⊥
[PROOFSTEP]
simp [Intersecting]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
hs : Intersecting s
ha : a ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint a b
⊢ Intersecting (insert a s)
[PROOFSTEP]
rintro b (rfl | hb) c (rfl | hc)
[GOAL]
case inl.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
b c✝ : α
hs : Intersecting s
c : α
ha : c ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint c b
⊢ ¬Disjoint c c
[PROOFSTEP]
rwa [disjoint_self]
[GOAL]
case inl.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
b✝ c✝ : α
hs : Intersecting s
b : α
ha : b ≠ ⊥
h : ∀ (b_1 : α), b_1 ∈ s → ¬Disjoint b b_1
c : α
hc : c ∈ s
⊢ ¬Disjoint b c
[PROOFSTEP]
exact h _ hc
[GOAL]
case inr.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
b✝ c✝ : α
hs : Intersecting s
b : α
hb : b ∈ s
c : α
ha : c ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint c b
⊢ ¬Disjoint b c
[PROOFSTEP]
exact fun H => h _ hb H.symm
[GOAL]
case inr.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b✝ c✝ : α
hs : Intersecting s
ha : a ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
⊢ ¬Disjoint b c
[PROOFSTEP]
exact hs hb hc
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
⊢ Intersecting s ↔ (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
[PROOFSTEP]
refine' ⟨fun h => ⟨fun a ha b hb _ => h ha hb, _⟩, fun h a ha b hb hab => _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
h : Intersecting s
⊢ s ≠ {⊥}
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
t : Set α
a b c : α
h : Intersecting {⊥}
⊢ False
[PROOFSTEP]
exact intersecting_singleton.1 h rfl
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
⊢ False
[PROOFSTEP]
have := h.1.eq ha hb (Classical.not_not.2 hab)
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
this : a = b
⊢ False
[PROOFSTEP]
rw [this, disjoint_self] at hab 
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : b = ⊥
this : a = b
⊢ False
[PROOFSTEP]
rw [hab] at hb 
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : ⊥ ∈ s
hab : b = ⊥
this : a = b
⊢ False
[PROOFSTEP]
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⟩)
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s✝ t : Set α
a b c : α
inst✝ : Subsingleton α
s : Set α
⊢ Intersecting s ↔ s = ∅
[PROOFSTEP]
refine'
  subsingleton_of_subsingleton.intersecting.trans
    ⟨not_imp_comm.2 fun h => subsingleton_of_subsingleton.eq_singleton_of_mem _, _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s✝ t : Set α
a b c : α
inst✝ : Subsingleton α
s : Set α
h : ¬s = ∅
⊢ ⊥ ∈ s
[PROOFSTEP]
obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 h
[GOAL]
case refine'_1.intro
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s✝ t : Set α
a✝ b c : α
inst✝ : Subsingleton α
s : Set α
h : ¬s = ∅
a : α
ha : a ∈ s
⊢ ⊥ ∈ s
[PROOFSTEP]
rwa [Subsingleton.elim ⊥ a]
[GOAL]
case refine'_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s✝ t : Set α
a b c : α
inst✝ : Subsingleton α
s : Set α
⊢ s = ∅ → s ≠ {⊥}
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderBot α
s t : Set α
a b c : α
inst✝ : Subsingleton α
⊢ ∅ ≠ {⊥}
[PROOFSTEP]
exact (Set.singleton_nonempty _).ne_empty.symm
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
⊢ IsUpperSet s
[PROOFSTEP]
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
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
⊢ IsUpperSet s
[PROOFSTEP]
rintro a b hab ha
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ s
[PROOFSTEP]
rw [h (Insert.insert b s) _ (subset_insert _ _)]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ insert b s
[PROOFSTEP]
exact mem_insert _ _
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ Intersecting (insert b s)
[PROOFSTEP]
exact hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s✝ t : Set α
a b c : α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ IsUpperSet ↑s
[PROOFSTEP]
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
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s✝ t : Set α
a b c : α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ IsUpperSet ↑s
[PROOFSTEP]
rintro a b hab ha
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s✝ t : Set α
a✝ b✝ c : α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ b ∈ ↑s
[PROOFSTEP]
rw [h (Insert.insert b s) _ (Finset.subset_insert _ _)]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s✝ t : Set α
a✝ b✝ c : α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ b ∈ ↑(insert b s)
[PROOFSTEP]
exact mem_insert_self _ _
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s✝ t : Set α
a✝ b✝ c : α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ Intersecting ↑(insert b s)
[PROOFSTEP]
rw [coe_insert]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s✝ t : Set α
a✝ b✝ c : α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ Intersecting (insert b ↑s)
[PROOFSTEP]
exact hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
[GOAL]
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : Intersecting ↑s
⊢ Disjoint s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)
[PROOFSTEP]
rw [Finset.disjoint_left]
[GOAL]
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : Intersecting ↑s
⊢ ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ map { toFun := compl, inj' := (_ : Function.Injective compl) } s
[PROOFSTEP]
rintro x hx hxc
[GOAL]
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : Intersecting ↑s
x : α
hx : x ∈ s
hxc : x ∈ map { toFun := compl, inj' := (_ : Function.Injective compl) } s
⊢ False
[PROOFSTEP]
obtain ⟨x, hx', rfl⟩ := mem_map.mp hxc
[GOAL]
case intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : Intersecting ↑s
x : α
hx' : x ∈ s
hx : ↑{ toFun := compl, inj' := (_ : Function.Injective compl) } x ∈ s
hxc :
  ↑{ toFun := compl, inj' := (_ : Function.Injective compl) } x ∈
    map { toFun := compl, inj' := (_ : Function.Injective compl) } s
⊢ False
[PROOFSTEP]
exact hs.not_compl_mem hx' hx
[GOAL]
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ 2 * card s ≤ Fintype.card α
[PROOFSTEP]
classical
refine' (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' _
rw [two_mul, card_disjUnion, card_map]
[GOAL]
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ 2 * card s ≤ Fintype.card α
[PROOFSTEP]
refine' (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' _
[GOAL]
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ 2 * card s =
    card
      (disjUnion s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)
        (_ : Disjoint s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)))
[PROOFSTEP]
rw [two_mul, card_disjUnion, card_map]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ (∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t) ↔ 2 * card s = Fintype.card α
[PROOFSTEP]
classical
refine'
  ⟨fun h => _, fun h t ht hst =>
    Finset.eq_of_subset_of_card_le hst <| le_of_mul_le_mul_left (ht.card_le.trans_eq h.symm) two_pos⟩
suffices s.disjUnion (s.map ⟨compl, compl_injective⟩) hs.disjoint_map_compl = Finset.univ by
  rw [Fintype.card, ← this, 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_not_mem _ 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).not_top_mem.1 ha.2)] at this 
exact Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ (∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t) ↔ 2 * card s = Fintype.card α
[PROOFSTEP]
refine'
  ⟨fun h => _, fun h t ht hst =>
    Finset.eq_of_subset_of_card_le hst <| le_of_mul_le_mul_left (ht.card_le.trans_eq h.symm) two_pos⟩
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ 2 * card s = Fintype.card α
[PROOFSTEP]
suffices s.disjUnion (s.map ⟨compl, compl_injective⟩) hs.disjoint_map_compl = Finset.univ by
  rw [Fintype.card, ← this, two_mul, card_disjUnion, card_map]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
this :
  disjUnion s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)
      (_ : Disjoint s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)) =
    Finset.univ
⊢ 2 * card s = Fintype.card α
[PROOFSTEP]
rw [Fintype.card, ← this, two_mul, card_disjUnion, card_map]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ disjUnion s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)
      (_ : Disjoint s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)) =
    Finset.univ
[PROOFSTEP]
rw [← coe_eq_univ, disjUnion_eq_union, coe_union, coe_map, Function.Embedding.coeFn_mk,
  image_eq_preimage_of_inverse compl_compl compl_compl]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ ↑s ∪ compl ⁻¹' ↑s = univ
[PROOFSTEP]
refine' eq_univ_of_forall fun a => _
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a : α
⊢ a ∈ ↑s ∪ compl ⁻¹' ↑s
[PROOFSTEP]
simp_rw [mem_union, mem_preimage]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a : α
⊢ a ∈ ↑s ∨ aᶜ ∈ ↑s
[PROOFSTEP]
by_contra' ha
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a : α
ha : ¬a ∈ ↑s ∧ ¬aᶜ ∈ ↑s
⊢ False
[PROOFSTEP]
refine' s.ne_insert_of_not_mem _ ha.1 (h _ _ <| s.subset_insert _)
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a : α
ha : ¬a ∈ ↑s ∧ ¬aᶜ ∈ ↑s
⊢ Intersecting ↑(insert a s)
[PROOFSTEP]
rw [coe_insert]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a : α
ha : ¬a ∈ ↑s ∧ ¬aᶜ ∈ ↑s
⊢ Intersecting (insert a ↑s)
[PROOFSTEP]
refine' hs.insert _ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
a : α
ha : ¬a ∈ ↑s ∧ ¬aᶜ ∈ ↑s
⊢ a ≠ ⊥
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
ha : ¬⊥ ∈ ↑s ∧ ¬⊥ᶜ ∈ ↑s
⊢ False
[PROOFSTEP]
have := h {⊤} (by rw [coe_singleton]; exact intersecting_singleton.2 top_ne_bot)
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
ha : ¬⊥ ∈ ↑s ∧ ¬⊥ᶜ ∈ ↑s
⊢ Intersecting ↑{⊤}
[PROOFSTEP]
rw [coe_singleton]
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
ha : ¬⊥ ∈ ↑s ∧ ¬⊥ᶜ ∈ ↑s
⊢ Intersecting {⊤}
[PROOFSTEP]
exact intersecting_singleton.2 top_ne_bot
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
ha : ¬⊥ ∈ ↑s ∧ ¬⊥ᶜ ∈ ↑s
this : s ⊆ {⊤} → s = {⊤}
⊢ False
[PROOFSTEP]
rw [compl_bot] at ha 
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
ha : ¬⊥ ∈ ↑s ∧ ¬⊤ ∈ ↑s
this : s ⊆ {⊤} → s = {⊤}
⊢ False
[PROOFSTEP]
rw [coe_eq_empty.1 ((hs.isUpperSet' h).not_top_mem.1 ha.2)] at this 
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
ha : ¬⊥ ∈ ↑s ∧ ¬⊤ ∈ ↑s
this : ∅ ⊆ {⊤} → ∅ = {⊤}
⊢ False
[PROOFSTEP]
exact Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
have := hs.card_le
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
this : 2 * card s ≤ Fintype.card α
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
rw [mul_comm, ← Nat.le_div_iff_mul_le' two_pos] at this 
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
this : card s ≤ Fintype.card α / 2
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
revert hs
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
this : card s ≤ Fintype.card α / 2
⊢ Intersecting ↑s → ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
refine' s.strongDownwardInductionOn _ this
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
this : card s ≤ Fintype.card α / 2
⊢ ∀ (t₁ : Finset α),
    (∀ {t₂ : Finset α},
        card t₂ ≤ Fintype.card α / 2 →
          t₁ ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t) →
      card t₁ ≤ Fintype.card α / 2 → Intersecting ↑t₁ → ∃ t, t₁ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
rintro s ih _hcard hs
[GOAL]
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
by_cases h : ∀ t : Finset α, (t : Set α).Intersecting → s ⊆ t → s = t
[GOAL]
case pos
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
h : ∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
exact ⟨s, Subset.rfl, hs.is_max_iff_card_eq.1 h, hs⟩
[GOAL]
case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
h : ¬∀ (t : Finset α), Intersecting ↑t → s ⊆ t → s = t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
h : ∃ t, Intersecting ↑t ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
obtain ⟨t, ht, hst⟩ := h
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
t : Finset α
ht : Intersecting ↑t
hst : s ⊆ t ∧ s ≠ t
⊢ ∃ t, s ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
[PROOFSTEP]
refine' (ih _ (_root_.ssubset_iff_subset_ne.2 hst) ht).imp fun u => And.imp_left hst.1.trans
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
t : Finset α
ht : Intersecting ↑t
hst : s ⊆ t ∧ s ≠ t
⊢ card t ≤ Fintype.card α / 2
[PROOFSTEP]
rw [Nat.le_div_iff_mul_le' two_pos, mul_comm]
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : card s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    card t₂ ≤ Fintype.card α / 2 →
      s ⊂ t₂ → Intersecting ↑t₂ → ∃ t, t₂ ⊆ t ∧ 2 * card t = Fintype.card α ∧ Intersecting ↑t
_hcard : card s ≤ Fintype.card α / 2
hs : Intersecting ↑s
t : Finset α
ht : Intersecting ↑t
hst : s ⊆ t ∧ s ≠ t
⊢ 2 * card t ≤ Fintype.card α
[PROOFSTEP]
exact ht.card_le
