refine' certificator_subset_disjSups.antisymm fun a ha ↦ mem_certificator.2 _
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
⊢ s □ t = s ○ t
α : Type u_1
inst✝ : BooleanAlgebra α
s t u : Finset α
a✝ : α
hs : IsUpperSet ↑s
ht : IsUpperSet ↑t
a : α
ha : a ∈ s ○ t
⊢ ∃ x y, IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t