case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s) → ∃ a x, insert a s ∈ 𝒜

case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ a x, insert a s ∈ 𝒜) → ∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ (∂ ) 𝒜 ↔ ∃ a x, insert a s ∈ 𝒜
refine' mem_shadow_iff.trans ⟨_, _⟩
case refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : a ∈ s
⊢ ∃ a_1 x, insert a_1 (erase s a) ∈ 𝒜
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s) → ∃ a x, insert a s ∈ 𝒜
rintro ⟨s, hs, a, ha, rfl⟩
case refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : a ∈ s
⊢ insert a (erase s a) ∈ 𝒜
case refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : a ∈ s
⊢ ∃ a_1 x, insert a_1 (erase s a) ∈ 𝒜
refine' ⟨a, not_mem_erase a s, _⟩
no goals
case refine'_1.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
a✝ : α
k r : ℕ
s : Finset α
hs : s ∈ 𝒜
a : α
ha : a ∈ s
⊢ insert a (erase s a) ∈ 𝒜
rwa [insert_erase ha]
case refine'_2.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a✝ : α
k r : ℕ
a : α
ha : ¬a ∈ s
hs : insert a s ∈ 𝒜
⊢ ∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ a x, insert a s ∈ 𝒜) → ∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s
rintro ⟨a, ha, hs⟩
no goals
case refine'_2.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a✝ : α
k r : ℕ
a : α
ha : ¬a ∈ s
hs : insert a s ∈ 𝒜
⊢ ∃ t, t ∈ 𝒜 ∧ ∃ a, a ∈ t ∧ erase t a = s
exact ⟨insert a s, hs, a, mem_insert_self _ _, erase_insert ha⟩