α : Type u_2
β : Type u_1
r✝ : Setoid α
f✝ f : α → β
r : Setoid β
x y : α
⊢ Setoid.r x y ↔ f x ≈ f y
α : Type u_2
β : Type u_1
r✝ : Setoid α
f✝ f : α → β
r : Setoid β
x y : α
⊢ Setoid.r x y ↔ Quotient.mk r (f x) = Quotient.mk r (f y)
rw [Quotient.eq]
no goals
α : Type u_2
β : Type u_1
r✝ : Setoid α
f✝ f : α → β
r : Setoid β
x y : α
⊢ Setoid.r x y ↔ f x ≈ f y
rfl