cancel isos

Stream: general

[Reid Barton]

@Scott Morrison Somehow, cancel_epi with f = ↑i (i : x ≅ y) doesn't work any more.
I managed to track this down far enough to find that adding the line (which used to be in tidy.tidy)

attribute [reducible] lift_t coe_t coe_b

makes it work again. But I don't really understand what is going on.

[Scott Morrison]

@Reid Barton, thanks for all these requests. I am giving a demo in a few hours of parts of obviously and my category theory library, and right after that I will address these three issues!

[Scott Morrison]

The last one is a bit interesting: I'm now very careful to have my automation _not_ unfold too much, and cancel_epi is having trouble seeing through a coercion that formerly someone else was unfolding. I'll have to find another solution. If you have a MWE showing the cancel_epi issue that would be great.

[Reid Barton]

Yes, I think the situation with cancel_epi makes sense to me now. Probably the right thing to do is just to add a second instance which matches ↑i (in addition to the existing instance which matches i.hom).

[Scott Morrison]

Okay, this issue should be fixed in https://github.com/leanprover/mathlib/pull/278/commits/ccb1adf8a0fba114c5cbcad0169212d4775517d7, which is part of https://github.com/leanprover/mathlib/pull/278.

[Patrick Massot]

I'm happy to see you are enjoying your Paris sightseeing

[Scott Morrison]

:-)

[Scott Morrison]

I went out and ate lots of pastries and cheese this morning. :-)

[Scott Morrison]

Also I can see the Notre Dame from where I'm sitting.

[Patrick Massot]

Cheese, Notre-Dame and Lean seems to be a good combination