α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
⊢ ↑f x = ↑f (↑f.symm y) ↔ x = ↑f.symm y
α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
⊢ ↑f x = y ↔ x = ↑f.symm y
conv_lhs => rw [← apply_symm_apply f y]
no goals
α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
⊢ ↑f x = ↑f (↑f.symm y) ↔ x = ↑f.symm y
rw [apply_eq_iff_eq]