chore(*): use *_*_*_comm where possible (#12372)

These lemmas are quite helpful when proving `map_add` type statements; hopefully people will remember them more if they see them used in a few more places.

src/data/num/lemmas.lean

@@ -51,8 +51,7 @@ theorem add_one (n : pos_num) : n + 1 = succ n := by cases n; refl
 theorem add_to_nat : ∀ m n, ((m + n : pos_num) : ℕ) = m + n
 | 1        b        := by rw [one_add b, succ_to_nat, add_comm]; refl
 | a        1        := by rw [add_one a, succ_to_nat]; refl
-| (bit0 a) (bit0 b) := (congr_arg _root_.bit0 (add_to_nat a b)).trans $
-  show ((a + b) + (a + b) : ℕ) = (a + a) + (b + b), by simp [add_left_comm]
+| (bit0 a) (bit0 b) := (congr_arg _root_.bit0 (add_to_nat a b)).trans $ add_add_add_comm _ _ _ _
 | (bit0 a) (bit1 b) := (congr_arg _root_.bit1 (add_to_nat a b)).trans $
   show ((a + b) + (a + b) + 1 : ℕ) = (a + a) + (b + b + 1), by simp [add_left_comm]
 | (bit1 a) (bit0 b) := (congr_arg _root_.bit1 (add_to_nat a b)).trans $

src/group_theory/free_abelian_group.lean

@@ -167,8 +167,7 @@ begin
   { assume x h,
     simp only [(lift _).map_neg, lift.of, pi.add_apply, neg_add] },
   { assume x y hx hy,
-    simp only [(lift _).map_add, hx, hy],
-    ac_refl }
+    simp only [(lift _).map_add, hx, hy, add_add_add_comm] }
 end
 
 /-- If `g : free_abelian_group X` and `A` is an abelian group then `lift_add_group_hom g`

src/linear_algebra/bilinear_form.lean

@@ -128,10 +128,10 @@ lemma ext_iff : B = D ↔ (∀ x y, B x y = D x y) := ⟨congr_fun, ext⟩
 
 instance : add_comm_monoid (bilin_form R M) :=
 { add := λ B D, { bilin := λ x y, B x y + D x y,
-                  bilin_add_left := λ x y z, by { rw add_left, rw add_left, ac_refl },
-                  bilin_smul_left := λ a x y, by { rw [smul_left, smul_left, mul_add] },
-                  bilin_add_right := λ x y z, by { rw add_right, rw add_right, ac_refl },
-                  bilin_smul_right := λ a x y, by { rw [smul_right, smul_right, mul_add] } },
+                  bilin_add_left := λ x y z, by rw [add_left, add_left, add_add_add_comm],
+                  bilin_smul_left := λ a x y, by rw [smul_left, smul_left, mul_add],
+                  bilin_add_right := λ x y z, by rw [add_right, add_right, add_add_add_comm],
+                  bilin_smul_right := λ a x y, by rw [smul_right, smul_right, mul_add] },
   add_assoc := by { intros, ext, unfold bilin coe_fn has_coe_to_fun.coe bilin, rw add_assoc },
   zero := { bilin := λ x y, 0,
             bilin_add_left := λ x y z, (add_zero 0).symm,

src/linear_algebra/matrix/determinant.lean

@@ -582,8 +582,7 @@ begin
     rw fintype.prod_sum_type,
     simp_rw [equiv.sum_congr_apply, sum.map_inr, sum.map_inl, from_blocks_apply₁₁,
       from_blocks_apply₂₂],
-    have hr : ∀ (a b c d : R), (a * b) * (c * d) = a * c * (b * d), { intros, ac_refl },
-    rw hr,
+    rw mul_mul_mul_comm,
     congr,
     rw [sign_sum_congr, units.coe_mul, int.cast_mul] },
   { intros σ₁ σ₂ h₁ h₂,

src/linear_algebra/prod.lean

@@ -195,7 +195,7 @@ See note [bundled maps over different rings] for why separate `R` and `S` semiri
   left_inv := λ f, by simp only [prod.mk.eta, coprod_inl, coprod_inr],
   right_inv := λ f, by simp only [←comp_coprod, comp_id, coprod_inl_inr],
   map_add' := λ a b,
-    by { ext, simp only [prod.snd_add, add_apply, coprod_apply, prod.fst_add], ac_refl },
+    by { ext, simp only [prod.snd_add, add_apply, coprod_apply, prod.fst_add, add_add_add_comm] },
   map_smul' := λ r a,
     by { dsimp, ext, simp only [smul_add, smul_apply, prod.smul_snd, prod.smul_fst,
                                 coprod_apply] } }

src/tactic/omega/eq_elim.lean

@@ -205,9 +205,7 @@ begin
           apply fun_mono_2 rfl,
           simp only [coeffs.val_except, mul_add],
           repeat {rw ← coeffs.val_between_map_mul},
-          have h4 : ∀ {a b c d : int},
-            a + b + (c + d) = (a + c) + (b + d),
-          { intros, ring }, rw h4,
+          rw add_add_add_comm,
           have h5 : add as (list.map (has_mul.mul a_n)
             (list.map (λ (x : ℤ), symmod x (get n as + 1)) as)) =
             list.map (λ (a_i : ℤ), a_i + a_n * symmod a_i m) as,