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