-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
G : ι → Type u_4
inst_2 : (i : ι) → Group (G i)
x y : CoprodI G
ihx :
  MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          x) *
      x =
    1
ihy :
  MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          y) *
      y =
    1
mul :
  MulOpposite.unop
        (HMul.hMul (α := (CoprodI G)ᵐᵒᵖ) (β := (CoprodI G)ᵐᵒᵖ)
          (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
                  MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                    ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                      (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                    (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
                (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
              x :
            (CoprodI G)ᵐᵒᵖ)
          (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
                  MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                    ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                      (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                    (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
                (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
              y :
            (CoprodI G)ᵐᵒᵖ)) *
      (x * y) =
    1
⊢ MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          (x * y)) *
      (x * y) =
    1
have mul₁ : HMul.hMul (α := CoprodI G)
      (MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          y))
      (MulOpposite.unop
        (((lift (M := G) : (a : (i : ι) → G i →* (CoprodI G)ᵐᵒᵖ) → CoprodI G →* (CoprodI G)ᵐᵒᵖ) fun (i : ι) ↦
              MonoidHom.comp (N := (G i)ᵐᵒᵖ)
                ((MonoidHom.op : (a : G i →* CoprodI G) → (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ) (of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          x)) *
    (x * y) =
  1
Tactic: rw [map_mul, MulOpposite.unop_mul, mul_assoc, ← mul_assoc _ x y, ihx, one_mul,
          ihy]