chore(*): suggestions from the generalisation linter (#13092)

Prompted by zulip discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/An.20example.20of.20why.20formalization.20is.20useful

These are the "reasonable" suggestions from @alexjbest's generalisation linter up to `algebra.group.basic`.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/group/basic.lean

@@ -206,6 +206,10 @@ lemma mul_div_assoc' (a b c : G) : a * (b / c) = (a * b) / c :=
 @[simp, to_additive] lemma one_div (a : G) : 1 / a = a⁻¹ :=
 (inv_eq_one_div a).symm
 
+@[to_additive]
+lemma mul_div (a b c : G) : a * (b / c) = a * b / c :=
+by simp only [mul_assoc, div_eq_mul_inv]
+
 end div_inv_monoid
 
 section group
@@ -220,7 +224,7 @@ lemma one_inv : 1⁻¹ = (1 : G) :=
 inv_eq_of_mul_eq_one (one_mul 1)
 
 @[to_additive]
-theorem left_inverse_inv (G) [group G] :
+theorem left_inverse_inv (G) [has_involutive_inv G] :
   function.left_inverse (λ a : G, a⁻¹) (λ a, a⁻¹) :=
 inv_inv
 
@@ -366,12 +370,6 @@ mt eq_of_div_eq_one' h
 lemma div_inv_eq_mul (a b : G) : a / (b⁻¹) = a * b :=
 by rw [div_eq_mul_inv, inv_inv]
 
-local attribute [simp] mul_assoc
-
-@[to_additive]
-lemma mul_div (a b c : G) : a * (b / c) = a * b / c :=
-by simp only [mul_assoc, div_eq_mul_inv]
-
 @[to_additive]
 lemma div_mul_eq_div_div_swap (a b c : G) : a / (b * c) = a / c / b :=
 by simp only [mul_assoc, mul_inv_rev , div_eq_mul_inv]

src/order/basic.lean

@@ -96,9 +96,9 @@ protected lemma ge [preorder α] {x y : α} (h : x = y) : y ≤ x := h.symm.le
 
 lemma trans_le [preorder α] {x y z : α} (h1 : x = y) (h2 : y ≤ z) : x ≤ z := h1.le.trans h2
 
-lemma not_lt [partial_order α] {x y : α} (h : x = y) : ¬(x < y) := λ h', h'.ne h
+lemma not_lt [preorder α] {x y : α} (h : x = y) : ¬(x < y) := λ h', h'.ne h
 
-lemma not_gt [partial_order α] {x y : α} (h : x = y) : ¬(y < x) := h.symm.not_lt
+lemma not_gt [preorder α] {x y : α} (h : x = y) : ¬(y < x) := h.symm.not_lt
 
 end eq
 
@@ -205,7 +205,7 @@ lemma ne.le_iff_lt [partial_order α] {a b : α} (h : a ≠ b) : a ≤ b ↔ a <
 ⟨λ h', lt_of_le_of_ne h' h, λ h, h.le⟩
 
 -- See Note [decidable namespace]
-protected lemma decidable.ne_iff_lt_iff_le [partial_order α] [@decidable_rel α (≤)]
+protected lemma decidable.ne_iff_lt_iff_le [partial_order α] [decidable_eq α]
   {a b : α} : (a ≠ b ↔ a < b) ↔ a ≤ b :=
 ⟨λ h, decidable.by_cases le_of_eq (le_of_lt ∘ h.mp), λ h, ⟨lt_of_le_of_ne h, ne_of_lt⟩⟩