refine' ⟨x ⊓ u, hu (inf_right_idem _ _).symm, x ⊓ v, hv (inf_right_idem _ _).symm,
  huv.disjoint.mono inf_le_right inf_le_right, _⟩
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
⊢ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = x
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