Lean4
/-- Suppose `f` and `g` are two morphisms with a common codomain and `s` is a limit cone over the
diagram formed by `f` and `g`. Suppose `f` and `g` both factor through a monomorphism `h` via
`x` and `y`, respectively. Then `s` is also a limit cone over the diagram formed by `x` and `y`. -/
def isLimitOfFactors (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ Z) [Mono h] (x : X ⟶ W) (y : Y ⟶ W) (hxh : x ≫ h = f)
(hyh : y ≫ h = g) (s : PullbackCone f g) (hs : IsLimit s) :
IsLimit
(PullbackCone.mk _ _
(show s.fst ≫ x = s.snd ≫ y from (cancel_mono h).1 <| by simp only [Category.assoc, hxh, hyh, s.condition])) :=
PullbackCone.isLimitAux' _ fun t =>
have : fst t ≫ x ≫ h = snd t ≫ y ≫ h := by -- Porting note: reassoc workaround
rw [← Category.assoc, ← Category.assoc]
apply congrArg (· ≫ h) t.condition
⟨hs.lift (PullbackCone.mk t.fst t.snd <| by rw [← hxh, ← hyh, this]),
⟨hs.fac _ WalkingCospan.left, hs.fac _ WalkingCospan.right, fun hr hr' =>
by
apply PullbackCone.IsLimit.hom_ext hs <;> simp only [PullbackCone.mk_fst, PullbackCone.mk_snd] at hr hr' ⊢ <;>
simp only [hr, hr'] <;>
symm
exacts [hs.fac _ WalkingCospan.left, hs.fac _ WalkingCospan.right]⟩⟩
