English
For any f:X→Y, g:Z→Y, the preimage of pullbackDiagonal f under map_fst equals pullbackDiagonal of (f ∘ g).
Русский
Преобразование предварительного образа диагонали через map_fst даёт диагональ в композиции f∘g.
LaTeX
$$$(\\mathrm{map\\_fst}\ f\ g)^{-1}(\\mathrm{pullbackDiagonal}\ f) = \\mathrm{pullbackDiagonal}(f \\circ g)$$$
Lean4
theorem preimage_map_fst_pullbackDiagonal {f : X → Y} {g : Z → Y} :
@map_fst X Y Z f g ⁻¹' pullbackDiagonal f = pullbackDiagonal (@snd X Y Z f g) :=
by
ext ⟨⟨p₁, p₂⟩, he⟩
simp_rw [pullbackDiagonal, mem_setOf, Subtype.ext_iff, Prod.ext_iff]
exact (and_iff_left he).symm