[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
[PROOFSTEP]
have : DecidableEq ι := by classical infer_instance
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
⊢ DecidableEq ι
[PROOFSTEP]
classical infer_instance
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
⊢ DecidableEq ι
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
[PROOFSTEP]
obtain hs | hs := le_total (Fintype.card α) s.card
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
hs : Fintype.card α ≤ card s
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
[PROOFSTEP]
rw [tsub_eq_zero_of_le hs, pow_zero]
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
hs : Fintype.card α ≤ card s
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 1
[PROOFSTEP]
refine'
  (card_le_of_subset <|
        biUnion_subset.2 fun i hi a ha ↦ mem_compl.2 <| not_mem_singleton.2 <| (hf _ hi).ne_bot ha).trans_eq
    _
[GOAL]
case inl
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
hs : Fintype.card α ≤ card s
⊢ card {⊥}ᶜ = 2 ^ Fintype.card α - 1
[PROOFSTEP]
rw [card_compl, Fintype.card_finset, card_singleton]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)
this : DecidableEq ι
hs : card s ≤ Fintype.card α
⊢ card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
[PROOFSTEP]
induction' s using Finset.cons_induction with i s hi ih generalizing f
[GOAL]
case inr.empty
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s ≤ Fintype.card α
f : ι → Finset (Finset α)
hf : ∀ (i : ι), i ∈ ∅ → Set.Intersecting ↑(f i)
hs : card ∅ ≤ Fintype.card α
⊢ card (Finset.biUnion ∅ f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card ∅)
[PROOFSTEP]
simp
[GOAL]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
⊢ card (Finset.biUnion (cons i s hi) f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
[PROOFSTEP]
set f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then (hf j hj).exists_card_eq.choose else ∅
[GOAL]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
⊢ card (Finset.biUnion (cons i s hi) f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
[PROOFSTEP]
have hf₁ :
  ∀ j, j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * (f' j).card = 2 ^ Fintype.card α ∧ (f' j : Set (Finset α)).Intersecting :=
  by
  rintro j hj
  simp_rw [dif_pos hj, ← Fintype.card_finset]
  exact Classical.choose_spec (hf j hj).exists_card_eq
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
⊢ ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
[PROOFSTEP]
rintro j hj
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
[PROOFSTEP]
simp_rw [dif_pos hj, ← Fintype.card_finset]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆ Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t) ∧
    2 * card (Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)) =
        Fintype.card (Finset α) ∧
      Set.Intersecting ↑(Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t))
