no goals
F : Type ?u.81630
α : Type u_1
β : Type u_2
γ : Type ?u.81639
δ : Type ?u.81642
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
e e' : α ≃o β
h : symm e = symm e'
⊢ e = e'
rw [← e.symm_symm, h, e'.symm_symm]