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

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