rintro _ ⟨s, hs, t, ht, hts, rfl⟩
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ ∀ ⦃x : Finset α⦄,
    (∃ b ∈ 𝒜, ∃ c ∈ ℬ, c ≤ b ∧ b \ c = x) → ∃ b, (b ∈ 𝒜 ∧ b ∈ ℬ) ∧ ∃ c, (c ∈ 𝒜 ∧ c ∈ ℬ) ∧ c ≤ b ∧ b \ c = x
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