rintro ⟨u, v, _, hu, hv⟩
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ (∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t) → a ∈ s ∩ t
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