-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst : Monoid K
inst_1 : (i : ι) → Group (G i)
inst_2 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
d : Transversal (G := G) φ
inst_3 : DecidableEq ι
inst_4 : (i : ι) → DecidableEq (G i)
i : ι
x x_1 : G i
x_2 : NormalWord (G := G) d
⊢ Eq (α := NormalWord (G := G) d)
    ((Equiv.symm (equivPair (G := G) i) : (a : Pair d i) → NormalWord d)
        (Pair.mk (G := G)
          (Word.Pair.mk (M := G)
            (HMul.hMul (β := G i) (x * x_1)
              (Word.Pair.head (M := G)
                  (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                    ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) x_2)) :
                G i))
            (Word.Pair.tail (M := G) (i := i)
              (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) x_2)))
            ⋯)
          ⋯) :
      NormalWord (G := G) d)
    ((Equiv.symm (equivPair (G := G) i) : (a : Pair d i) → NormalWord d)
        (Pair.mk (G := G)
          (Word.Pair.mk (M := G)
            (HMul.hMul (β := G i) x
              (Word.Pair.head (M := G)
                  (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                    ((equivPair (G := G) i : (a : NormalWord d) → Pair d i)
                      ((Equiv.symm (equivPair (G := G) i) : (a : Pair d i) → NormalWord d)
                        (Pair.mk (G := G)
                          (Word.Pair.mk (M := G)
                            (HMul.hMul (β := G i) x_1
                              (Word.Pair.head (M := G)
                                  (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                                    ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) x_2)) :
                                G i))
                            (Word.Pair.tail (M := G) (i := i)
                              (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                                ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) x_2)))
                            ⋯)
                          ⋯)))) :
                G i))
            (Word.Pair.tail (M := G) (i := i)
              (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                ((equivPair (G := G) i : (a : NormalWord d) → Pair d i)
                  ((Equiv.symm (equivPair (G := G) i) : (a : Pair d i) → NormalWord d)
                    (Pair.mk (G := G)
                      (Word.Pair.mk (M := G)
                        (HMul.hMul (β := G i) x_1
                          (Word.Pair.head (M := G)
                              (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                                ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) x_2)) :
                            G i))
                        (Word.Pair.tail (M := G) (i := i)
                          (Pair.toPair.{u_1, u_2, u_3} (G := G) (H := H) (φ := φ) (d := d)
                            ((equivPair (G := G) i : (a : NormalWord d) → Pair d i) x_2)))
                        ⋯)
                      ⋯)))))
            ⋯)
          ⋯) :
      NormalWord (G := G) d)

Tactic:
simp [mul_assoc, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, mul_assoc