mathlib4#659 Algebra.Hom.Group

Stream: mathlib4

[Scott Morrison]

mathlib4#659, porting Algebra.Hom.Group, has been sitting a few days waiting for the merge of #17733, reverting #17048. That's all now landed on the mathlib3 side, and I think this PR is probably on the critical path at the moment.

[Scott Morrison]

If someone is looking for something to do, opening up that PR and working out how to bring it in sync with mathlib3 master would be great.

[Scott Morrison]

Hopefully this just involves deleting unported stuff! If so it will be very satisfying. :-)

[Scott Morrison]

Okay, this is now back in sync with mathlib3, but there are a lot of porting notes that need more work before we can merge.

[Scott Morrison]

@Floris van Doorn, would you have a chance to diagnose the @[to_additive] issues that arise there?

[Scott Morrison]

There is an unfortunate issue with outParam. After the resolution of https://github.com/leanprover/lean4/issues/1852 we were hoping to be able to remove outParam from the typeclass arguments. Now at least the declarations are accepted, but there are simp failures afterwards. This is not critical for this PR, but it is probably something that needs fixing in Lean 4, but to do that we'll need to reduce it to a non-mathlib #mwe.

[Winston Yin]

Would you like the porting of #17733 to be in the same PR as #659? I can comb through it and make all the equivalent changes during the (US west coast) day

[Winston Yin]

Breadcrumb to other Zulip topics about these porting notes:

Instance loop: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/instance.20loop.3F/near/311533638
↑1 = 1: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.86.911.20.3D.201.3F/near/311798847
simp not using lemma: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20not.20using.20a.20simp.20lemma/near/311227341

[Floris van Doorn]

Scott Morrison said:

Floris van Doorn, would you have a chance to diagnose the @[to_additive] issues that arise there?

mathlib4#779

[Scott Morrison]

Winston Yin said:

Would you like the porting of #17733 to be in the same PR as #659? I can comb through it and make all the equivalent changes during the (US west coast) day

Sorry, Winston, I don't understand this message. mathlib4#659 should be a faithful port of algebra.hom.group as it currently exists in mathlib master (i.e. now that #17733 has merged).

[Winston Yin]

I see 85 changed files in #17733. Changes in Algebra.Hom.Group have been ported over but I’ll look through the other changed files too

[Jireh Loreaux]

Don't worry about the other changed files, they should all be further along the import hierarchy, which means we won't have encountered them during porting yet.