Inverse of Quot.sound

Stream: new members

[Matei Adriel]

Is there any way to go from Quot.mk r a = Quot.mk r b to r a b?

[Chris B]

Looks like docs#quotient.eq

[Chris B]

Actually docs#quotient.exact is just the direction you want. eq is iff.

[Kevin Buzzard]

[note that this is Lean 3]

[Chris B]

Oh right, capital letters. https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Quotient.exact

[Henrik Böving]

We've mapped the mathlib4_docs links to docs4# btw.

[Kevin Buzzard]

docs4#Quot.exact docs4#Quotient.exact

[Kevin Buzzard]

If Quot is "quotient by the equivalence relation generated by r" then it's not possible to go from Quot.mk r a = Quot.mk r b to r a b (because maybe r a c and r c b are true instead) but I'm not entirely sure what Quot is.

[Chris B]

Ah, good eye, I glossed over Quot as Quotient.

[Mauricio Collares]

Quot is defined in Lean core, and is explained in https://leanprover.github.io/theorem_proving_in_lean4/axioms_and_computation.html. But Kevin's point stands: If r is not already an equivalence relation, the converse might not be true. If r is an equivalence relation, you should use Quotient instead of Quot, which is also defined in core.

[Mauricio Collares]

@Matei Adriel There's some useful discussion in the above link if you Ctrl-F for "Given r as above".

[Matei Adriel]

Yep, I was using Quotient, but used simp to try and remove as many layers of function calls as possible. Quotient.exact looks exactly like what I need

[Mario Carneiro]

Matei Adriel said:

Yep, I was using Quotient, but used simp to try and remove as many layers of function calls as possible.

Don't do this, this is a common newbie mistake. Only unfold definitional layers if you have no other choice; if you unfold more than one layer of definitions then that means you are either missing an API lemma or are ignoring the one that exists