English
Under the same hypotheses, for all i, j, k in 𝒰.I₀, the composition t'(𝒰) i j k followed by fst, fst, snd equals fst, fst, snd; that is t'(𝒰) i j k ≫ fst ≫ fst ≫ snd = fst ≫ fst ≫ snd.
Русский
При тех же предпосылках для любых i, j, k ∈ 𝒰.I₀ композиция t'(𝒰) i j k с последовательно идущими fst, fst, snd равна композиции fst, fst, snd.
LaTeX
$$$ t'_{\\mathcal{U}} f g i j k \\;\\gg\\; \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{snd} \\_ \\_ = \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{fst} \\_ \\_ \\;\\gg\\; \\mathrm{snd} \\_ \\_.$$
Lean4
@[simp, reassoc]
theorem t'_fst_fst_snd (i j k : 𝒰.I₀) :
t' 𝒰 f g i j k ≫ pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.snd _ _ =
pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.snd _ _ :=
by
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_fst_assoc, pullbackRightPullbackFstIso_inv_snd_fst_assoc,
pullback.lift_fst_assoc, t_fst_snd, pullbackRightPullbackFstIso_hom_fst_assoc]
