α : 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) ℬ)
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ✝ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 ℬ : Finset (Finset α)
⊢ memberSubfamily a (𝒜 ∩ ℬ) = memberSubfamily a 𝒜 ∩ memberSubfamily a ℬ
unfold memberSubfamily
α : 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}
α : 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) ℬ)
rw [filter_inter_distrib, image_inter_of_injOn _ _ ((erase_injOn' _).mono _)]
no goals
α : 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}
simp