exact mem_inter.2 ⟨hu rfl, hv rfl⟩
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a u v : α
left✝ : IsCompl u v
hu : ∀ ⦃b : α⦄, a ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, a ⊓ v = b ⊓ v → b ∈ t
⊢ a ∈ s ∩ t
no goals