[PROOFSTEP]
exact Classical.choose_spec (hf j hj).exists_card_eq
[GOAL]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
⊢ card (Finset.biUnion (cons i s hi) f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
[PROOFSTEP]
have hf₂ : ∀ j, j ∈ cons i s hi → IsUpperSet (f' j : Set (Finset α)) :=
  by
  refine' fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 _)
  rw [Fintype.card_finset]
  exact (hf₁ _ hj).2.1
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
⊢ ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
[PROOFSTEP]
refine' fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 _)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
j : ι
hj : j ∈ cons i s hi
⊢ 2 * card (f' j) = Fintype.card (Finset α)
[PROOFSTEP]
rw [Fintype.card_finset]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
j : ι
hj : j ∈ cons i s hi
⊢ 2 * card (f' j) = 2 ^ Fintype.card α
[PROOFSTEP]
exact (hf₁ _ hj).2.1
[GOAL]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (Finset.biUnion (cons i s hi) f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
[PROOFSTEP]
refine' (card_le_of_subset <| biUnion_mono fun j hj ↦ (hf₁ _ hj).1).trans _
[GOAL]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (Finset.biUnion (cons i s hi) fun j => f' j) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
[PROOFSTEP]
nth_rw 1 [cons_eq_insert i]
[GOAL]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (Finset.biUnion (insert i s) fun j => f' j) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
[PROOFSTEP]
rw [biUnion_insert]
[GOAL]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (f' i ∪ Finset.biUnion s fun j => f' j) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
[PROOFSTEP]
refine' (card_mono <| @le_sup_sdiff _ _ _ <| f' i).trans ((card_union_le _ _).trans _)
[GOAL]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (f' i) + card ((f' i ∪ Finset.biUnion s fun j => f' j) \ f' i) ≤
    2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
[PROOFSTEP]
rw [union_sdiff_left, sdiff_eq_inter_compl]
[GOAL]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ card (f' i) + card ((Finset.biUnion s fun j => f' j) ∩ (f' i)ᶜ) ≤
    2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))
[PROOFSTEP]
refine' le_of_mul_le_mul_left _ (pow_pos (zero_lt_two' ℕ) <| Fintype.card α + 1)
[GOAL]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ (Fintype.card α + 1) * (card (f' i) + card ((Finset.biUnion s fun j => f' j) ∩ (f' i)ᶜ)) ≤
    2 ^ (Fintype.card α + 1) * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
[PROOFSTEP]
rw [pow_succ', mul_add, mul_assoc, mul_comm _ 2, mul_assoc]
[GOAL]
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * (2 * card (f' i)) +
      2 * (2 ^ Fintype.card α * card ((Finset.biUnion s fun j => f' j) ∩ (f' i)ᶜ)) ≤
    2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
[PROOFSTEP]
refine'
  (add_le_add ((mul_le_mul_left <| pow_pos (zero_lt_two' ℕ) _).2 (hf₁ _ <| mem_cons_self _ _).2.2.card_le) <|
        (mul_le_mul_left <| zero_lt_two' ℕ).2 <| IsUpperSet.card_inter_le_finset _ _).trans
    _
[GOAL]
case inr.cons.refine'_1
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ IsUpperSet ↑(Finset.biUnion s fun j => f' j)
[PROOFSTEP]
rw [coe_biUnion]
[GOAL]
case inr.cons.refine'_1
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ IsUpperSet (⋃ (x : ι) (_ : x ∈ ↑s), ↑(f' x))
[PROOFSTEP]
exact isUpperSet_iUnion₂ fun i hi ↦ hf₂ _ <| subset_cons _ hi
[GOAL]
case inr.cons.refine'_2
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ IsLowerSet ↑(f' i)ᶜ
[PROOFSTEP]
rw [coe_compl]
[GOAL]
case inr.cons.refine'_2
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ IsLowerSet (↑(f' i))ᶜ
[PROOFSTEP]
exact (hf₂ _ <| mem_cons_self _ _).compl
[GOAL]
case inr.cons.refine'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * Fintype.card (Finset α) + 2 * (card (Finset.biUnion s fun j => f' j) * card (f' i)ᶜ) ≤
    2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
[PROOFSTEP]
rw [mul_tsub, card_compl, Fintype.card_finset, mul_left_comm, mul_tsub, (hf₁ _ <| mem_cons_self _ _).2.1, two_mul,
  add_tsub_cancel_left, ← mul_tsub, ← mul_two, mul_assoc, ← add_mul, mul_comm]
[GOAL]
case inr.cons.refine'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * (2 ^ Fintype.card α + card (Finset.biUnion s fun j => f' j)) ≤
    2 ^ Fintype.card α * (2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi))))
[PROOFSTEP]
refine' mul_le_mul_left' _ _
[GOAL]
case inr.cons.refine'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α + card (Finset.biUnion s fun j => f' j) ≤
    2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
[PROOFSTEP]
refine'
  (add_le_add_left (ih _ (fun i hi ↦ (hf₁ _ <| subset_cons _ hi).2.2) ((card_le_of_subset <| subset_cons _).trans hs))
        _).trans
    _
[GOAL]
case inr.cons.refine'_3
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s✝ : Finset ι
f✝ : ι → Finset (Finset α)
hf✝ : ∀ (i : ι), i ∈ s✝ → Set.Intersecting ↑(f✝ i)
this : DecidableEq ι
hs✝ : card s✝ ≤ Fintype.card α
i : ι
s : Finset ι
hi : ¬i ∈ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i)) →
      card s ≤ Fintype.card α → card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)
f : ι → Finset (Finset α)
hf : ∀ (i_1 : ι), i_1 ∈ cons i s hi → Set.Intersecting ↑(f i_1)
hs : card (cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) :=
  fun j =>
    if hj : j ∈ cons i s hi then
      Exists.choose (_ : ∃ t, f j ⊆ t ∧ 2 * card t = Fintype.card (Finset α) ∧ Set.Intersecting ↑t)
    else ∅
hf₁ : ∀ (j : ι), j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * card (f' j) = 2 ^ Fintype.card α ∧ Set.Intersecting ↑(f' j)
hf₂ : ∀ (j : ι), j ∈ cons i s hi → IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α + (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card s)) ≤
    2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - card (cons i s hi)))
[PROOFSTEP]
rw [mul_tsub, two_mul, ← pow_succ, ← add_tsub_assoc_of_le (pow_le_pow' (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self),
  tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right]


[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 _) _


[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ nonMemberSubfamily a 𝒜 ↔ s ∈ 𝒜 ∧ ¬a ∈ s
[PROOFSTEP]
simp [nonMemberSubfamily]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ memberSubfamily a 𝒜 ↔ insert a s ∈ 𝒜 ∧ ¬a ∈ s
[PROOFSTEP]
simp_rw [memberSubfamily, mem_image, mem_filter]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ (∃ a_1, (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ erase a_1 a = s) ↔ insert a s ∈ 𝒜 ∧ ¬a ∈ s
[PROOFSTEP]
refine' ⟨_, fun h => ⟨insert a s, ⟨h.1, by simp⟩, erase_insert h.2⟩⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝒜 ∧ ¬a ∈ s
⊢ a ∈ insert a s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ (∃ a_1, (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ erase a_1 a = s) → insert a s ∈ 𝒜 ∧ ¬a ∈ s
[PROOFSTEP]
rintro ⟨s, ⟨hs1, hs2⟩, rfl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ insert a (erase s a) ∈ 𝒜 ∧ ¬a ∈ erase s a
[PROOFSTEP]
rw [insert_erase hs2]
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ s ∈ 𝒜 ∧ ¬a ∈ erase s a
[PROOFSTEP]
exact ⟨hs1, not_mem_erase _ _⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 ℬ : Finset (Finset α)
⊢ memberSubfamily a (𝒜 ∩ ℬ) = memberSubfamily a 𝒜 ∩ memberSubfamily a ℬ
[PROOFSTEP]
unfold memberSubfamily
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 ℬ : Finset (Finset α)
⊢ image (fun s => erase s a) (filter (fun s => a ∈ s) (𝒜 ∩ ℬ)) =
    image (fun s => erase s a) (filter (fun s => a ∈ s) 𝒜) ∩ image (fun s => erase s a) (filter (fun s => a ∈ s) ℬ)
[PROOFSTEP]
rw [filter_inter_distrib, image_inter_of_injOn _ _ ((erase_injOn' _).mono _)]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 ℬ : Finset (Finset α)
⊢ ↑(filter (fun s => a ∈ s) 𝒜) ∪ ↑(filter (fun s => a ∈ s) ℬ) ⊆ {s | a ∈ s}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 ℬ : Finset (Finset α)
⊢ memberSubfamily a (𝒜 ∪ ℬ) = memberSubfamily a 𝒜 ∪ memberSubfamily a ℬ
[PROOFSTEP]
simp_rw [memberSubfamily, filter_union, image_union]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
⊢ card (memberSubfamily a 𝒜) + card (nonMemberSubfamily a 𝒜) = card 𝒜
[PROOFSTEP]
rw [memberSubfamily, nonMemberSubfamily, card_image_of_injOn]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
⊢ card (filter (fun s => a ∈ s) 𝒜) + card (filter (fun s => ¬a ∈ s) 𝒜) = card 𝒜
[PROOFSTEP]
conv_rhs => rw [← filter_card_add_filter_neg_card_eq_card (fun s => (a ∈ s))]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
| card 𝒜
[PROOFSTEP]
rw [← filter_card_add_filter_neg_card_eq_card (fun s => (a ∈ s))]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
| card 𝒜
[PROOFSTEP]
rw [← filter_card_add_filter_neg_card_eq_card (fun s => (a ∈ s))]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
| card 𝒜
[PROOFSTEP]
rw [← filter_card_add_filter_neg_card_eq_card (fun s => (a ∈ s))]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
⊢ Set.InjOn (fun s => erase s a) ↑(filter (fun s => a ∈ s) 𝒜)
[PROOFSTEP]
apply (erase_injOn' _).mono
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
⊢ ↑(filter (fun s => a ∈ s) 𝒜) ⊆ {s | a ∈ s}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
⊢ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 = image (fun s => erase s a) 𝒜
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 ↔ s ∈ image (fun s => erase s a) 𝒜
[PROOFSTEP]
simp only [mem_union, mem_memberSubfamily, mem_nonMemberSubfamily, mem_image, exists_prop]
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ ¬a ∈ s ∨ s ∈ 𝒜 ∧ ¬a ∈ s ↔ ∃ a_1, a_1 ∈ 𝒜 ∧ erase a_1 a = s
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ ¬a ∈ s ∨ s ∈ 𝒜 ∧ ¬a ∈ s → ∃ a_2, a_2 ∈ 𝒜 ∧ erase a_2 a = s
[PROOFSTEP]
rintro (h | h)
[GOAL]
case a.mp.inl
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
h : insert a s ∈ 𝒜 ∧ ¬a ∈ s
⊢ ∃ a_1, a_1 ∈ 𝒜 ∧ erase a_1 a = s
[PROOFSTEP]
exact ⟨_, h.1, erase_insert h.2⟩
[GOAL]
case a.mp.inr
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝒜 ∧ ¬a ∈ s
⊢ ∃ a_1, a_1 ∈ 𝒜 ∧ erase a_1 a = s
[PROOFSTEP]
exact ⟨_, h.1, erase_eq_of_not_mem h.2⟩
[GOAL]
case a.mpr
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ a_1, a_1 ∈ 𝒜 ∧ erase a_1 a = s) → insert a s ∈ 𝒜 ∧ ¬a ∈ s ∨ s ∈ 𝒜 ∧ ¬a ∈ s
[PROOFSTEP]
rintro ⟨s, hs, rfl⟩
[GOAL]
case a.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
⊢ insert a (erase s a) ∈ 𝒜 ∧ ¬a ∈ erase s a ∨ erase s a ∈ 𝒜 ∧ ¬a ∈ erase s a
[PROOFSTEP]
by_cases ha : a ∈ s
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (erase s a) ∈ 𝒜 ∧ ¬a ∈ erase s a ∨ erase s a ∈ 𝒜 ∧ ¬a ∈ erase s a
[PROOFSTEP]
exact Or.inl ⟨by rwa [insert_erase ha], not_mem_erase _ _⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (erase s a) ∈ 𝒜
[PROOFSTEP]
rwa [insert_erase ha]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : ¬a ∈ s
⊢ insert a (erase s a) ∈ 𝒜 ∧ ¬a ∈ erase s a ∨ erase s a ∈ 𝒜 ∧ ¬a ∈ erase s a
[PROOFSTEP]
exact Or.inr ⟨by rwa [erase_eq_of_not_mem ha], not_mem_erase _ _⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : ¬a ∈ s
⊢ erase s a ∈ 𝒜
[PROOFSTEP]
rwa [erase_eq_of_not_mem ha]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ memberSubfamily a (memberSubfamily a 𝒜) = ∅
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
a✝ : Finset α
⊢ a✝ ∈ memberSubfamily a (memberSubfamily a 𝒜) ↔ a✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ memberSubfamily a (nonMemberSubfamily a 𝒜) = ∅
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
a✝ : Finset α
⊢ a✝ ∈ memberSubfamily a (nonMemberSubfamily a 𝒜) ↔ a✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ nonMemberSubfamily a (memberSubfamily a 𝒜) = memberSubfamily a 𝒜
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
a✝ : Finset α
⊢ a✝ ∈ nonMemberSubfamily a (memberSubfamily a 𝒜) ↔ a✝ ∈ memberSubfamily a 𝒜
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ nonMemberSubfamily a (nonMemberSubfamily a 𝒜) = nonMemberSubfamily a 𝒜
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
a✝ : Finset α
⊢ a✝ ∈ nonMemberSubfamily a (nonMemberSubfamily a 𝒜) ↔ a✝ ∈ nonMemberSubfamily a 𝒜
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
h₁ : s ∈ filter (fun s => erase s a ∈ 𝒜) 𝒜
h₂ : s ∈ filter (fun s => ¬s ∈ 𝒜) (image (fun s => erase s a) 𝒜)
⊢ False
[PROOFSTEP]
have := (mem_filter.1 h₂).2
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
h₁ : s ∈ filter (fun s => erase s a ∈ 𝒜) 𝒜
h₂ : s ∈ filter (fun s => ¬s ∈ 𝒜) (image (fun s => erase s a) 𝒜)
this : ¬s ∈ 𝒜
⊢ False
[PROOFSTEP]
exact this (mem_filter.1 h₁).1
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝓓 a 𝒜 ↔ s ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ ¬s ∈ 𝒜 ∧ insert a s ∈ 𝒜
[PROOFSTEP]
simp_rw [compression, mem_disjUnion, mem_filter, mem_image, and_comm (a := (¬s ∈ 𝒜))]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ (∃ a_1, a_1 ∈ 𝒜 ∧ erase a_1 a = s) ∧ ¬s ∈ 𝒜 ↔ s ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ insert a s ∈ 𝒜 ∧ ¬s ∈ 𝒜
[PROOFSTEP]
refine'
  or_congr_right
    (and_congr_left fun hs => ⟨_, fun h => ⟨_, h, erase_insert <| insert_ne_self.1 <| ne_of_mem_of_not_mem h hs⟩⟩)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
hs : ¬s ∈ 𝒜
⊢ (∃ a_1, a_1 ∈ 𝒜 ∧ erase a_1 a = s) → insert a s ∈ 𝒜
[PROOFSTEP]
rintro ⟨t, ht, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
a : α
t : Finset α
ht : t ∈ 𝒜
hs : ¬erase t a ∈ 𝒜
⊢ insert a (erase t a) ∈ 𝒜
[PROOFSTEP]
rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem ht hs).symm)]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ erase s a ∈ 𝓓 a 𝒜
[PROOFSTEP]
simp_rw [mem_compression, erase_idem, and_self_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ erase s a ∈ 𝒜 ∨ ¬erase s a ∈ 𝒜 ∧ insert a (erase s a) ∈ 𝒜
[PROOFSTEP]
refine' (em _).imp_right fun h => ⟨h, _⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
h : ¬erase s a ∈ 𝒜
⊢ insert a (erase s a) ∈ 𝒜
[PROOFSTEP]
rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem hs h).symm)]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝓓 a 𝒜 → erase s a ∈ 𝓓 a 𝒜
[PROOFSTEP]
simp_rw [mem_compression, erase_idem]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ ¬s ∈ 𝒜 ∧ insert a s ∈ 𝒜 →
    erase s a ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ ¬erase s a ∈ 𝒜 ∧ insert a (erase s a) ∈ 𝒜
[PROOFSTEP]
refine' Or.imp (fun h => ⟨h.2, h.2⟩) fun h => _
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h : ¬s ∈ 𝒜 ∧ insert a s ∈ 𝒜
⊢ ¬erase s a ∈ 𝒜 ∧ insert a (erase s a) ∈ 𝒜
[PROOFSTEP]
rwa [erase_eq_of_not_mem (insert_ne_self.1 <| ne_of_mem_of_not_mem h.2 h.1)]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜
[PROOFSTEP]
by_cases ha : a ∈ s
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∈ s
⊢ s ∈ 𝓓 a 𝒜
[PROOFSTEP]
rwa [insert_eq_of_mem ha] at h
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : ¬a ∈ s
⊢ s ∈ 𝓓 a 𝒜
[PROOFSTEP]
rw [← erase_insert ha]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : ¬a ∈ s
⊢ erase (insert a s) a ∈ 𝓓 a 𝒜
[PROOFSTEP]
exact erase_mem_compression_of_mem_compression h
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
⊢ 𝓓 a (𝓓 a 𝒜) = 𝓓 a 𝒜
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝓓 a (𝓓 a 𝒜) ↔ s ∈ 𝓓 a 𝒜
[PROOFSTEP]
refine' mem_compression.trans ⟨_, fun h => Or.inl ⟨h, erase_mem_compression_of_mem_compression h⟩⟩
[GOAL]
case a
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝓓 a 𝒜 ∧ erase s a ∈ 𝓓 a 𝒜 ∨ ¬s ∈ 𝓓 a 𝒜 ∧ insert a s ∈ 𝓓 a 𝒜 → s ∈ 𝓓 a 𝒜
[PROOFSTEP]
rintro (h | h)
[GOAL]
case a.inl
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝓓 a 𝒜 ∧ erase s a ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜
[PROOFSTEP]
exact h.1
[GOAL]
case a.inr
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
h : ¬s ∈ 𝓓 a 𝒜 ∧ insert a s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜
[PROOFSTEP]
cases h.1 (mem_compression_of_insert_mem_compression h.2)
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
⊢ card (𝓓 a 𝒜) = card 𝒜
[PROOFSTEP]
rw [compression, card_disjUnion, image_filter, card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ←
  card_disjoint_union]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
⊢ card (filter (fun s => erase s a ∈ 𝒜) 𝒜 ∪ filter ((fun s => ¬s ∈ 𝒜) ∘ fun s => erase s a) 𝒜) = card 𝒜
[PROOFSTEP]
conv_rhs => rw [← filter_union_filter_neg_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
| card 𝒜
[PROOFSTEP]
rw [← filter_union_filter_neg_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
| card 𝒜
[PROOFSTEP]
rw [← filter_union_filter_neg_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
| card 𝒜
[PROOFSTEP]
rw [← filter_union_filter_neg_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
⊢ Disjoint (filter (fun s => erase s a ∈ 𝒜) 𝒜) (filter ((fun s => ¬s ∈ 𝒜) ∘ fun s => erase s a) 𝒜)
[PROOFSTEP]
exact disjoint_filter_filter_neg 𝒜 𝒜 (fun s => (erase s a ∈ 𝒜))
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
⊢ ∀ (s : Finset α), s ∈ ↑(filter ((fun s => ¬s ∈ 𝒜) ∘ fun s => erase s a) 𝒜) → s ∈ {s | a ∈ s}
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ ↑(filter ((fun s => ¬s ∈ 𝒜) ∘ fun s => erase s a) 𝒜)
⊢ s ∈ {s | a ∈ s}
[PROOFSTEP]
rw [mem_coe, mem_filter, Function.comp_apply] at hs
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜 ∧ ¬erase s a ∈ 𝒜
⊢ s ∈ {s | a ∈ s}
[PROOFSTEP]
exact not_imp_comm.1 erase_eq_of_not_mem (ne_of_mem_of_not_mem hs.1 hs.2).symm


[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂ 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
simp only [shadow, mem_sup, mem_image]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂ 𝒜 ↔ ∃ a x, insert a s ∈ 𝒜
[PROOFSTEP]
refine' mem_shadow_iff.trans ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s) → ∃ a x, insert a s ∈ 𝒜
[PROOFSTEP]
rintro ⟨s, hs, a, ha, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : a ∈ s
⊢ ∃ a_1 x, insert a_1 (erase s a) ∈ 𝒜
[PROOFSTEP]
refine' ⟨a, not_mem_erase a s, _⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : a ∈ s
⊢ insert a (erase s a) ∈ 𝒜
[PROOFSTEP]
rwa [insert_erase ha]
[GOAL]
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ a x, insert a s ∈ 𝒜) → ∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
rintro ⟨a, ha, hs⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a✝ : α
k r : ℕ
a : α
ha : ¬a ∈ s
hs : insert a s ∈ 𝒜
⊢ ∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
exact ⟨insert a s, hs, a, mem_insert_self _ _, erase_insert ha⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized (r - 1) ↑(∂ 𝒜)
[PROOFSTEP]
intro A h
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
h : A ∈ ↑(∂ 𝒜)
⊢ card A = r - 1
[PROOFSTEP]
obtain ⟨A, hA, i, hi, rfl⟩ := mem_shadow_iff.1 h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∈ A
h : erase A i ∈ ↑(∂ 𝒜)
⊢ card (erase A i) = r - 1
[PROOFSTEP]
rw [card_erase_of_mem hi, h𝒜 hA]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h : ¬∅ ∈ 𝒜
⊢ Set.Sized r ↑(∂ 𝒜) ↔ Set.Sized (r + 1) ↑𝒜
[PROOFSTEP]
refine' ⟨fun h𝒜 s hs => _, Set.Sized.shadow⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
h : ¬∅ ∈ 𝒜
h𝒜 : Set.Sized r ↑(∂ 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
⊢ card s = r + 1
[PROOFSTEP]
obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 (ne_of_mem_of_not_mem hs h)
[GOAL]
case intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a✝ : α
k r : ℕ
h : ¬∅ ∈ 𝒜
h𝒜 : Set.Sized r ↑(∂ 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
a : α
ha : a ∈ s
⊢ card s = r + 1
[PROOFSTEP]
rw [← h𝒜 (erase_mem_shadow hs ha), card_erase_add_one ha]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂ 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1
[PROOFSTEP]
refine' mem_shadow_iff_insert_mem.trans ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ a x, insert a s ∈ 𝒜) → ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1
[PROOFSTEP]
rintro ⟨a, ha, hs⟩
[GOAL]
case refine'_1.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a✝ : α
k r : ℕ
a : α
ha : ¬a ∈ s
hs : insert a s ∈ 𝒜
⊢ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1
[PROOFSTEP]
exact ⟨insert a s, hs, subset_insert _ _, card_insert_of_not_mem ha⟩
[GOAL]
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1) → ∃ a x, insert a s ∈ 𝒜
[PROOFSTEP]
rintro ⟨t, ht, hst, h⟩
[GOAL]
case refine'_2.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
⊢ ∃ a x, insert a s ∈ 𝒜
[PROOFSTEP]
obtain ⟨a, ha⟩ : ∃ a, t \ s = { a } := card_eq_one.1 (by rw [card_sdiff hst, h, add_tsub_cancel_left])
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
⊢ card (t \ s) = 1
[PROOFSTEP]
rw [card_sdiff hst, h, add_tsub_cancel_left]
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
a : α
ha : t \ s = {a}
⊢ ∃ a x, insert a s ∈ 𝒜
[PROOFSTEP]
exact
  ⟨a, fun hat => not_mem_sdiff_of_mem_right hat (ha.superset <| mem_singleton_self a), by
    rwa [insert_eq a s, ← ha, sdiff_union_of_subset hst]⟩
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
a : α
ha : t \ s = {a}
⊢ insert a s ∈ 𝒜
[PROOFSTEP]
rwa [insert_eq a s, ← ha, sdiff_union_of_subset hst]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
[PROOFSTEP]
induction' k with k ih generalizing 𝒜 s
[GOAL]
case zero
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂ ^[zero] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + zero
[PROOFSTEP]
refine' ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, _⟩
[GOAL]
case zero
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + zero) → s ∈ ∂ ^[zero] 𝒜
[PROOFSTEP]
rintro ⟨t, ht, hst, hcard⟩
[GOAL]
case zero.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + zero
⊢ s ∈ ∂ ^[zero] 𝒜
[PROOFSTEP]
rwa [eq_of_subset_of_card_le hst hcard.le]
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂ ^[succ k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
simp only [exists_prop, Function.comp_apply, Function.iterate_succ]
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂ ^[k] (∂ 𝒜) ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
refine' ih.trans _
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k) ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
clear ih
[GOAL]
case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k) ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
constructor
[GOAL]
case succ.mp
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k) → ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
rintro ⟨t, ht, hst, hcardst⟩
[GOAL]
case succ.mp.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂ 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
⊢ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
obtain ⟨u, hu, htu, hcardtu⟩ := mem_shadow_iff_exists_mem_card_add_one.1 ht
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂ 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
hcardtu : card u = card t + 1
⊢ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k
[PROOFSTEP]
refine' ⟨u, hu, hst.trans htu, _⟩
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂ 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
hcardtu : card u = card t + 1
⊢ card u = card s + succ k
[PROOFSTEP]
rw [hcardtu, hcardst]
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂ 𝒜
hst : s ⊆ t
hcardst : card t = card s + k
u : Finset α
hu : u ∈ 𝒜
htu : t ⊆ u
hcardtu : card u = card t + 1
⊢ card s + k + 1 = card s + succ k
[PROOFSTEP]
rfl
[GOAL]
case succ.mpr
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + succ k) → ∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
[PROOFSTEP]
rintro ⟨t, ht, hst, hcard⟩
[GOAL]
case succ.mpr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
⊢ ∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
[PROOFSTEP]
obtain ⟨u, hsu, hut, hu⟩ :=
  Finset.exists_intermediate_set k
    (by
      rw [add_comm, hcard]
      exact le_succ _)
    hst
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
⊢ k + card s ≤ card t
[PROOFSTEP]
rw [add_comm, hcard]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
⊢ card s + k ≤ card s + succ k
[PROOFSTEP]
exact le_succ _
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = k + card s
⊢ ∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
[PROOFSTEP]
rw [add_comm] at hu
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = card s + k
⊢ ∃ t, t ∈ ∂ 𝒜 ∧ s ⊆ t ∧ card t = card s + k
[PROOFSTEP]
refine' ⟨u, mem_shadow_iff_exists_mem_card_add_one.2 ⟨t, ht, hut, _⟩, hsu, hu⟩
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = card s + k
⊢ card t = card u + 1
[PROOFSTEP]
rw [hcard, hu]
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
hcard : card t = card s + succ k
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : card u = card s + k
⊢ card s + succ k = card s + k + 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂⁺ 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ ∃ a x, insert a t = s
[PROOFSTEP]
simp_rw [upShadow, mem_sup, mem_image, exists_prop, mem_compl]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized (r + 1) ↑(∂⁺ 𝒜)
[PROOFSTEP]
intro A h
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
h : A ∈ ↑(∂⁺ 𝒜)
⊢ card A = r + 1
[PROOFSTEP]
obtain ⟨A, hA, i, hi, rfl⟩ := mem_upShadow_iff.1 h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : ¬i ∈ A
h : insert i A ∈ ↑(∂⁺ 𝒜)
⊢ card (insert i A) = r + 1
[PROOFSTEP]
rw [card_insert_of_not_mem hi, h𝒜 hA]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂⁺ 𝒜 ↔ ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
[PROOFSTEP]
refine' mem_upShadow_iff.trans ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ ∃ a x, insert a t = s) → ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
[PROOFSTEP]
rintro ⟨s, hs, a, ha, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : ¬a ∈ s
⊢ ∃ a_1, a_1 ∈ insert a s ∧ erase (insert a s) a_1 ∈ 𝒜
[PROOFSTEP]
refine' ⟨a, mem_insert_self a s, _⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : ¬a ∈ s
⊢ erase (insert a s) a ∈ 𝒜
[PROOFSTEP]
rwa [erase_insert ha]
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ a, a ∈ s ∧ erase s a ∈ 𝒜) → ∃ t, t ∈ 𝒜 ∧ ∃ a x, insert a t = s
[PROOFSTEP]
rintro ⟨a, ha, hs⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a✝ : α
k r : ℕ
a : α
ha : a ∈ s
hs : erase s a ∈ 𝒜
⊢ ∃ t, t ∈ 𝒜 ∧ ∃ a x, insert a t = s
[PROOFSTEP]
exact ⟨s.erase a, hs, a, not_mem_erase _ _, insert_erase ha⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂⁺ 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s
[PROOFSTEP]
refine' mem_upShadow_iff_erase_mem.trans ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ a, a ∈ s ∧ erase s a ∈ 𝒜) → ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s
[PROOFSTEP]
rintro ⟨a, ha, hs⟩
[GOAL]
case refine'_1.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a✝ : α
k r : ℕ
a : α
ha : a ∈ s
hs : erase s a ∈ 𝒜
⊢ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s
[PROOFSTEP]
exact ⟨s.erase a, hs, erase_subset _ _, card_erase_add_one ha⟩
[GOAL]
case refine'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s) → ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
[PROOFSTEP]
rintro ⟨t, ht, hts, h⟩
[GOAL]
case refine'_2.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
⊢ ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
[PROOFSTEP]
obtain ⟨a, ha⟩ : ∃ a, s \ t = { a } := card_eq_one.1 (by rw [card_sdiff hts, ← h, add_tsub_cancel_left])
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
⊢ card (s \ t) = 1
[PROOFSTEP]
rw [card_sdiff hts, ← h, add_tsub_cancel_left]
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
a : α
ha : s \ t = {a}
⊢ ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
[PROOFSTEP]
refine' ⟨a, sdiff_subset _ _ ((ha.ge : _ ⊆ _) <| mem_singleton_self a), _⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
a : α
ha : s \ t = {a}
⊢ erase s a ∈ 𝒜
[PROOFSTEP]
rwa [← sdiff_singleton_eq_erase, ← ha, sdiff_sdiff_eq_self hts]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
[PROOFSTEP]
induction' k with k ih generalizing 𝒜 s
[GOAL]
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[zero] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + zero = card s
[PROOFSTEP]
refine' ⟨fun hs => ⟨s, hs, Subset.refl _, rfl⟩, _⟩
[GOAL]
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + zero = card s) → s ∈ ∂⁺ ^[zero] 𝒜
[PROOFSTEP]
rintro ⟨t, ht, hst, hcard⟩
[GOAL]
case zero.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k r : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hst : t ⊆ s
hcard : card t + zero = card s
⊢ s ∈ ∂⁺ ^[zero] 𝒜
[PROOFSTEP]
rwa [← eq_of_subset_of_card_le hst hcard.ge]
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[succ k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
simp only [exists_prop, Function.comp_apply, Function.iterate_succ]
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ ^[k] (∂⁺ 𝒜) ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
refine' ih.trans _
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
ih : ∀ {𝒜 : Finset (Finset α)} {s : Finset α}, s ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s) ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
clear ih
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s) ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
constructor
[GOAL]
case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s) → ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
rintro ⟨t, ht, hts, hcardst⟩
[GOAL]
case succ.mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : card t + k = card s
⊢ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
obtain ⟨u, hu, hut, hcardtu⟩ := mem_upShadow_iff_exists_mem_card_add_one.1 ht
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : card t + k = card s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : card u + 1 = card t
⊢ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s
[PROOFSTEP]
refine' ⟨u, hu, hut.trans hts, _⟩
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : card t + k = card s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : card u + 1 = card t
⊢ card u + succ k = card s
[PROOFSTEP]
rw [← hcardst, ← hcardtu, add_right_comm]
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ ∂⁺ 𝒜
hts : t ⊆ s
hcardst : card t + k = card s
u : Finset α
hu : u ∈ 𝒜
hut : u ⊆ t
hcardtu : card u + 1 = card t
⊢ card u + succ k = card u + k + 1
[PROOFSTEP]
rfl
[GOAL]
case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + succ k = card s) → ∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
[PROOFSTEP]
rintro ⟨t, ht, hts, hcard⟩
[GOAL]
case succ.mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
⊢ ∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
[PROOFSTEP]
obtain ⟨u, htu, hus, hu⟩ :=
  Finset.exists_intermediate_set 1
    (by
      rw [add_comm, ← hcard]
      exact add_le_add_left (succ_le_of_lt (zero_lt_succ _)) _)
    hts
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
⊢ 1 + card t ≤ card s
[PROOFSTEP]
rw [add_comm, ← hcard]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
⊢ card t + 1 ≤ card t + succ k
[PROOFSTEP]
exact add_le_add_left (succ_le_of_lt (zero_lt_succ _)) _
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : card u = 1 + card t
⊢ ∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
[PROOFSTEP]
rw [add_comm] at hu
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : card u = card t + 1
⊢ ∃ t, t ∈ ∂⁺ 𝒜 ∧ t ⊆ s ∧ card t + k = card s
[PROOFSTEP]
refine' ⟨u, mem_upShadow_iff_exists_mem_card_add_one.2 ⟨t, ht, htu, hu.symm⟩, hus, _⟩
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : card u = card t + 1
⊢ card u + k = card s
[PROOFSTEP]
rw [hu, ← hcard, add_right_comm]
[GOAL]
case succ.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜✝ : Finset (Finset α)
s✝ t✝ : Finset α
a : α
k✝ r k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : card t + succ k = card s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : card u = card t + 1
⊢ card t + k + 1 = card t + succ k
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ image compl (∂ 𝒜) = ∂⁺ (image compl 𝒜)
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ s ∈ image compl (∂ 𝒜) ↔ s ∈ ∂⁺ (image compl 𝒜)
[PROOFSTEP]
simp only [mem_image, exists_prop, mem_shadow_iff, mem_upShadow_iff]
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ (∃ a, (∃ t, t ∈ 𝒜 ∧ ∃ a_1, a_1 ∈ t ∧ erase t a_1 = a) ∧ aᶜ = s) ↔
    ∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a, ¬a ∈ t ∧ insert a t = s
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ (∃ a, (∃ t, t ∈ 𝒜 ∧ ∃ a_1, a_1 ∈ t ∧ erase t a_1 = a) ∧ aᶜ = s) →
    ∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a, ¬a ∈ t ∧ insert a t = s
[PROOFSTEP]
rintro ⟨_, ⟨s, hs, a, ha, rfl⟩, rfl⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : a ∈ s
⊢ ∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a_1, ¬a_1 ∈ t ∧ insert a_1 t = (erase s a)ᶜ
[PROOFSTEP]
exact ⟨sᶜ, ⟨s, hs, rfl⟩, a, not_mem_compl.2 ha, compl_erase.symm⟩
[GOAL]
case a.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ (∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a, ¬a ∈ t ∧ insert a t = s) →
    ∃ a, (∃ t, t ∈ 𝒜 ∧ ∃ a_1, a_1 ∈ t ∧ erase t a_1 = a) ∧ aᶜ = s
[PROOFSTEP]
rintro ⟨_, ⟨s, hs, rfl⟩, a, ha, rfl⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : ¬a ∈ sᶜ
⊢ ∃ a_1, (∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = a_1) ∧ a_1ᶜ = insert a sᶜ
[PROOFSTEP]
exact ⟨s.erase a, ⟨s, hs, a, not_mem_compl.1 ha, rfl⟩, compl_erase⟩
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ image compl (∂⁺ 𝒜) = ∂ (image compl 𝒜)
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ s ∈ image compl (∂⁺ 𝒜) ↔ s ∈ ∂ (image compl 𝒜)
[PROOFSTEP]
simp only [mem_image, exists_prop, mem_shadow_iff, mem_upShadow_iff]
[GOAL]
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ (∃ a, (∃ t, t ∈ 𝒜 ∧ ∃ a_1, ¬a_1 ∈ t ∧ insert a_1 t = a) ∧ aᶜ = s) ↔
    ∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ (∃ a, (∃ t, t ∈ 𝒜 ∧ ∃ a_1, ¬a_1 ∈ t ∧ insert a_1 t = a) ∧ aᶜ = s) →
    ∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a, a ∈ t ∧ erase t a = s
[PROOFSTEP]
rintro ⟨_, ⟨s, hs, a, ha, rfl⟩, rfl⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : ¬a ∈ s
⊢ ∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a_1, a_1 ∈ t ∧ erase t a_1 = (insert a s)ᶜ
[PROOFSTEP]
exact ⟨sᶜ, ⟨s, hs, rfl⟩, a, mem_compl.2 ha, compl_insert.symm⟩
[GOAL]
case a.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
s : Finset α
⊢ (∃ t, (∃ a, a ∈ 𝒜 ∧ aᶜ = t) ∧ ∃ a, a ∈ t ∧ erase t a = s) →
    ∃ a, (∃ t, t ∈ 𝒜 ∧ ∃ a_1, ¬a_1 ∈ t ∧ insert a_1 t = a) ∧ aᶜ = s
[PROOFSTEP]
rintro ⟨_, ⟨s, hs, rfl⟩, a, ha, rfl⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : a ∈ sᶜ
⊢ ∃ a_1, (∃ t, t ∈ 𝒜 ∧ ∃ a, ¬a ∈ t ∧ insert a t = a_1) ∧ a_1ᶜ = erase sᶜ a
[PROOFSTEP]
exact ⟨insert a s, ⟨s, hs, a, mem_compl.1 ha, rfl⟩, compl_insert⟩