feat: port Algebra.Order.Monoid.WithTop (#902)

mathlib3: 655994e298904d7e5bbd1e18c95defd7b543eb94

- [x] depends on #910

Not too bad. Mostly renaming instances and a few broken proofs.

Things to double-check (all marked with `Porting note`):
- `lift` is not implemented yet, I replaced it with `induction`.
- In `addSemigroup` I didn't get `repeat` or `repeat'` to work. That could be golfed.
- In `WithTop.addHom` the anonymous constructor didn't work, but writing it out, it did. Is that expected?
- I'm a bit unsure about coersions. I left in most things and removed (commented out) the lemma `coe_coe_add_hom`. Could be worth gleaming over anything that has `coe` in it's name.


Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Co-authored-by: Jon Eugster <Jon.Eugster@hhu.de>

Author: joneugster

Mathlib.lean

@@ -60,6 +60,7 @@ import Mathlib.Algebra.Order.Monoid.NatCast
 import Mathlib.Algebra.Order.Monoid.OrderDual
 import Mathlib.Algebra.Order.Monoid.TypeTags
 import Mathlib.Algebra.Order.Monoid.Units
+import Mathlib.Algebra.Order.Monoid.WithTop
 import Mathlib.Algebra.Order.Monoid.WithZero.Basic
 import Mathlib.Algebra.Order.Monoid.WithZero.Defs
 import Mathlib.Algebra.Order.Positive.Ring