English
In a given open cover, the composite of t with fst followed by fst again is equal to the composite with snd followed by fst, expressing a symmetry constraint in the second level of pullback tringles.
Русский
В открытом покрытии композиция t с fst и затем ещё fst равна композиции с snd затем fst, выражая симметрию в втором уровне pullback-структур.
LaTeX
$$$t 𝒰 f g i j ≫ pullback.fst _ _ ≫ pullback.fst _ _ = pullback.snd _ _$$$
Lean4
@[simp, reassoc]
theorem t_fst_fst (i j : 𝒰.I₀) : t 𝒰 f g i j ≫ pullback.fst _ _ ≫ pullback.fst _ _ = pullback.snd _ _ := by
simp only [t, Category.assoc, pullbackSymmetry_hom_comp_fst_assoc, pullbackAssoc_hom_snd_fst, pullback.lift_fst_assoc,
pullbackSymmetry_hom_comp_snd, pullbackAssoc_inv_fst_fst, pullbackSymmetry_hom_comp_fst]
