α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ ¬s ∈ 𝒜 ∧ insert a s ∈ 𝒜 →
    erase s a ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ ¬erase s a ∈ 𝒜 ∧ insert a (erase s a) ∈ 𝒜
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝓓 a 𝒜 → erase s a ∈ 𝓓 a 𝒜
simp_rw [mem_compression, erase_idem]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h : ¬s ∈ 𝒜 ∧ insert a s ∈ 𝒜
⊢ ¬erase s a ∈ 𝒜 ∧ insert a (erase s a) ∈ 𝒜
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ ¬s ∈ 𝒜 ∧ insert a s ∈ 𝒜 →
    erase s a ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ ¬erase s a ∈ 𝒜 ∧ insert a (erase s a) ∈ 𝒜
refine' Or.imp (fun h => ⟨h.2, h.2⟩) fun h => _
no goals
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
h : ¬s ∈ 𝒜 ∧ insert a s ∈ 𝒜
⊢ ¬erase s a ∈ 𝒜 ∧ insert a (erase s a) ∈ 𝒜
rwa [erase_eq_of_not_mem (insert_ne_self.1 <| ne_of_mem_of_not_mem h.2 h.1)]