-- 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)
m : CoprodI G
one :
  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)ᵐᵒᵖ) (CoprodI.of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          1))
      1 =
    1
of :
  ∀ (m : ι) (ih : G m),
    HMul.hMul (α := CoprodI G) (β := 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)ᵐᵒᵖ) (CoprodI.of (M := G)) :
                      (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                    (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
                (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
              ((CoprodI.of (M := G) : (a : G m) → CoprodI G) ih)) :
          CoprodI G)
        ((CoprodI.of (M := G) : (a : G m) → CoprodI G) ih : CoprodI G) =
      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)ᵐᵒᵖ) (CoprodI.of (M := G)) :
                  (G i)ᵐᵒᵖ →* (CoprodI G)ᵐᵒᵖ)
                (MulEquiv.toMonoidHom (MulEquiv.inv' (G i)) : G i →* (G i)ᵐᵒᵖ) :
            (a : CoprodI G) → (CoprodI G)ᵐᵒᵖ)
          m) *
      m =
    1
have mul : ∀ (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)ᵐᵒᵖ) (CoprodI.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)ᵐᵒᵖ) (CoprodI.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),
  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)ᵐᵒᵖ) (CoprodI.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
Tactic: induction m using CoprodI.induction_on with
      | one => rw [map_one, MulOpposite.unop_one, one_mul]
      | of m ih =>
        change of _⁻¹ * of _ = 1
        rw [← of.map_mul, inv_mul_cancel, of.map_one]
      | mul x y ihx ihy =>
        rw [map_mul, MulOpposite.unop_mul, mul_assoc, ← mul_assoc _ x y, ihx, one_mul,
          ihy]
Cleared hypotheses: m