Lean4
/-- An auxiliary morphism for the definition of the underlying morphism of the inverse component of
the associator isomorphism. -/
noncomputable def invAux : P.X ⊗ (Q.tensorBimod L).X ⟶ ((P.tensorBimod Q).tensorBimod L).X :=
(PreservesCoequalizer.iso (tensorLeft P.X) _ _).inv ≫
coequalizer.desc ((α_ _ _ _).inv ≫ (coequalizer.π _ _ ▷ L.X) ≫ coequalizer.π _ _)
(by
dsimp; dsimp [TensorBimod.X]
slice_lhs 1 2 => rw [associator_inv_naturality_middle]
rw [← Iso.inv_hom_id_assoc (α_ _ _ _) (P.X ◁ Q.actRight), comp_whiskerRight]
slice_lhs 3 4 => rw [← comp_whiskerRight, Category.assoc, ← TensorBimod.π_tensor_id_actRight, comp_whiskerRight]
slice_lhs 4 5 => rw [coequalizer.condition]
slice_lhs 3 4 => rw [associator_naturality_left]
slice_rhs 1 2 => rw [whiskerLeft_comp]
slice_rhs 2 3 => rw [associator_inv_naturality_right]
slice_rhs 3 4 => rw [whisker_exchange]
simp)
