English
The repeated left inclusion composed with the associator collapses to a single left inclusion; the two-stage inclusion reduces to one.
Русский
Повторное левое включение, за которым следует ассоциатор, сводится к одному левому включению; двухступенчатое включение упрощается до одного.
LaTeX
$$$\\forall x,y,z:\\; inl_{x,y} \\; \\circ inl_{y,z} \\; \\circ (\\alpha_{x,y,z})^{\\mathrm{hom}} = inl_{x,z}.$$$
Lean4
@[reassoc (attr := simp)]
theorem inl_comp_inl_comp_associator (x y z : AugmentedSimplexCategory) :
inl _ _ ≫ inl _ _ ≫ (α_ x y z).hom = inl _ _ :=
match x, y, z with
| .of x, .of y, .of z => by
change inl' _ _ ≫ inl' _ _ ≫ WithInitial.down _ = inl' _ _
ext i : 3
dsimp [MonoidalCategoryStruct.associator, associator]
have e₁ := inl'_eval x y i
have e₂ := inl'_eval x (tensorObjOf y z) i
have e₃ := inl'_eval (tensorObjOf x y) z <| Fin.cast (by simp +arith) <| i.castAdd (y.len + 1)
simp only [SimplexCategory.len_mk] at e₁ e₂ e₃
rw [e₁, e₂, e₃]
ext; simp +arith
| .star, _, _ => by cat_disch
| _, .star, _ => by cat_disch
| _, _, .star => by cat_disch
