-- Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean
theorem IsLowerSet.le_card_inter_finset' (h𝒜 : IsLowerSet (𝒜 : Set (Finset α)))
    (hℬ : IsLowerSet (ℬ : Set (Finset α))) (h𝒜s : ∀ t ∈ 𝒜, t ⊆ s) (hℬs : ∀ t ∈ ℬ, t ⊆ s) :
    #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)

Proof state:
case empty
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : 𝒜 = ∅ ∨ 𝒜 = {∅}
hℬs : ℬ = ∅ ∨ ℬ = {∅}
⊢ #𝒜 * #ℬ ≤ 2 ^ #∅ * #(𝒜 ∩ ℬ)

Tactic:
obtain rfl | rfl := h𝒜s

Result:
case empty.inl
α : Type u_1
inst✝ : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑∅
⊢ #∅ * #ℬ ≤ 2 ^ #∅ * #(∅ ∩ ℬ)

case empty.inr
α : Type u_1
inst✝ : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑{∅}
⊢ #{∅} * #ℬ ≤ 2 ^ #∅ * #({∅} ∩ ℬ)

Proof state:
case empty.inr
α : Type u_1
inst✝ : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑{∅}
⊢ #{∅} * #ℬ ≤ 2 ^ #∅ * #({∅} ∩ ℬ)

Tactic:
obtain rfl | rfl := hℬs

Result:
case empty.inr.inl
α : Type u_1
inst✝ : DecidableEq α
h𝒜 : IsLowerSet ↑{∅}
hℬ : IsLowerSet ↑∅
⊢ #{∅} * #∅ ≤ 2 ^ #∅ * #({∅} ∩ ∅)

case empty.inr.inr
α : Type u_1
inst✝ : DecidableEq α
h𝒜 hℬ : IsLowerSet ↑{∅}
⊢ #{∅} * #{∅} ≤ 2 ^ #∅ * #({∅} ∩ {∅})

Proof state:
case empty.inl
α : Type u_1
inst✝ : DecidableEq α
ℬ : Finset (Finset α)
hℬ : IsLowerSet ↑ℬ
hℬs : ℬ = ∅ ∨ ℬ = {∅}
h𝒜 : IsLowerSet ↑∅
⊢ #∅ * #ℬ ≤ 2 ^ #∅ * #(∅ ∩ ℬ)

Tactic:
simp only [card_empty, zero_mul, empty_inter, mul_zero, le_refl]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : t ∈ Finset.nonMemberSubfamily a 𝒞
⊢ t ⊆ s

Tactic:
rw [mem_nonMemberSubfamily] at ht

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : t ∈ 𝒞 ∧ a ∉ t
⊢ t ⊆ s

Proof state:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
⊢ 2 ^ #s * #(Finset.memberSubfamily a 𝒜 ∩ Finset.memberSubfamily a ℬ) +
      2 ^ #s * #(Finset.nonMemberSubfamily a 𝒜 ∩ Finset.nonMemberSubfamily a ℬ) =
    2 ^ #s * #(𝒜 ∩ ℬ)

Tactic:
rw [← mul_add, ← memberSubfamily_inter, ← nonMemberSubfamily_inter,
  card_memberSubfamily_add_card_nonMemberSubfamily]

Result:
no goals

Proof state:
case empty.inr.inl
α : Type u_1
inst✝ : DecidableEq α
h𝒜 : IsLowerSet ↑{∅}
hℬ : IsLowerSet ↑∅
⊢ #{∅} * #∅ ≤ 2 ^ #∅ * #({∅} ∩ ∅)

Tactic:
simp only [card_empty, inter_empty, mul_zero, zero_mul, le_refl]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : insert a t ∈ 𝒞 ∧ a ∉ t
⊢ t ⊆ s

Tactic:
exact (subset_insert_iff_of_not_mem ht.2).1 ((subset_insert _ _).trans <| h𝒞 _ ht.1)

Result:
no goals

Proof state:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
⊢ 2 *
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 * (2 ^ #s * #(𝒜 ∩ ℬ))

Tactic:
refine mul_le_mul_left' ?_ _

Result:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
⊢ #(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
      #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ) ≤
    2 ^ #s * #(𝒜 ∩ ℬ)

Proof state:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ #(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ) +
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 ^ (#s + 1) * #(𝒜 ∩ ℬ)

Tactic:
rw [← two_mul, pow_succ', mul_assoc]

Result:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ 2 *
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 * (2 ^ #s * #(𝒜 ∩ ℬ))