mathlib

a79df550 - chore(algebra/ordered_group): remove linear_ordered_comm_group.to_comm_group (#7861)

chore(algebra/ordered_group): remove linear_ordered_comm_group.to_comm_group (#7861) This instance shortcut bypassed `ordered_comm_group`, and could easily result in computability problems since many `linear_order` instances are noncomputable due to their embedded decidable instances. This would happen when: * Lean needs an `add_comm_group A` * We have: * `noncomputable instance : linear_ordered_comm_group A` * `instance : ordered_comm_group A` * Lean tries `linear_ordered_comm_group.to_comm_group` before `ordered_comm_group.to_comm_group`, and hands us back a noncomputable one, even though there is a computable one available. There're no comments explaining why things were done this way, suggesting it was accidental, or perhaps that `ordered_comm_group` came later. This broke one proof which somehow `simponly`ed associativity the wrong way, so I just golfed that proof and the one next to it for good measure.