α : 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 𝒜

α : 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) 𝒜)

α : 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}
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
⊢ card (𝓓 a 𝒜) = card 𝒜
rw [compression, card_disjUnion, image_filter,
  card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ← card_disjoint_union]
α : 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}
α : 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}
intro s hs
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜 ∧ ¬erase s a ∈ 𝒜
⊢ s ∈ {s | a ∈ s}
α : 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}
rw [mem_coe, mem_filter, Function.comp_apply] at hs
no goals
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜 ∧ ¬erase s a ∈ 𝒜
⊢ s ∈ {s | a ∈ s}
exact not_imp_comm.1 erase_eq_of_not_mem (ne_of_mem_of_not_mem hs.1 hs.2).symm
no goals
α : 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 𝒜
conv_rhs => rw [← filter_union_filter_neg_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]
no goals
α : 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) 𝒜)
exact disjoint_filter_filter_neg 𝒜 𝒜 (fun s => (erase s a ∈ 𝒜))