Lean4
/-- The underlying morphism of the inverse component of the associator isomorphism. -/
noncomputable def inv : (P.tensorBimod (Q.tensorBimod L)).X ⟶ ((P.tensorBimod Q).tensorBimod L).X :=
coequalizer.desc (invAux P Q L)
(by
dsimp [invAux]
refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
dsimp [TensorBimod.X]
slice_lhs 1 2 => rw [whisker_exchange]
slice_lhs 2 4 => rw [id_tensor_π_preserves_coequalizer_inv_desc]
slice_lhs 1 2 => rw [associator_inv_naturality_left]
slice_lhs 2 3 => rw [← comp_whiskerRight, coequalizer.condition, comp_whiskerRight, comp_whiskerRight]
slice_rhs 1 2 => rw [associator_naturality_right]
slice_rhs 2 3 => rw [← whiskerLeft_comp, TensorBimod.whiskerLeft_π_actLeft, whiskerLeft_comp, whiskerLeft_comp]
slice_rhs 4 6 => rw [id_tensor_π_preserves_coequalizer_inv_desc]
slice_rhs 3 4 => rw [associator_inv_naturality_middle]
monoidal)
