Lift composition with quot.mk

Stream: Is there code for X?

[Yaël Dillies]

Do we have this anywhere? Is it true?

import data.quot

example {α β : Type*} {s : setoid α} (f : quotient s → β)
  (h : ∀ a b, @setoid.r _ s a b → f (quotient.mk' a) = f (quotient.mk' b)) (x : quotient s) :
  quotient.lift_on' x (f ∘ quotient.mk') h = f x :=
sorry

[Yaël Dillies]

It's roughly docs#quotient.lift_on'_mk', but the other way around, somehow.

[Yury G. Kudryashov]

Can't find it

[Yaël Dillies]

Got it

[Yaël Dillies]

example {α β : Type*} {s : setoid α} (f : quotient s → β)
  (h : ∀ a b, @setoid.r _ s a b → f (quotient.mk' a) = f (quotient.mk' b)) (a : quotient s) :
  quotient.lift_on' a (f ∘ quotient.mk') h = f a :=
quotient.induction_on' a $ λ a, rfl

[Yaël Dillies]

Is it worth having or does it belong to the too-trivial-to-be-stated realm?

[Yury G. Kudryashov]

It isn't more trivial than docs#quotient.lift_on_mk

[Yaël Dillies]

Okay, great :smiling_face:

[Eric Wieser]

Should lift_on just be marked simp so that it unfolds to lift (same for the primed versions)?