Quotient.finLiftOn₂

Stream: Is there code for X?

[Tristan Figueroa-Reid]

Some analog of Quotient.liftOn₂ for Quotient.finLiftOn? Working on defining it right now, but this seems like something mathlib would have already had - I can't seem to find it, though.

[Aaron Liu]

I have never used docs#Quotient.finLiftOn before so I'm not too surprised that the double version isn't in mathlib

[Tristan Figueroa-Reid]

(Got distracted, but just opened #27302.)

[Kenny Lau]

@Tristan Figueroa-Reid i've golfed your code (and changed abbrev to def)

[Kenny Lau]

is the reason of making it abbrev so that simp would apply? in that case I would suggest stating a separate simp lemma instead

[Tristan Figueroa-Reid]

Kenny Lau said:

is the reason of making it abbrev so that simp would apply? in that case I would suggest stating a separate simp lemma instead

It should have been def. Thanks :+1: [I was reusing the original definition of liftOn₂, which was abbrev since it was defined directly with lift₂]

[Tristan Figueroa-Reid]

Thanks a lot for the help @Kenny Lau!