α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsLowerSet ↑ℬ
⊢ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ) ≤ card 𝒜 * card ℬ
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜 : IsUpperSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
⊢ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ) ≤ card 𝒜 * card ℬ
rw [← isLowerSet_compl, ← coe_compl] at h𝒜
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsLowerSet ↑ℬ
this : card (𝒜ᶜ) * card ℬ ≤ 2 ^ Fintype.card α * card (𝒜ᶜ ∩ ℬ)
⊢ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ) ≤ card 𝒜 * card ℬ
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsLowerSet ↑ℬ
⊢ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ) ≤ card 𝒜 * card ℬ
have := h𝒜.le_card_inter_finset hℬ
no goals
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsLowerSet ↑ℬ
this : card (𝒜ᶜ) * card ℬ ≤ 2 ^ Fintype.card α * card (𝒜ᶜ ∩ ℬ)
⊢ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ) ≤ card 𝒜 * card ℬ
rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
  card_sdiff (inter_subset_right _ _), sdiff_inter_self_right, sdiff_compl,
  _root_.inf_comm] at this