mathlib3

db07e6fe - chore(algebra/order/lattice_group): remove redundant instance (#18951)

chore(algebra/order/lattice_group): remove redundant instance (#18951) This instance was redundant. It can be synthesised at the declaration site via: ``` example (α : Type u) [linear_ordered_comm_group α] : covariant_class α α (*) (≤) := by show_term {apply_instance} -- ordered_comm_group.to_covariant_class_left_le α ``` Moreover, it is implicated in a timeout in the reenableeta branches, so I want it gone! This PR is just a verification that mathlib still compiles. I don't care if it is merged. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>