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