α : Type u_1
β : Type ?u.136843
γ : Type ?u.136846
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ Set.toFinset s = Set.toFinset s
α : Type u_1
β : Type ?u.136843
γ : Type ?u.136846
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ ↑finsetEquivSet.symm s = Set.toFinset s
simp [finsetEquivSet]
case h.e_3.h
α : Type u_1
β : Type ?u.136843
γ : Type ?u.136846
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ (Subtype.fintype fun x => x ∈ s) = inst✝
α : Type u_1
β : Type ?u.136843
γ : Type ?u.136846
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ Set.toFinset s = Set.toFinset s
congr
no goals
case h.e_3.h
α : Type u_1
β : Type ?u.136843
γ : Type ?u.136846
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ (Subtype.fintype fun x => x ∈ s) = inst✝
exact Subsingleton.elim _ _