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

case refine'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s) → ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ (∂⁺ ) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s
refine' mem_upShadow_iff_erase_mem.trans ⟨_, _⟩
case refine'_1.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 ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s
case refine'_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ a, a ∈ s ∧ erase s a ∈ 𝒜) → ∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s
rintro ⟨a, ha, hs⟩
no goals
case refine'_1.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 ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s
exact ⟨s.erase a, hs, erase_subset _ _, card_erase_add_one ha⟩
case refine'_2.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card 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 : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ t ⊆ s ∧ card t + 1 = card s) → ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
rintro ⟨t, ht, hts, h⟩
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
a : α
ha : s \ t = {a}
⊢ ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
case refine'_2.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
⊢ ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
obtain ⟨a, ha⟩ : ∃ a, s \ t = {a} :=
  card_eq_one.1 (by rw [card_sdiff hts, ← h, add_tsub_cancel_left])
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
a : α
ha : s \ t = {a}
⊢ erase s a ∈ 𝒜
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
a : α
ha : s \ t = {a}
⊢ ∃ a, a ∈ s ∧ erase s a ∈ 𝒜
refine' ⟨a, sdiff_subset _ _ ((ha.ge : _ ⊆ _) <| mem_singleton_self a), _⟩
no goals
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
a : α
ha : s \ t = {a}
⊢ erase s a ∈ 𝒜
rwa [← sdiff_singleton_eq_erase, ← ha, sdiff_sdiff_eq_self hts]
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
h : card t + 1 = card s
⊢ card (s \ t) = 1
rw [card_sdiff hts, ← h, add_tsub_cancel_left]