α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
h : ¬∅ ∈ 𝒜
h𝒜 : Set.Sized r ↑((∂ ) 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
⊢ card s = r + 1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
a : α
k r : ℕ
h : ¬∅ ∈ 𝒜
⊢ Set.Sized r ↑((∂ ) 𝒜) ↔ Set.Sized (r + 1) ↑𝒜
refine' ⟨fun h𝒜 s hs => _, Set.Sized.shadow⟩
case intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a✝ : α
k r : ℕ
h : ¬∅ ∈ 𝒜
h𝒜 : Set.Sized r ↑((∂ ) 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
a : α
ha : a ∈ s
⊢ card s = r + 1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a : α
k r : ℕ
h : ¬∅ ∈ 𝒜
h𝒜 : Set.Sized r ↑((∂ ) 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
⊢ card s = r + 1
obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 (ne_of_mem_of_not_mem hs h)
no goals
case intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s✝ t : Finset α
a✝ : α
k r : ℕ
h : ¬∅ ∈ 𝒜
h𝒜 : Set.Sized r ↑((∂ ) 𝒜)
s : Finset α
hs : s ∈ ↑𝒜
a : α
ha : a ∈ s
⊢ card s = r + 1
rw [← h𝒜 (erase_mem_shadow hs ha), card_erase_add_one ha]