α : Sort u_1
β : Sort ?u.34513
s : Setoid α
x : Quotient s
y : α
⊢ x = Quotient.mk s y ↔ Quotient.mk s (out x) = Quotient.mk s y
α : Sort u_1
β : Sort ?u.34513
s : Setoid α
x : Quotient s
y : α
⊢ x = Quotient.mk s y ↔ out x ≈ y
refine' Iff.trans _ Quotient.eq
no goals
α : Sort u_1
β : Sort ?u.34513
s : Setoid α
x : Quotient s
y : α
⊢ x = Quotient.mk s y ↔ Quotient.mk s (out x) = Quotient.mk s y
rw [Quotient.out_eq x]