-- 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 α
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
refine₁₁ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (ha : ⊥ ∉ (↑s : Set α) ∧ ⊤ ∉ (↑s : Set α))
    (this : s ⊆ {⊤} → s = {⊤}), False
refine₁₂ :
  ∀ (h : ∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) (ha : ⊥ ∉ (↑s : Set α) ∧ ⊤ ∉ (↑s : Set α))
    (this : Subset (α := Finset α) ∅ {⊤} → Eq (α := Finset α) ∅ {⊤}), False
⊢ (∀ (t : Finset α), (↑t : Set α).Intersecting → s ⊆ t → s = t) ↔ 2 * #s = Fintype.card α

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

Premises used: Set.mem_union, compl_compl, Finset.coe_eq_univ, Set.eq_univ_of_forall, Set.image_eq_preimage_of_inverse, Function.Embedding.coeFn_mk, Finset.coe_map, Finset.disjUnion_eq_union, Finset.coe_insert, rfl, Set.mem_preimage, compl_bot, Finset.coe_union