refine' (card_le_card _).trans (card_posDiffs_self_le _)
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ (𝒜 \₊ ℬ).card ≤ (𝒜 ∩ ℬ).card
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 𝒜 \₊ ℬ ⊆ 𝒜 ∩ ℬ \₊ (𝒜 ∩ ℬ)

case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ (↑(𝒜 ∩ ℬ)).OrdConnected