α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ (∃ a_1, a_1 ∈ 𝒜 ∧ erase a_1 a = s) ∧ ¬s ∈ 𝒜 ↔ s ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ insert a s ∈ 𝒜 ∧ ¬s ∈ 𝒜
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝓓 a 𝒜 ↔ s ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ ¬s ∈ 𝒜 ∧ insert a s ∈ 𝒜
simp_rw [compression, mem_disjUnion, mem_filter, mem_image, and_comm (a := (¬ s ∈ 𝒜))]
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
hs : ¬s ∈ 𝒜
⊢ (∃ a_1, a_1 ∈ 𝒜 ∧ erase a_1 a = s) → insert a s ∈ 𝒜
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ (∃ a_1, a_1 ∈ 𝒜 ∧ erase a_1 a = s) ∧ ¬s ∈ 𝒜 ↔ s ∈ 𝒜 ∧ erase s a ∈ 𝒜 ∨ insert a s ∈ 𝒜 ∧ ¬s ∈ 𝒜
refine'
  or_congr_right
    (and_congr_left fun hs =>
      ⟨_, fun h => ⟨_, h, erase_insert <| insert_ne_self.1 <| ne_of_mem_of_not_mem h hs⟩⟩)
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
a : α
t : Finset α
ht : t ∈ 𝒜
hs : ¬erase t a ∈ 𝒜
⊢ insert a (erase t a) ∈ 𝒜
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
a : α
hs : ¬s ∈ 𝒜
⊢ (∃ a_1, a_1 ∈ 𝒜 ∧ erase a_1 a = s) → insert a s ∈ 𝒜
rintro ⟨t, ht, rfl⟩
no goals
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
a : α
t : Finset α
ht : t ∈ 𝒜
hs : ¬erase t a ∈ 𝒜
⊢ insert a (erase t a) ∈ 𝒜
rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem ht hs).symm)]