no goals
α : 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 α
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
α : 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 α
α : 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 α
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⟩
α : 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
α : 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 α
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]
α : 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
α : 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
rw [← coe_eq_univ, disjUnion_eq_union, coe_union, coe_map, Function.Embedding.coeFn_mk,
  image_eq_preimage_of_inverse compl_compl compl_compl]
α : 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
α : 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
refine' eq_univ_of_forall fun a => _
α : 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
α : 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
simp_rw [mem_union, mem_preimage]
α : 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
α : 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
by_contra' ha
α : 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.insert a s)
α : 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
refine' s.ne_insert_of_not_mem _ ha.1 (h _ _ <| s.subset_insert _)
α : 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.insert a ↑s)
α : 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.insert a s)
rw [coe_insert]
α : 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 ≠ ⊥
α : 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.insert a ↑s)
refine' hs.insert _ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb
α : 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
α : 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 ≠ ⊥
rintro rfl
α : 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
α : 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
have := h {⊤} (by rw [coe_singleton]; exact intersecting_singleton.2 top_ne_bot)
α : 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
α : 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
rw [compl_bot] at ha
α : 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
α : 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
rw [coe_eq_empty.1 ((hs.isUpperSet' h).not_top_mem.1 ha.2)] at this
no goals
α : 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
exact Finset.singleton_ne_empty _ (this <| Finset.empty_subset _).symm
no goals
α : 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 α
rw [Fintype.card, ← this, two_mul, card_disjUnion, card_map]
α : 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 {⊤}
α : 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 ↑{⊤}
rw [coe_singleton]
no goals
α : 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 {⊤}
exact intersecting_singleton.2 top_ne_bot