exact ⟨s, ⟨hs, hℬ hts ht⟩, t, ⟨h𝒜 hts hs, ht⟩, hts, rfl⟩
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
s : Finset α
hs : s ∈ 𝒜
t : Finset α
ht : t ∈ ℬ
hts : t ≤ s
⊢ ∃ b, (b ∈ 𝒜 ∧ b ∈ ℬ) ∧ ∃ c, (c ∈ 𝒜 ∧ c ∈ ℬ) ∧ c ≤ b ∧ b \ c = s \ t
no goals