CategoryTheory.Quotient (!4#2339)

Stream: mathlib4

[Matej Penciak]

I'm running into some hairy issues in this file... In particular for the Category instance of Quotient r (here) the three properties id_comp, comp_id, and assoc were dispatched by tidy in Lean 3 but aren't solved by aesop_cat in Lean 4.

I did a little bit of sleuthing in Lean 3, and tidy? suggests that id_comp can be solved by the following:intros X Y f, induction f, work_on_goal 1 { dsimp at *, simp at * }, refl.

In Lean 4 I immediately run into an error with induction freturning major premise type is not an inductive type.

This is true, as f has type Quot (CompClosure r), so it is not actually an inductive type. But Lean 3 is happy to see through the Quot and induction works on the wrapped inductive type CompClosure r.

Any suggestions would be helpful!

[Matthew Ballard]

In a similar situation where induction could not see through a quotient, I had to fall back on Quot.ind and its variants.

[Matej Penciak]

Matthew Ballard said:

In a similar situation where induction could not see through a quotient, I had to fall back on Quot.ind and its variants.

I'll give it a try!

[Kevin Buzzard]

So is this a regression in the induction tactic? Can you minimise?

[Reid Barton]

Is it about "seeing through" the quotient or doing induction on the quotient?

[Reid Barton]

Was induction working on quotients added in community lean?

[Matthew Ballard]

My language was off but it worked before and didn’t after. I was surprised and I asked at the porting meeting it was specially baked into induction before. As far people know it wasn’t

[Rémi Bottinelli]

Hey, I took the liberty of commiting fixes to the errors (iirc semorisson encouraged people pitching in on other's PRs somewhere; hope that's OK).

[Rémi Bottinelli]

@Matej Penciak are alignment and other things already taken care of? Should I drop the WIP label and request a review?

[Rémi Bottinelli]

In the mathlib3 source, they call functor the functor from the category to its quotient, but this is a bit of a confusing name imo. Wouldn't mk or as make more sense? If so, I guess it's not necessarily a good idea to proceed with such a change during porting?

[Matej Penciak]

Rémi Bottinelli said:

Matej Penciak are alignment and other things already taken care of? Should I drop the WIP label and request a review?

I haven't had a chance to look at the PR in a while because I've gotten very busy at work recently. I don't recall doing any checks on the names in comments/alignments, so it's probably a good idea to do that. I'm not sure I'll be able to get back to the file until sometime next week, so anyone should feel free to fix it up (thanks for your help btw!)

[Rémi Bottinelli]

OK, I'd like to do path_category next so I'll try and take care of it then

[Rémi Bottinelli]

OK, I checked the names and things look to be in order.