-- 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)
W X Y Z : Mon.{v₁, u₁} C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (TensorBimod.X N P) ⟶
      TensorBimod.X M'
        { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := ⋯, left_assoc := ⋯,
          actRight := TensorBimod.actRight N P, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ : Bimod X Z })
    (CategoryStruct.comp (Y :=
      coequalizer (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X X.X) (TensorBimod.X N P))
        (M.actRight ▷ TensorBimod.X N P) (Iso.hom (α_ M.X X.X (TensorBimod.X N P)) ≫ M.X ◁ TensorBimod.actLeft N P))
      (coequalizer.π (M.actRight ▷ TensorBimod.X N P)
        (Iso.hom (α_ M.X X.X (TensorBimod.X N P)) ≫ M.X ◁ TensorBimod.actLeft N P))
      (colimMap
        (parallelPairHom (M.actRight ▷ TensorBimod.X N P)
          (Iso.hom (α_ M.X X.X (TensorBimod.X N P)) ≫ M.X ◁ TensorBimod.actLeft N P) (M'.actRight ▷ TensorBimod.X N P)
          (Iso.hom (α_ M'.X X.X (TensorBimod.X N P)) ≫ M'.X ◁ TensorBimod.actLeft N P) (f.hom ▷ X.X ▷ TensorBimod.X N P)
          (f.hom ▷ TensorBimod.X N P) ⋯ ⋯)))
    (coequalizer.π (M.actRight ▷ TensorBimod.X N P)
        (Iso.hom (α_ M.X X.X (TensorBimod.X N P)) ≫ M.X ◁ TensorBimod.actLeft N P) ≫
      AssociatorBimod.inv M N P ≫
        colimMap
            (parallelPairHom (TensorBimod.actRight M N ▷ P.X)
              (Iso.hom (α_ (TensorBimod.X M N) Y.X P.X) ≫ TensorBimod.X M N ◁ P.actLeft)
              (TensorBimod.actRight M' N ▷ P.X)
              (Iso.hom (α_ (TensorBimod.X M' N) Y.X P.X) ≫ TensorBimod.X M' N ◁ P.actLeft)
              (colimMap
                    (parallelPairHom (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X)
                      (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷
                  Y.X ▷
                P.X)
              (colimMap
                  (parallelPairHom (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X)
                    (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷
                P.X)
              ⋯ ⋯) ≫
          AssociatorBimod.hom M' N P)
have h : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) M.X (TensorBimod.X N P) ⟶
    TensorBimod.X M'
      { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := sorry, left_assoc := sorry,
        actRight := TensorBimod.actRight N P, actRight_one := sorry, right_assoc := sorry, middle_assoc := sorry : Bimod X Z })
  (f.hom ▷ TensorBimod.X N P ≫
      colimit.ι
        (parallelPair (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X) (TensorBimod.X N P))
          (M'.actRight ▷ TensorBimod.X N P)
          (Iso.hom (α_ M'.X X.X (TensorBimod.X N P)) ≫ M'.X ◁ TensorBimod.actLeft N P))
        WalkingParallelPair.one :
    (parallelPair (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X X.X) (TensorBimod.X N P))
            (M.actRight ▷ TensorBimod.X N P)
            (Iso.hom (α_ M.X X.X (TensorBimod.X N P)) ≫ M.X ◁ TensorBimod.actLeft N P)).obj
        WalkingParallelPair.one ⟶
      colimit
        (parallelPair (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X) (TensorBimod.X N P))
          (M'.actRight ▷ TensorBimod.X N P)
          (Iso.hom (α_ M'.X X.X (TensorBimod.X N P)) ≫ M'.X ◁ TensorBimod.actLeft N P)))
  (coequalizer.π (M.actRight ▷ TensorBimod.X N P)
        (Iso.hom (α_ M.X X.X (TensorBimod.X N P)) ≫ M.X ◁ TensorBimod.actLeft N P) ≫
      AssociatorBimod.inv M N P ≫
        colimMap
            (parallelPairHom (TensorBimod.actRight M N ▷ P.X)
              (Iso.hom (α_ (TensorBimod.X M N) Y.X P.X) ≫ TensorBimod.X M N ◁ P.actLeft)
              (TensorBimod.actRight M' N ▷ P.X)
              (Iso.hom (α_ (TensorBimod.X M' N) Y.X P.X) ≫ TensorBimod.X M' N ◁ P.actLeft)
              (colimMap
                    (parallelPairHom (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X)
                      (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) sorry sorry) ▷
                  Y.X ▷
                P.X)
              (colimMap
                  (parallelPairHom (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X)
                    (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) sorry sorry) ▷
                P.X)
              sorry sorry) ≫
          AssociatorBimod.hom M' N P :
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (TensorBimod.X N P) ⟶
      TensorBimod.X M'
        { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := sorry, left_assoc := sorry,
          actRight := TensorBimod.actRight N P, actRight_one := sorry, right_assoc := sorry, middle_assoc := sorry : Bimod X Z })
Tactic: slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]