rw [← inf_sup_left, huv.codisjoint.eq_top, inf_top_eq]
case intro.intro.intro.intro
α : Type u_1
inst✝ : BooleanAlgebra α
s t u✝ : Finset α
a x u v : α
huv : IsCompl u v
hu : ∀ ⦃b : α⦄, x ⊓ u = b ⊓ u → b ∈ s
hv : ∀ ⦃b : α⦄, x ⊓ v = b ⊓ v → b ∈ t
⊢ x ⊓ u ⊔ x ⊓ v = x
no goals