rw [mem_inter] at ha
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∩ t
⊢ (∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ t
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ∧ a ∈ t
⊢ (∀ ⦃b : α⦄, a ⊓ aᶜ = b ⊓ aᶜ → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ a = b ⊓ a → b ∈ t