rw [certificator, mem_filter, and_iff_right_of_imp]
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
⊢ a ∈ s □ t ↔ ∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t
α : 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