-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
of :
  prod (M := M)
      (rcons (M := M) (i := i)
        (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
        Pair.mk (M := M)
          (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
          (__src.tail (M := M)) ⋯)) =
    HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
of₁ :
  HMul.hMul (α := CoprodI M)
      ((CoprodI.of (M := M) : (a : M i) → CoprodI M)
        (Pair.head (M := M)
          (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
          Pair.mk (M := M)
            (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
            (__src.tail (M := M)) ⋯)))
      (prod (M := M)
        (Pair.tail (M := M) (i := i)
          (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
          Pair.mk (M := M)
            (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
            (__src.tail (M := M)) ⋯))) =
    HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
of₂ :
  HMul.hMul (α := CoprodI M) (β := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M)
        ((CoprodI.of (M := M) : (a : M i) → CoprodI M)
            (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w)) :
          CoprodI M) *
      prod (M := M)
        (Pair.tail (M := M) (i := i)
          (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
          Pair.mk (M := M)
            (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
            (__src.tail (M := M)) ⋯)) =
    HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
⊢ (HSMul.hSMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) w).prod (M := M) =
    HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
have of₃ : HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M)
    (HMul.hMul (α := CoprodI M) (β := CoprodI M)
      ((CoprodI.of (M := M) : (a : M i) → CoprodI M)
          (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w)) :
        CoprodI M)
      (prod (M := M)
        (Pair.tail (M := M) (i := i)
          (have __src : Pair M i := (equivPair (M := M) i : (a : Word M) → Pair M i) w;
          Pair.mk (M := M)
            (HMul.hMul (β := M i) m (Pair.head (M := M) ((equivPair (M := M) i : (a : Word M) → Pair M i) w) : M i))
            (__src.tail (M := M)) sorry)))) =
  HMul.hMul (α := CoprodI M) ((CoprodI.of (M := M) : (a : M i) → CoprodI M) m : CoprodI M) (w.prod (M := M))
Tactic: rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
      Equiv.symm_apply_apply]