no goals
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ 2 * card s ≤ Fintype.card α
classical
  refine' (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' _
  rw [two_mul, card_disjUnion, card_map]
α : 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)))
α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : Intersecting ↑s
⊢ 2 * card s ≤ Fintype.card α
refine' (s.disjUnion _ hs.disjoint_map_compl).card_le_univ.trans_eq' _
no goals
α : 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)))
rw [two_mul, card_disjUnion, card_map]