refine' certificator_subset_inter.antisymm fun a ha ↦
  mem_certificator.2 ⟨aᶜ, a, isCompl_compl.symm, _⟩
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsLowerSet ↑s
ht : IsUpperSet ↑t
⊢ s □ t = s ∩ t
α : 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