Prove Quotient is initial

Stream: maths

[Erika Su]

In Theorem Proving in Lean

Of course, the quotient construction is most commonly used in situations when r is an equivalence relation. Given r as above, if we define r' according to the rule r' a b iff Quot.mk r a = Quot.mk r b, then it's clear that r' is an equivalence relation. Indeed, r' is the kernel of the function a ↦ quot.mk r a. The axiom Quot.sound says that r a b implies r' a b. Using Quot.lift and Quot.ind, we can show that r' is the smallest equivalence relation containing r, in the sense that if r'' is any equivalence relation containing r, then r' a b implies r'' a b. In particular, if r was an equivalence relation to start with, then for all a and b we have r a b iff r' a b.

So naturally i want to prove:

variable (α β : Prop) (s1 s2 s3: Setoid α)
variable (x y z : α)

theorem quod_init_algebra :
      ({ x y : α } -> s1.r x y -> s3.r x y) ->
      { x y : α } -> Quotient.mk s1 x = Quotient.mk s1 y -> s3.r x y :=
      λ infer =>
      λ {x y : α } q_eq => sorry

But i am stuck here......

[Alex J. Best]

reading through init/core.lean the theorem docs4#Quotient.exact is basically what you need:

variable (α β : Prop) (s1 s2 s3: Setoid α)


theorem quod_init_algebra :
      ({ x y : α } -> s1.r x y -> s3.r x y) ->
      { x y : α } -> Quotient.mk s1 x = Quotient.mk s1 y -> s3.r x y :=
      λ infer =>
      λ {x y : α } q_eq => infer (Quotient.exact q_eq)