-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
| (CategoryStruct.comp (Y :=
      TensorBimod.X M
        ({ X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
              right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }.tensorBimod
          N))
      (coequalizer.π
          (M.actRight ▷
            TensorBimod.X
              { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
              N)
          (Iso.hom
              (α_ M.X Y.X
                (TensorBimod.X
                  { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                  N)) ≫
            M.X ◁
              TensorBimod.actLeft
                { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }
                N) :
        tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)) ⟶
          coequalizer (X :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X)
              (TensorBimod.X
                { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                N))
            (M.actRight ▷
              TensorBimod.X
                { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                N)
            (Iso.hom
                (α_ M.X Y.X
                  (TensorBimod.X
                    { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                      right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                    N)) ≫
              M.X ◁
                TensorBimod.actLeft
                  { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ }
                  N))
      (colimMap
        (parallelPairHom
          (M.actRight ▷
            TensorBimod.X
              { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
              N)
          (Iso.hom
              (α_ M.X Y.X
                (TensorBimod.X
                  { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                  N)) ≫
            M.X ◁
              TensorBimod.actLeft
                { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }
                N)
          (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)
          (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ LeftUnitorBimod.hom N) (M.X ◁ LeftUnitorBimod.hom N) ⋯ ⋯)) :
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)) ⟶
      TensorBimod.X M N)
have a : (M.X ◁ LeftUnitorBimod.hom N ≫
    colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one :
  (parallelPair (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X)
            (TensorBimod.X
              { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
              N))
          (M.actRight ▷
            TensorBimod.X
              { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
              N)
          (Iso.hom
              (α_ M.X Y.X
                (TensorBimod.X
                  { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                    right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
                  N)) ≫
            M.X ◁
              TensorBimod.actLeft
                { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                  right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
                N)).obj
      WalkingParallelPair.one ⟶
    colimit (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)))
Tactic: rw [ι_colimMap, parallelPairHom_app_one]