proof for quotient.mk

Stream: general

[ZHAO Jinxiang]

example {α: Type*}  (s: setoid α) (a b: α) : @quotient.mk _ s a = @quotient.mk _ s b ↔ setoid.r a b :=
begin
  finish,
end

Can we proof it step by step? I don't know what happen in it.

[Eric Wieser]

docs#quotient.eq is a proof of exactly that statement (with different notation on the right)

[Eric Wieser]

When using quotient.mk, you're supposed to talk about x ≈ y not setoid.r x y

[Eric Wieser]

When using quotient.mk', setoid.r is the preferred spelling (see docs#quotient.eq')

[ZHAO Jinxiang]

I can't find the definition of quot.mk in std lib. Is this function built into the language?

[Markus Himmel]

Yes, see core.lean