α : 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
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ memberSubfamily a 𝒜 ↔ insert a s ∈ 𝒜 ∧ ¬a ∈ s
simp_rw [memberSubfamily, mem_image, mem_filter]
α : 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
α : 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
refine' ⟨_, fun h => ⟨insert a s, ⟨h.1, by simp⟩, erase_insert h.2⟩⟩
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
α : 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
rintro ⟨s, ⟨hs1, hs2⟩, rfl⟩
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ s ∈ 𝒜 ∧ ¬a ∈ erase s a
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
rw [insert_erase hs2]
no goals
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ s ∈ 𝒜 ∧ ¬a ∈ erase s a
exact ⟨hs1, not_mem_erase _ _⟩
no goals
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝒜 ∧ ¬a ∈ s
⊢ a ∈ insert a s
simp