pullbackCongr_hom_app_left_fst — Mathlib

English

If f = g, then the same left-projection equality holds in the pullback congruence as in the previous case.

Русский

Если f = g, то то же самое равенство левой проекции сохраняется в конгруэнции вытяжки.

LaTeX

$$$ ((Over.pullbackCongr h).hom.app A).left \\;\\circ\\; pullback.fst A.hom g = pullback.fst A.hom f $$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackCongr_hom_app_left_fst {X Y : T} {f g : X ⟶ Y} (h : f = g) (A : P.Over Q Y) :
    ((Over.pullbackCongr h).hom.app A).left ≫ pullback.fst A.hom g = pullback.fst A.hom f :=
  by
  subst h
  simp [pullbackCongr]

Похожие утверждения