quot.exact given equivalence

Stream: Is there code for X?

[Kyle Miller]

One part of the quot API is docs#quot.exact, which is less-than-convenient when you know the relation is an equivalence relation already. While docs#quotient.exact exists, it's in terms of setoids, and it doesn't put the relation syntactically into the correct form.

Is there something like this?

lemma eqv_gen.of_eqv {α : Type*} {r : α → α → Prop} (h : equivalence r)
  {x y : α} (H : eqv_gen r x y) : r x y :=
begin
 induction H,
 { assumption },
 { exact h.left _ },
 { exact h.right.left ‹_› },
 { exact h.right.right ‹_› ‹_› }
end

That lets you write something like (quot.exact r h).of_eqv proof_of_equivalence for h : quot.mk r x = quot.mk r y to get r x y.

(This seems more general than having parallel quot lemmas that take an additional equivalence r argument.)

(cc @Yakov Pechersky)

[Eric Wieser]

Pretty sure we have that

[Eric Wieser]

Probably in file#data/setoid/basic

[Eric Wieser]

docs#eqv_gen_eq_of_equivalence

[Kyle Miller]

Thanks (docs#relation.eqv_gen_iff_of_equivalence is a bit closer). It still seems like it would be nice for the quot API to have it be more amenable to dot notation.

lemma eqv_gen.of_eqv {α : Type*} {r : α → α → Prop} (h : equivalence r)
  {x y : α} (H : eqv_gen r x y) : r x y := (relation.eqv_gen_iff_of_equivalence h).mp H

[Eric Wieser]

I'd probably put it in the equivalence namespace instead

[Eric Wieser]

#10105