chore: golf using simp, and don't squeeze terminal simp calls (#35148)

Author: euprunin

Mathlib/Algebra/Group/Basic.lean

@@ -899,8 +899,7 @@ theorem div_eq_of_eq_mul' {a b c : G} (h : a = b * c) : a / b = c := by
 
 @[to_additive (attr := simp)]
 theorem mul_div_mul_left_eq_div (a b c : G) : c * a / (c * b) = a / b := by
-  rw [div_eq_mul_inv, mul_inv_rev, mul_comm b⁻¹ c⁻¹, mul_comm c a, mul_assoc, ← mul_assoc c,
-    mul_inv_cancel, one_mul, div_eq_mul_inv]
+  simp
 
 @[to_additive eq_sub_of_add_eq']
 theorem eq_div_of_mul_eq'' (h : c * a = b) : a = b / c := by simp [h.symm]

Mathlib/Algebra/Group/Hom/Basic.lean

@@ -164,7 +164,7 @@ theorem mul_comp [Mul M] [Mul N] [CommSemigroup P] (g₁ g₂ : N →ₙ* P) (f
 theorem comp_mul [Mul M] [CommSemigroup N] [CommSemigroup P] (g : N →ₙ* P) (f₁ f₂ : M →ₙ* N) :
     g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ := by
   ext
-  simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]
+  simp
 
 end MulHom
 
@@ -256,7 +256,8 @@ lemma mul_comp [MulOneClass P] (g₁ g₂ : M →* N) (f : P →* M) :
 @[to_additive]
 lemma comp_mul [CommMonoid P] (g : N →* P) (f₁ f₂ : M →* N) :
     g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂ := by
-  ext; simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]
+  ext
+  simp
 
 end Mul
 
@@ -278,7 +279,7 @@ theorem inv_comp (φ : N →* G) (ψ : M →* N) : φ⁻¹.comp ψ = (φ.comp ψ
 @[to_additive (attr := simp)]
 theorem comp_inv (φ : G →* H) (ψ : M →* G) : φ.comp ψ⁻¹ = (φ.comp ψ)⁻¹ := by
   ext
-  simp only [Function.comp_apply, inv_apply, map_inv, coe_comp]
+  simp
 
 /-- If `f` and `g` are monoid homomorphisms to a commutative group, then `f / g` is the homomorphism
 sending `x` to `(f x) / (g x)`. -/
@@ -295,7 +296,8 @@ lemma div_comp (f g : N →* G) (h : M →* N) : (f / g).comp h = f.comp h / g.c
 
 @[to_additive (attr := simp)]
 lemma comp_div (f : G →* H) (g h : M →* G) : f.comp (g / h) = f.comp g / f.comp h := by
-  ext; simp only [Function.comp_apply, div_apply, map_div, coe_comp]
+  ext
+  simp
 
 end InvDiv
 

Mathlib/Algebra/Group/Prod.lean

@@ -409,7 +409,7 @@ theorem snd_comp_prod (f : M →* N) (g : M →* P) : (snd N P).comp (f.prod g)
 
 @[to_additive (attr := simp) prod_unique]
 theorem prod_unique (f : M →* N × P) : ((fst N P).comp f).prod ((snd N P).comp f) = f :=
-  ext fun x => by simp only [prod_apply, coe_fst, coe_snd, comp_apply]
+  ext fun _ => by simp
 
 end Prod