porting algebra.order.ring_lemmas

Stream: mathlib4

[Yakov Pechersky]

mathlib4#482, notes I made through the process:

local notation doesn't work, had to make just notation and turn off quotPrecheck
Subtype.prop was mathported to x.Prop instead of x.prop
eq.Ne should be eq.ne
mathlib3's lt_of_not_le is now lt_of_not_ge
there is no convert tactic
rw doesn't leave side goals anymore, can't rw [mul_lt_mul_left]
LE.le.eq_or_lt used instead of has_le.le.eq_or_gt
used simp [...] at h instead of simpa [...] using h
needed to specify congr_arg (· * b) to make sure correct HMul was found,
instead of ideally congr_arg _
implicit arg handling caused different term proofs instead of using monotone
ported over CancelMonoidWithZero
simp! does not do anything to abbrevs, neither does dsimp
simp (only) doesn't terminate on syntactically matched LHS and RHS, rfl is needed

Should I mark the file on the yaml?

[Jakob von Raumer]

What didn't work with local notations?

[Yuyang Zhao]

Not related to the porting itself, but #16523 and #16525 haven't been merged, what should I do with them?

[Yuyang Zhao]

(algebra/order/monoid_lemmas_zero_lt in titles is its old name when these PRs are created)

[Yakov Pechersky]

@Jakob von Raumer making them local hits the various errors MWE'd here:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/local.20notation.20for.20subtypes