quotient mk vs mk' lemmas

Stream: new members

[Yakov Pechersky]

Is there a reason we don't have these?

import data.quot

variables {α β : Sort*} [setoid α]

lemma quotient.mk_eq_mk' (x : α) : ⟦x⟧ = quotient.mk' x := rfl

@[simp] lemma quotient.lift_on_mk' (x : α) (f : α → β) (h) : ⟦x⟧.lift_on' f h = f x := rfl

[Yakov Pechersky]

I have a case where I use \[[]] mk notation in a local instance section, and build API around equality of mk, to make the relation more explicit. But that means elsewhere, outside of the section, I have to use mk' to construct terms in the quotient. Which doesn't use the API I've built. Should I just make a simp tagged API lemma simplifying goals about setoid.r? I've been trying to convert all of my quotient.mk' to \[[]] so that my API simp lemmas can fire.

[Johan Commelin]

I don't think there's any reason we don't have these.

[Yakov Pechersky]

#12204

[Eric Wieser]

Is the first one an equation lemma for docs#quotient.mk'?

[Eric Wieser]

Ah no, it unfolds to quot.mk