mathlib

e8add823 - chore(algebra/{ordered_monoid,linear_ordered_comm_group_with_zero}): remove some uses of @ (#7884)

chore(algebra/{ordered_monoid,linear_ordered_comm_group_with_zero}): remove some uses of @ (#7884) This PR replaces a couple of uses of `@` with slightly more verbose proofs that only use the given explicit arguments. The `by apply mul_lt_mul''' hab0 hcd0` line also works with `mul_lt_mul''' hab0 hcd0` alone (at least on my machine). The reason for the slightly more elaborate proof is that once the typeclass assumptions will change, the direct term-mode proof will break, while the `by apply` version is more stable. Besides its aesthetic value, this is useful in PR #7645, as the typeclass arguments of the involved lemmas will change and this will keep the diff (slightly) shorter.