α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ erase s a ∈ 𝒜 ∨ ¬erase s a ∈ 𝒜 ∧ insert a (erase s a) ∈ 𝒜
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ erase s a ∈ 𝓓 a 𝒜
simp_rw [mem_compression, erase_idem, and_self_iff]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
h : ¬erase s a ∈ 𝒜
⊢ insert a (erase s a) ∈ 𝒜
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ erase s a ∈ 𝒜 ∨ ¬erase s a ∈ 𝒜 ∧ insert a (erase s a) ∈ 𝒜
refine' (em _).imp_right fun h => ⟨h, _⟩
no goals
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
h : ¬erase s a ∈ 𝒜
⊢ insert a (erase s a) ∈ 𝒜
rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem hs h).symm)]