α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : Intersecting ↑s
⊢ ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ map { toFun := compl, inj' := (_ : Function.Injective compl) } s
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : Intersecting ↑s
⊢ Disjoint s (map { toFun := compl, inj' := (_ : Function.Injective compl) } s)
rw [Finset.disjoint_left]
α : 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
α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : Intersecting ↑s
⊢ ∀ ⦃a : α⦄, a ∈ s → ¬a ∈ map { toFun := compl, inj' := (_ : Function.Injective compl) } s
rintro x hx hxc
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
α : 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
obtain ⟨x, hx', rfl⟩ := mem_map.mp hxc
no goals
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
exact hs.not_compl_mem hx' hx