case h
α : Sort u_1
β : Sort u_2
e : α ≃ β
x✝ : α
⊢ ↑(Embedding.trans (Equiv.toEmbedding e) (Equiv.toEmbedding e.symm)) x✝ = ↑(Embedding.refl α) x✝
α : Sort u_1
β : Sort u_2
e : α ≃ β
⊢ Embedding.trans (Equiv.toEmbedding e) (Equiv.toEmbedding e.symm) = Embedding.refl α
ext
no goals
case h
α : Sort u_1
β : Sort u_2
e : α ≃ β
x✝ : α
⊢ ↑(Embedding.trans (Equiv.toEmbedding e) (Equiv.toEmbedding e.symm)) x✝ = ↑(Embedding.refl α) x✝
simp