chore(algebra/ordered_group): remove linear_ordered_comm_group.to_com…

…m_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.

src/algebra/ordered_group.lean

@@ -575,9 +575,8 @@ end ordered_add_comm_group
 /-- A linearly ordered additive commutative group is an
 additive commutative group with a linear order in which
 addition is monotone. -/
-@[protect_proj, ancestor add_comm_group linear_order]
-class linear_ordered_add_comm_group (α : Type u) extends add_comm_group α, linear_order α :=
-(add_le_add_left : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
+@[protect_proj, ancestor ordered_add_comm_group linear_order]
+class linear_ordered_add_comm_group (α : Type u) extends ordered_add_comm_group α, linear_order α
 
 /-- A linearly ordered commutative monoid with an additively absorbing `⊤` element.
   Instances should include number systems with an infinite element adjoined.` -/
@@ -590,17 +589,12 @@ class linear_ordered_add_comm_group_with_top (α : Type*)
 /-- A linearly ordered commutative group is a
 commutative group with a linear order in which
 multiplication is monotone. -/
-@[protect_proj, ancestor comm_group linear_order, to_additive]
-class linear_ordered_comm_group (α : Type u) extends comm_group α, linear_order α :=
-(mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b)
+@[protect_proj, ancestor ordered_comm_group linear_order, to_additive]
+class linear_ordered_comm_group (α : Type u) extends ordered_comm_group α, linear_order α
 
 section linear_ordered_comm_group
 variables [linear_ordered_comm_group α] {a b c : α}
 
-@[priority 100, to_additive] -- see Note [lower instance priority]
-instance linear_ordered_comm_group.to_ordered_comm_group : ordered_comm_group α :=
-{ ..‹linear_ordered_comm_group α› }
-
 @[priority 100, to_additive] -- see Note [lower instance priority]
 instance linear_ordered_comm_group.to_linear_ordered_cancel_comm_monoid :
   linear_ordered_cancel_comm_monoid α :=

src/data/nat/modeq.lean

@@ -86,16 +86,16 @@ end
 
 theorem modeq_add (h₁ : a ≡ b [MOD n]) (h₂ : c ≡ d [MOD n]) : a + c ≡ b + d [MOD n] :=
 modeq_of_dvd begin
-  convert dvd_add (dvd_of_modeq h₁) (dvd_of_modeq h₂) using 1,
-  simp [sub_eq_add_neg, add_left_comm, add_comm],
+  rw [int.coe_nat_add, int.coe_nat_add, add_sub_comm],
+  exact dvd_add (dvd_of_modeq h₁) (dvd_of_modeq h₂),
 end
 
 theorem modeq_add_cancel_left (h₁ : a ≡ b [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) : c ≡ d [MOD n] :=
 begin
-  simp only [modeq_iff_dvd] at *,
+  simp only [modeq_iff_dvd, int.coe_nat_add] at *,
+  rw add_sub_comm at h₂,
   convert _root_.dvd_sub h₂ h₁ using 1,
-  simp [sub_eq_add_neg],
-  abel
+  rw add_sub_cancel',
 end
 
 theorem modeq_add_cancel_right (h₁ : c ≡ d [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) : a ≡ b [MOD n] :=