[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s✝ : Finset α
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ s ∈ ↑(Finset.nonMemberSubfamily a 𝒜) → t ∈ ↑(Finset.nonMemberSubfamily a 𝒜)
[PROOFSTEP]
simp_rw [mem_coe, mem_nonMemberSubfamily]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s✝ : Finset α
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ s ∈ 𝒜 ∧ ¬a ∈ s → t ∈ 𝒜 ∧ ¬a ∈ t
[PROOFSTEP]
exact And.imp (h hts) (mt <| @hts _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h : IsLowerSet ↑𝒜
⊢ IsLowerSet ↑(Finset.memberSubfamily a 𝒜)
[PROOFSTEP]
rintro s t hts
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s✝ : Finset α
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ s ∈ ↑(Finset.memberSubfamily a 𝒜) → t ∈ ↑(Finset.memberSubfamily a 𝒜)
[PROOFSTEP]
simp_rw [mem_coe, mem_memberSubfamily]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s✝ : Finset α
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ insert a s ∈ 𝒜 ∧ ¬a ∈ s → insert a t ∈ 𝒜 ∧ ¬a ∈ t
[PROOFSTEP]
exact And.imp (h <| insert_subset_insert _ hts) (mt <| @hts _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s✝ : Finset α
a : α
h : IsLowerSet ↑𝒜
s : Finset α
⊢ s ∈ Finset.memberSubfamily a 𝒜 → s ∈ Finset.nonMemberSubfamily a 𝒜
[PROOFSTEP]
rw [mem_memberSubfamily, mem_nonMemberSubfamily]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s✝ : Finset α
a : α
h : IsLowerSet ↑𝒜
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ ¬a ∈ s → s ∈ 𝒜 ∧ ¬a ∈ s
[PROOFSTEP]
exact And.imp_left (h <| subset_insert _ _)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ s
⊢ card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
[PROOFSTEP]
induction' s using Finset.induction with a s hs ih generalizing 𝒜 ℬ
[GOAL]
case empty
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s : Finset α
a : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ ∅
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ ∅
⊢ card 𝒜 * card ℬ ≤ 2 ^ card ∅ * card (𝒜 ∩ ℬ)
[PROOFSTEP]
simp_rw [subset_empty, ← subset_singleton_iff', subset_singleton_iff] at h𝒜s hℬs 
[GOAL]
case empty
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s : Finset α
a : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : 𝒜 = ∅ ∨ 𝒜 = {∅}
hℬs : ℬ = ∅ ∨ ℬ = {∅}
⊢ card 𝒜 * card ℬ ≤ 2 ^ card ∅ * card (𝒜 ∩ ℬ)
[PROOFSTEP]
obtain rfl | rfl := h𝒜s
[GOAL]
case empty.inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ✝ : Finset (Finset α)
s : Finset α
a : α
h𝒜✝ : IsLowerSet ↑𝒜
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑∅
⊢ card ∅ * card ℬ ≤ 2 ^ card ∅ * card (∅ ∩ ℬ)
[PROOFSTEP]
simp only [card_empty, empty_inter, mul_zero, zero_mul]
[GOAL]
case empty.inr
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ✝ : Finset (Finset α)
s : Finset α
a : α
h𝒜✝ : IsLowerSet ↑𝒜
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑{∅}
⊢ card {∅} * card ℬ ≤ 2 ^ card ∅ * card ({∅} ∩ ℬ)
[PROOFSTEP]
obtain rfl | rfl := hℬs
[GOAL]
case empty.inr.inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h𝒜✝ : IsLowerSet ↑𝒜
hℬ✝ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ s
h𝒜 : IsLowerSet ↑{∅}
hℬ : IsLowerSet ↑∅
⊢ card {∅} * card ∅ ≤ 2 ^ card ∅ * card ({∅} ∩ ∅)
[PROOFSTEP]
simp only [card_empty, inter_empty, mul_zero, zero_mul]
[GOAL]
case empty.inr.inr
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h𝒜✝ : IsLowerSet ↑𝒜
hℬ✝ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ s
h𝒜 hℬ : IsLowerSet ↑{∅}
⊢ card {∅} * card {∅} ≤ 2 ^ card ∅ * card ({∅} ∩ {∅})
[PROOFSTEP]
simp only [card_empty, pow_zero, inter_singleton_of_mem, mem_singleton, card_singleton]
[GOAL]
case insert
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
⊢ card 𝒜 * card ℬ ≤ 2 ^ card (insert a s) * card (𝒜 ∩ ℬ)
[PROOFSTEP]
rw [card_insert_of_not_mem hs, ← card_memberSubfamily_add_card_nonMemberSubfamily a 𝒜, ←
  card_memberSubfamily_add_card_nonMemberSubfamily a ℬ, add_mul, mul_add, mul_add, add_comm (_ * _), add_add_add_comm]
[GOAL]
case insert
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
⊢ card (Finset.memberSubfamily a 𝒜) * card (Finset.nonMemberSubfamily a ℬ) +
        card (Finset.nonMemberSubfamily a 𝒜) * card (Finset.memberSubfamily a ℬ) +
      (card (Finset.memberSubfamily a 𝒜) * card (Finset.memberSubfamily a ℬ) +
        card (Finset.nonMemberSubfamily a 𝒜) * card (Finset.nonMemberSubfamily a ℬ)) ≤
    2 ^ (card s + 1) * card (𝒜 ∩ ℬ)
[PROOFSTEP]
refine'
  (add_le_add_right
        (mul_add_mul_le_mul_add_mul (card_le_of_subset h𝒜.memberSubfamily_subset_nonMemberSubfamily) <|
          card_le_of_subset hℬ.memberSubfamily_subset_nonMemberSubfamily)
        _).trans
    _
[GOAL]
case insert
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
⊢ card (Finset.memberSubfamily a 𝒜) * card (Finset.memberSubfamily a ℬ) +
        card (Finset.nonMemberSubfamily a 𝒜) * card (Finset.nonMemberSubfamily a ℬ) +
      (card (Finset.memberSubfamily a 𝒜) * card (Finset.memberSubfamily a ℬ) +
        card (Finset.nonMemberSubfamily a 𝒜) * card (Finset.nonMemberSubfamily a ℬ)) ≤
    2 ^ (card s + 1) * card (𝒜 ∩ ℬ)
[PROOFSTEP]
rw [← two_mul, pow_succ, mul_assoc]
[GOAL]
case insert
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
⊢ 2 *
      (card (Finset.memberSubfamily a 𝒜) * card (Finset.memberSubfamily a ℬ) +
        card (Finset.nonMemberSubfamily a 𝒜) * card (Finset.nonMemberSubfamily a ℬ)) ≤
    2 * (2 ^ card s * card (𝒜 ∩ ℬ))
[PROOFSTEP]
have h₀ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ 𝒞.nonMemberSubfamily a, t ⊆ s :=
  by
  rintro 𝒞 h𝒞 t ht
  rw [mem_nonMemberSubfamily] at ht 
  exact (subset_insert_iff_of_not_mem ht.2).1 (h𝒞 _ ht.1)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
⊢ ∀ (𝒞 : Finset (Finset α)),
    (∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s) → ∀ (t : Finset α), t ∈ Finset.nonMemberSubfamily a 𝒞 → t ⊆ s
[PROOFSTEP]
rintro 𝒞 h𝒞 t ht
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
𝒞 : Finset (Finset α)
h𝒞 : ∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s
t : Finset α
ht : t ∈ Finset.nonMemberSubfamily a 𝒞
⊢ t ⊆ s
[PROOFSTEP]
rw [mem_nonMemberSubfamily] at ht 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
𝒞 : Finset (Finset α)
h𝒞 : ∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s
t : Finset α
ht : t ∈ 𝒞 ∧ ¬a ∈ t
⊢ t ⊆ s
[PROOFSTEP]
exact (subset_insert_iff_of_not_mem ht.2).1 (h𝒞 _ ht.1)
[GOAL]
case insert
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
h₀ :
  ∀ (𝒞 : Finset (Finset α)),
    (∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s) → ∀ (t : Finset α), t ∈ Finset.nonMemberSubfamily a 𝒞 → t ⊆ s
⊢ 2 *
      (card (Finset.memberSubfamily a 𝒜) * card (Finset.memberSubfamily a ℬ) +
        card (Finset.nonMemberSubfamily a 𝒜) * card (Finset.nonMemberSubfamily a ℬ)) ≤
    2 * (2 ^ card s * card (𝒜 ∩ ℬ))
[PROOFSTEP]
have h₁ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ 𝒞.memberSubfamily a, t ⊆ s :=
  by
  rintro 𝒞 h𝒞 t ht
  rw [mem_memberSubfamily] at ht 
  exact (subset_insert_iff_of_not_mem ht.2).1 ((subset_insert _ _).trans <| h𝒞 _ ht.1)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
h₀ :
  ∀ (𝒞 : Finset (Finset α)),
    (∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s) → ∀ (t : Finset α), t ∈ Finset.nonMemberSubfamily a 𝒞 → t ⊆ s
⊢ ∀ (𝒞 : Finset (Finset α)),
    (∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s) → ∀ (t : Finset α), t ∈ Finset.memberSubfamily a 𝒞 → t ⊆ s
[PROOFSTEP]
rintro 𝒞 h𝒞 t ht
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
h₀ :
  ∀ (𝒞 : Finset (Finset α)),
    (∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s) → ∀ (t : Finset α), t ∈ Finset.nonMemberSubfamily a 𝒞 → t ⊆ s
𝒞 : Finset (Finset α)
h𝒞 : ∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s
t : Finset α
ht : t ∈ Finset.memberSubfamily a 𝒞
⊢ t ⊆ s
[PROOFSTEP]
rw [mem_memberSubfamily] at ht 
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
h₀ :
  ∀ (𝒞 : Finset (Finset α)),
    (∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s) → ∀ (t : Finset α), t ∈ Finset.nonMemberSubfamily a 𝒞 → t ⊆ s
𝒞 : Finset (Finset α)
h𝒞 : ∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s
t : Finset α
ht : insert a t ∈ 𝒞 ∧ ¬a ∈ t
⊢ t ⊆ s
[PROOFSTEP]
exact (subset_insert_iff_of_not_mem ht.2).1 ((subset_insert _ _).trans <| h𝒞 _ ht.1)
[GOAL]
case insert
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
h₀ :
  ∀ (𝒞 : Finset (Finset α)),
    (∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s) → ∀ (t : Finset α), t ∈ Finset.nonMemberSubfamily a 𝒞 → t ⊆ s
h₁ :
  ∀ (𝒞 : Finset (Finset α)),
    (∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s) → ∀ (t : Finset α), t ∈ Finset.memberSubfamily a 𝒞 → t ⊆ s
⊢ 2 *
      (card (Finset.memberSubfamily a 𝒜) * card (Finset.memberSubfamily a ℬ) +
        card (Finset.nonMemberSubfamily a 𝒜) * card (Finset.nonMemberSubfamily a ℬ)) ≤
    2 * (2 ^ card s * card (𝒜 ∩ ℬ))
[PROOFSTEP]
refine' mul_le_mul_left' _ _
[GOAL]
case insert
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
h₀ :
  ∀ (𝒞 : Finset (Finset α)),
    (∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s) → ∀ (t : Finset α), t ∈ Finset.nonMemberSubfamily a 𝒞 → t ⊆ s
h₁ :
  ∀ (𝒞 : Finset (Finset α)),
    (∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s) → ∀ (t : Finset α), t ∈ Finset.memberSubfamily a 𝒞 → t ⊆ s
⊢ card (Finset.memberSubfamily a 𝒜) * card (Finset.memberSubfamily a ℬ) +
      card (Finset.nonMemberSubfamily a 𝒜) * card (Finset.nonMemberSubfamily a ℬ) ≤
    2 ^ card s * card (𝒜 ∩ ℬ)
[PROOFSTEP]
refine'
  (add_le_add (ih h𝒜.memberSubfamily hℬ.memberSubfamily (h₁ _ h𝒜s) <| h₁ _ hℬs) <|
        ih h𝒜.nonMemberSubfamily hℬ.nonMemberSubfamily (h₀ _ h𝒜s) <| h₀ _ hℬs).trans_eq
    _
[GOAL]
case insert
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s✝ : Finset α
a✝ : α
h𝒜✝ : IsLowerSet ↑𝒜✝
hℬ✝ : IsLowerSet ↑ℬ✝
h𝒜s✝ : ∀ (t : Finset α), t ∈ 𝒜✝ → t ⊆ s✝
hℬs✝ : ∀ (t : Finset α), t ∈ ℬ✝ → t ⊆ s✝
a : α
s : Finset α
hs : ¬a ∈ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 →
      IsLowerSet ↑ℬ →
        (∀ (t : Finset α), t ∈ 𝒜 → t ⊆ s) →
          (∀ (t : Finset α), t ∈ ℬ → t ⊆ s) → card 𝒜 * card ℬ ≤ 2 ^ card s * card (𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ (t : Finset α), t ∈ 𝒜 → t ⊆ insert a s
hℬs : ∀ (t : Finset α), t ∈ ℬ → t ⊆ insert a s
h₀ :
  ∀ (𝒞 : Finset (Finset α)),
    (∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s) → ∀ (t : Finset α), t ∈ Finset.nonMemberSubfamily a 𝒞 → t ⊆ s
h₁ :
  ∀ (𝒞 : Finset (Finset α)),
    (∀ (t : Finset α), t ∈ 𝒞 → t ⊆ insert a s) → ∀ (t : Finset α), t ∈ Finset.memberSubfamily a 𝒞 → t ⊆ s
⊢ 2 ^ card s * card (Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
      2 ^ card s * card (Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ) =
    2 ^ card s * card (𝒜 ∩ ℬ)
[PROOFSTEP]
rw [← mul_add, ← memberSubfamily_inter, ← nonMemberSubfamily_inter, card_memberSubfamily_add_card_nonMemberSubfamily]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜 : IsUpperSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
⊢ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ) ≤ card 𝒜 * card ℬ
[PROOFSTEP]
rw [← isLowerSet_compl, ← coe_compl] at h𝒜 
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜)ᶜ
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsLowerSet ↑ℬ
⊢ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ) ≤ card 𝒜 * card ℬ
[PROOFSTEP]
have := h𝒜.le_card_inter_finset hℬ
[GOAL]
α : 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 ℬ
[PROOFSTEP]
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 
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ) ≤ card 𝒜 * card ℬ
[PROOFSTEP]
rw [inter_comm, mul_comm 𝒜.card]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 2 ^ Fintype.card α * card (ℬ ∩ 𝒜) ≤ card ℬ * card 𝒜
[PROOFSTEP]
exact hℬ.card_inter_le_finset h𝒜
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜 : IsUpperSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ card 𝒜 * card ℬ ≤ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ)
[PROOFSTEP]
rw [← isLowerSet_compl, ← coe_compl] at h𝒜 
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
inst✝ : Fintype α
h𝒜✝ : IsLowerSet (↑𝒜)ᶜ
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
⊢ card 𝒜 * card ℬ ≤ 2 ^ Fintype.card α * card (𝒜 ∩ ℬ)
[PROOFSTEP]
have := h𝒜.card_inter_le_finset hℬ
[GOAL]
α : 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 (𝒜 ∩ ℬ)
[PROOFSTEP]
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 
[GOAL]
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 ℬ
[PROOFSTEP]
exact mul_le_mul_left' (card_le_of_subset <| inter_subset_right _ _) _
[GOAL]
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 ℬ
[PROOFSTEP]
rw [← Fintype.card_finset]
[GOAL]
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 ℬ
[PROOFSTEP]
exact mul_le_mul_right' (card_le_univ _) _
