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

case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1) → ∃ a x, insert a s ∈ 𝒜
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ s ∈ (∂ ) 𝒜 ↔ ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1
refine' mem_shadow_iff_insert_mem.trans ⟨_, _⟩
case refine'_1.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 ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ a x, insert a s ∈ 𝒜) → ∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1
rintro ⟨a, ha, hs⟩
no goals
case refine'_1.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 ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1
exact ⟨insert a s, hs, subset_insert _ _, card_insert_of_not_mem ha⟩
case refine'_2.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
⊢ ∃ a x, insert a s ∈ 𝒜
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
⊢ (∃ t, t ∈ 𝒜 ∧ s ⊆ t ∧ card t = card s + 1) → ∃ a x, insert a s ∈ 𝒜
rintro ⟨t, ht, hst, h⟩
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
a : α
ha : t \ s = {a}
⊢ ∃ a x, insert a s ∈ 𝒜
case refine'_2.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
⊢ ∃ a x, insert a s ∈ 𝒜
obtain ⟨a, ha⟩ : ∃ a, t \ s = {a} :=
  card_eq_one.1 (by rw [card_sdiff hst, h, add_tsub_cancel_left])
no goals
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
a : α
ha : t \ s = {a}
⊢ ∃ a x, insert a s ∈ 𝒜
exact
  ⟨a, fun hat => not_mem_sdiff_of_mem_right hat ((ha.ge : _ ⊆ _) <| mem_singleton_self a), by
    rwa [insert_eq a s, ← ha, sdiff_union_of_subset hst]⟩
no goals
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
⊢ card (t \ s) = 1
rw [card_sdiff hst, h, add_tsub_cancel_left]
no goals
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t✝ : Finset α
a✝ : α
k r : ℕ
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
h : card t = card s + 1
a : α
ha : t \ s = {a}
⊢ insert a s ∈ 𝒜
rwa [insert_eq a s, ← ha, sdiff_union_of_subset hst]