-- Lean 4 proof step from Mathlib.GroupTheory.PushoutI (goal)
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
⊢ (x * x_1) • x_2 = x • x_1 • x_2
have dsimp : 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)))
          sorry)
        sorry) :
    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)))
                          sorry)
                        sorry)))) :
              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)))
                      sorry)
                    sorry)))))
          sorry)
        sorry) :
    NormalWord (G := G) d)
Tactic: dsimp +instances [instHSMul]