chore(GroupTheory): golf entire base_smul_def and summand_smul_def using rfl (leanprover-community#28563)

Co-authored-by: euprunin <euprunin@users.noreply.github.com>

Author: euprunin

Mathlib/GroupTheory/PushoutI.lean

@@ -466,18 +466,12 @@ noncomputable instance mulAction : MulAction (PushoutI φ) (NormalWord d) :=
       smul_inv_smul, base_smul_def', MonoidHom.apply_ofInjective_symm]
 
 theorem base_smul_def (h : H) (w : NormalWord d) :
-    base φ h • w = { w with head := h * w.head } := by
-  dsimp [NormalWord.mulAction, instHSMul, SMul.smul]
-  rw [lift_base]
-  rfl
+    base φ h • w = { w with head := h * w.head } := rfl
 
 theorem summand_smul_def {i : ι} (g : G i) (w : NormalWord d) :
     of (φ := φ) i g • w = (equivPair i).symm
       { equivPair i w with
-        head := g * (equivPair i w).head } := by
-  dsimp [NormalWord.mulAction, instHSMul, SMul.smul]
-  rw [lift_of]
-  rfl
+        head := g * (equivPair i w).head } := rfl
 
 theorem of_smul_eq_smul {i : ι} (g : G i) (w : NormalWord d) :
     of (φ := φ) i g • w = g • w := by