-- Module: Mathlib.GroupTheory.Coprod.Basic
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx :
  HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H) =
    1
mul_of :
  HMul.hMul (α := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      (HMul.hMul (α := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of (Sum.map Inv.inv Inv.inv x)) : G ∗ H)
        (HMul.hMul (α := G ∗ H) (β := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x) : G ∗ H)
          ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H))) =
    1
mul_of₁ :
  HMul.hMul (α := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      (HMul.hMul (β := G ∗ H)
        (HMul.hMul (α := G ∗ H) (β := G ∗ H)
          ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of (Sum.map Inv.inv Inv.inv x)) : G ∗ H)
          ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x) : G ∗ H))
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H)) =
    1
mul_of₂ :
  HMul.hMul (α := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      (HMul.hMul (α := G ∗ H) (β := G ∗ H) (1 : G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H)) =
    1
mul_of₃ mul_of₄ mul_of₅ mul_of₆ :
  HMul.hMul (α := G ∗ H) (β := G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
          ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
            (List.reverse
              (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
        G ∗ H)
      ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H) =
    1
⊢ HMul.hMul (α := G ∗ H) (β := G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H)
            ((ofList : (a : List (G ⊕ H)) → FreeMonoid (G ⊕ H))
              (List.reverse
                (List.map (Sum.map Inv.inv Inv.inv) ((toList : (a : FreeMonoid (G ⊕ H)) → List (G ⊕ H)) xs)))) :
          G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of (Sum.map Inv.inv Inv.inv x)) : G ∗ H) *
      HMul.hMul (α := G ∗ H) (β := G ∗ H) ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) (of x) : G ∗ H)
        ((mk : (a : FreeMonoid (G ⊕ H)) → G ∗ H) xs : G ∗ H) =
    1

Tactic:
rwa [mul_assoc, ← mul_assoc (mk (of _)), mk_of_inv_mul, one_mul]

Premises used: mul_assoc, Monoid.Coprod.mk, FreeMonoid.of, DFunLike.coe, Monoid.Coprod.mk_of_inv_mul, one_mul