case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ∈ powersetLen (card s) s ↔ a✝ ∈ {s}
α : Type u_1
s✝ t s : Finset α
⊢ powersetLen (card s) s = {s}
ext
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ⊆ s ∧ card a✝ = card s ↔ a✝ = s
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ∈ powersetLen (card s) s ↔ a✝ ∈ {s}
rw [mem_powersetLen, mem_singleton]
case a.mp
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ⊆ s ∧ card a✝ = card s → a✝ = s

case a.mpr
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ = s → a✝ ⊆ s ∧ card a✝ = card s
case a
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ⊆ s ∧ card a✝ = card s ↔ a✝ = s
constructor
no goals
case a.mp
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ ⊆ s ∧ card a✝ = card s → a✝ = s
exact fun ⟨hs, hc⟩ => eq_of_subset_of_card_le hs hc.ge
case a.mpr
α : Type u_1
s t a✝ : Finset α
⊢ a✝ ⊆ a✝ ∧ card a✝ = card a✝
case a.mpr
α : Type u_1
s✝ t s a✝ : Finset α
⊢ a✝ = s → a✝ ⊆ s ∧ card a✝ = card s
rintro rfl
no goals
case a.mpr
α : Type u_1
s t a✝ : Finset α
⊢ a✝ ⊆ a✝ ∧ card a✝ = card a✝
simp