no goals
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : (fun x => α) x
H : ↑e.symm x = y
⊢ x = ↑e y
simp [H.symm]
no goals
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : (fun x => α) x
H : x = ↑e y
⊢ ↑e.symm x = y
simp [H]