Commit 2022-12-09 00:56 f4eb9061

feat: port Algebra.Group.WithOne.Basic (#922) mathlib3 SHA: 4dc134b97a3de65ef2ed881f3513d56260971562 porting notes:

1. In WithOne.lift mathport's output was broken, but I think the only reason was that it was parenthesized wrong (or maybe it was a whitespace / formatting issue?)
2. In MulEquiv.withOneCongr, there were some simp calls that broke. I think this is a result of the way coercions are handled now. I think the net result is that simp doesn't get it into a form where it can apply Equiv.symm_apply_apply.
3. I added the to_additive attribute to MulEquiv.withOneCongr_{refl, symm, trans} because it just seemed to be missing from mathlib3.
4. WithOne already has semireducible transparency in mathlib4, so we are just ignoring the changing of transparency settings (this isn't even possible in Lean 4); see Zulip