-- Lean 4 proof step from Mathlib.GroupTheory.CoprodI (goal)
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
⊢ 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)
have 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)
Tactic: cases a
Cleared hypotheses: a