feat(algebra/*): some simp lemmas, and changing binders (#4681)

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

src/algebra/algebra/basic.lean

@@ -162,7 +162,7 @@ by rw [smul_def, smul_def, left_comm]
 by rw [smul_def, smul_def, mul_assoc]
 
 section
-variables (r : R) (a : A)
+variables {r : R} {a : A}
 
 @[simp] lemma bit0_smul_one : bit0 r • (1 : A) = r • 2 :=
 by simp [bit0, add_smul, smul_add]

src/algebra/invertible.lean

@@ -62,6 +62,14 @@ invertible.inv_of_mul_self
 lemma mul_inv_of_self [has_mul α] [has_one α] (a : α) [invertible a] : a * ⅟a = 1 :=
 invertible.mul_inv_of_self
 
+@[simp]
+lemma inv_of_mul_self_assoc [monoid α] (a b : α) [invertible a] : ⅟a * (a * b) = b :=
+by rw [←mul_assoc, inv_of_mul_self, one_mul]
+
+@[simp]
+lemma mul_inv_of_self_assoc [monoid α] (a b : α) [invertible a] : a * (⅟a * b) = b :=
+by rw [←mul_assoc, mul_inv_of_self, one_mul]
+
 @[simp]
 lemma mul_inv_of_mul_self_cancel [monoid α] (a b : α) [invertible b] : a * ⅟b * b = a :=
 by simp [mul_assoc]

src/group_theory/group_action.lean

@@ -64,9 +64,11 @@ section gwz
 
 variables {G : Type*} [group_with_zero G] [mul_action G β]
 
+@[simp]
 lemma inv_smul_smul' {c : G} (hc : c ≠ 0) (x : β) : c⁻¹ • c • x = x :=
 (units.mk0 c hc).inv_smul_smul x
 
+@[simp]
 lemma smul_inv_smul' {c : G} (hc : c ≠ 0) (x : β) : c • c⁻¹ • x = x :=
 (units.mk0 c hc).smul_inv_smul x