-- Module: Mathlib.GroupTheory.CoprodI
Goal:
ι_1 : Type u_1
M : ι_1 → Type u_2
inst : (i : ι_1) → Monoid (M i)
N : Type u_3
inst_1 : Monoid N
ι : Type u_1
i : ι
a : Unit
refine_4 :
  Eq.{u_1 + 1} (α := CoprodI fun (x : ι) ↦ FreeGroup Unit)
    (((MonoidHom.comp (N := CoprodI fun (x : ι) ↦ FreeGroup Unit)
              (MonoidHom.comp (N := FreeGroup ι)
                ((FreeGroup.lift :
                    (a : ι → CoprodI fun (x : ι) ↦ FreeGroup Unit) →
                      FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit)
                  fun (i : ι) ↦
                  ((of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i) :
                        FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
                      (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
                    (FreeGroup.of ()))
                ((lift (M := fun (x : ι) ↦ FreeGroup Unit) :
                    (a : (i : ι) → FreeGroup Unit →* FreeGroup ι) →
                      (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι)
                  fun (i : ι) ↦
                  (FreeGroup.lift : (a : Unit → FreeGroup ι) → FreeGroup Unit →* FreeGroup ι) fun (x : Unit) ↦
                    FreeGroup.of i))
              (of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i)) :
            FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
          (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
        (FreeGroup.of PUnit.unit) :
      CoprodI fun (x : ι) ↦ FreeGroup Unit)
    (((MonoidHom.comp (MonoidHom.id (CoprodI fun (x : ι) ↦ FreeGroup Unit))
              (of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i)) :
            FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
          (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
        (FreeGroup.of PUnit.unit) :
      CoprodI fun (x : ι) ↦ FreeGroup Unit)
⊢ Eq.{u_1 + 1} (α := CoprodI fun (x : ι) ↦ FreeGroup Unit)
    (((MonoidHom.comp (N := CoprodI fun (x : ι) ↦ FreeGroup Unit)
              (MonoidHom.comp (N := FreeGroup ι)
                ((FreeGroup.lift :
                    (a : ι → CoprodI fun (x : ι) ↦ FreeGroup Unit) →
                      FreeGroup ι →* CoprodI fun (x : ι) ↦ FreeGroup Unit)
                  fun (i : ι) ↦
                  ((of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i) :
                        FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
                      (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
                    (FreeGroup.of ()))
                ((lift (M := fun (x : ι) ↦ FreeGroup Unit) :
                    (a : (i : ι) → FreeGroup Unit →* FreeGroup ι) →
                      (CoprodI fun (x : ι) ↦ FreeGroup Unit) →* FreeGroup ι)
                  fun (i : ι) ↦
                  (FreeGroup.lift : (a : Unit → FreeGroup ι) → FreeGroup Unit →* FreeGroup ι) fun (x : Unit) ↦
                    FreeGroup.of i))
              (of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i)) :
            FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
          (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
        (FreeGroup.of a) :
      CoprodI fun (x : ι) ↦ FreeGroup Unit)
    (((MonoidHom.comp (MonoidHom.id (CoprodI fun (x : ι) ↦ FreeGroup Unit))
              (of (M := fun (x : ι) ↦ FreeGroup Unit) (i := i)) :
            FreeGroup Unit →* CoprodI fun (x : ι) ↦ FreeGroup Unit) :
          (a : FreeGroup Unit) → CoprodI fun (x : ι) ↦ FreeGroup Unit)
        (FreeGroup.of a) :
      CoprodI fun (x : ι) ↦ FreeGroup Unit)

Tactic:
cases a