quot.mk vs quotient.mk

Stream: general

[Patrick Massot]

Do we already have lemma quot_mk_quotient_mk {α :Type*} [setoid α] (a : α) : quot.mk setoid.r a = ⟦a⟧ := rfl? I need this because rintro typically produces the left-hand side.