English
Left whiskering is compatible with (g ∘ g') via composition rules.
Русский
Левое whisker совместимо с (g ∘ g') через правила композиции.
LaTeX
$$$eHomWhiskerLeft\,V\,X\, (g \circ g') = eHomWhiskerLeft\,V\,X\, g \, \circ \, eHomWhiskerLeft\,V\,X\, g'.$$$
Lean4
@[simp, reassoc]
theorem eHomWhiskerLeft_comp (X : C) {Y Y' Y'' : C} (g : Y ⟶ Y') (g' : Y' ⟶ Y'') :
eHomWhiskerLeft V X (g ≫ g') = eHomWhiskerLeft V X g ≫ eHomWhiskerLeft V X g' :=
by
dsimp [eHomWhiskerLeft]
rw [assoc, assoc, eHomEquiv_comp, MonoidalCategory.whiskerLeft_comp_assoc, MonoidalCategory.whiskerLeft_comp_assoc, ←
e_assoc, tensorHom_def, MonoidalCategory.whiskerRight_id_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
MonoidalCategory.whiskerLeft_comp_assoc, MonoidalCategory.whiskerLeft_comp_assoc, whiskerLeft_rightUnitor_assoc,
whiskerLeft_rightUnitor_inv_assoc, triangle_assoc_comp_left_inv_assoc, MonoidalCategory.whiskerRight_id_assoc,
Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc, associator_inv_naturality_right_assoc, Iso.hom_inv_id_assoc,
whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc, Iso.inv_hom_id_assoc]
