α : Type u_1
β : Type ?u.3949
γ : Type ?u.3952
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = card ↑p
α : Type u_1
β : Type ?u.3949
γ : Type ?u.3952
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = Finset.card s
rw [← card_ofFinset s H]
case h.e_2.h
α : Type u_1
β : Type ?u.3949
γ : Type ?u.3952
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ inst✝ = ofFinset s H
α : Type u_1
β : Type ?u.3949
γ : Type ?u.3952
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = card ↑p
congr
no goals
case h.e_2.h
α : Type u_1
β : Type ?u.3949
γ : Type ?u.3952
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ inst✝ = ofFinset s H
apply Subsingleton.elim