Lean4
/-- The underlying morphism of the forward component of the associator isomorphism. -/
noncomputable def hom : ((P.tensorBimod Q).tensorBimod L).X ⟶ (P.tensorBimod (Q.tensorBimod L)).X :=
coequalizer.desc (homAux P Q L)
(by
dsimp [homAux]
refine (cancel_epi ((tensorRight _ ⋙ tensorRight _).map (coequalizer.π _ _))).1 ?_
dsimp [TensorBimod.X]
slice_lhs 1 2 => rw [← comp_whiskerRight, TensorBimod.π_tensor_id_actRight, comp_whiskerRight, comp_whiskerRight]
slice_lhs 3 5 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
slice_lhs 2 3 => rw [associator_naturality_middle]
slice_lhs 3 4 => rw [← whiskerLeft_comp, coequalizer.condition, whiskerLeft_comp, whiskerLeft_comp]
slice_rhs 1 2 => rw [associator_naturality_left]
slice_rhs 2 3 => rw [← whisker_exchange]
slice_rhs 3 5 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
simp)
