α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsUpperSet ↑ℬ
⊢ card 𝒜 * card ℬ ≤ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ)
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜 : IsUpperSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ card 𝒜 * card ℬ ≤ 2 ^ Fintype.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ℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * card (𝒜ᶜ ∩ ℬ) ≤ card (𝒜ᶜ) * card ℬ
⊢ card 𝒜 * card ℬ ≤ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ)
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsUpperSet ↑ℬ
⊢ card 𝒜 * card ℬ ≤ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ)
have := h𝒜.card_inter_le_finset hℬ
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * card (𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * card ℬ - card 𝒜 * card ℬ
⊢ 2 ^ Fintype.card α * card (𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * card ℬ

case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * card (𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * card ℬ - card 𝒜 * card ℬ
⊢ card 𝒜 * card ℬ ≤ 2 ^ Fintype.card α * card ℬ
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * card (𝒜ᶜ ∩ ℬ) ≤ card (𝒜ᶜ) * card ℬ
⊢ card 𝒜 * card ℬ ≤ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ)
rwa [card_compl, Fintype.card_finset, tsub_mul, le_tsub_iff_le_tsub, ← mul_tsub, ←
  card_sdiff (inter_subset_right _ _), sdiff_inter_self_right, sdiff_compl,
  _root_.inf_comm] at this
no goals
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * card (𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * card ℬ - card 𝒜 * card ℬ
⊢ 2 ^ Fintype.card α * card (𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * card ℬ
exact mul_le_mul_left' (card_le_of_subset <| inter_subset_right _ _) _
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * card (𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * card ℬ - card 𝒜 * card ℬ
⊢ card 𝒜 * card ℬ ≤ Fintype.card (Finset α) * card ℬ
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * card (𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * card ℬ - card 𝒜 * card ℬ
⊢ card 𝒜 * card ℬ ≤ 2 ^ Fintype.card α * card ℬ
rw [← Fintype.card_finset]
no goals
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜ᶜ)
h𝒜 : IsLowerSet ↑(𝒜ᶜ)
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * card (𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * card ℬ - card 𝒜 * card ℬ
⊢ card 𝒜 * card ℬ ≤ Fintype.card (Finset α) * card ℬ
exact mul_le_mul_right' (card_le_univ _) _