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) 𝒜
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
⊢ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 = image (fun s => erase s a) 𝒜
ext s
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
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) 𝒜
simp only [mem_union, mem_memberSubfamily, mem_nonMemberSubfamily, mem_image, exists_prop]
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

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
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
constructor
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

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
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
rintro (h | h)
no goals
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
exact ⟨_, h.1, erase_insert h.2⟩
no goals
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
exact ⟨_, h.1, erase_eq_of_not_mem h.2⟩
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
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
rintro ⟨s, hs, rfl⟩
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

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
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
by_cases ha : a ∈ s
no goals
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
exact Or.inl ⟨by rwa [insert_erase ha], not_mem_erase _ _⟩
no goals
α : 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) ∈ 𝒜
rwa [insert_erase ha]
no goals
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
exact Or.inr ⟨by rwa [erase_eq_of_not_mem ha], not_mem_erase _ _⟩
no goals
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
s✝ : Finset α
a✝ a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : ¬a ∈ s
⊢ erase s a ∈ 𝒜
rwa [erase_eq_of_not_mem ha]