[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
