α : Type u_1
β : Type ?u.77478
γ : Type ?u.77481
s✝ t s : Set α
inst✝¹ inst✝ : Fintype ↑s
⊢ toFinset s = toFinset s
α : Type u_1
β : Type ?u.77478
γ : Type ?u.77481
s✝ t✝ s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s = t
⊢ toFinset s = toFinset t
subst h
case h.e_3.h
α : Type u_1
β : Type ?u.77478
γ : Type ?u.77481
s✝ t s : Set α
inst✝¹ inst✝ : Fintype ↑s
⊢ inst✝¹ = inst✝
α : Type u_1
β : Type ?u.77478
γ : Type ?u.77481
s✝ t s : Set α
inst✝¹ inst✝ : Fintype ↑s
⊢ toFinset s = toFinset s
congr
no goals
case h.e_3.h
α : Type u_1
β : Type ?u.77478
γ : Type ?u.77481
s✝ t s : Set α
inst✝¹ inst✝ : Fintype ↑s
⊢ inst✝¹ = inst✝
exact Subsingleton.elim _ _