no goals
α✝ : Type ?u.23858
β✝ : Type ?u.23861
γ : Type ?u.23864
inst✝² : Fintype α✝
s t : Finset α✝
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
e : α ≃ β
b : β
⊢ ↑(Equiv.toEmbedding e) (↑e.symm b) = b
simp