mathlib3

74746bde - chore(counterexamples/canonically_ordered_comm_semiring_two_mul): golf (#12504)