isPullbackOfIsTerminalIsProduct — Mathlib

Lean4
/-- The product is the pullback over the terminal object. -/
def isPullbackOfIsTerminalIsProduct {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : W ⟶ X) (k : W ⟶ Y) (H₁ : IsTerminal Z)
    (H₂ : IsLimit (BinaryFan.mk h k)) : IsLimit (PullbackCone.mk _ _ (show h ≫ f = k ≫ g from H₁.hom_ext _ _)) :=
  by
  apply PullbackCone.isLimitAux'
  intro s
  use H₂.lift (BinaryFan.mk s.fst s.snd)
  use H₂.fac (BinaryFan.mk s.fst s.snd) ⟨WalkingPair.left⟩
  use H₂.fac (BinaryFan.mk s.fst s.snd) ⟨WalkingPair.right⟩
  intro m h₁ h₂
  apply H₂.hom_ext
  rintro ⟨⟨⟩⟩
  · exact h₁.trans (H₂.fac (BinaryFan.mk s.fst s.snd) ⟨WalkingPair.left⟩).symm
  · exact h₂.trans (H₂.fac (BinaryFan.mk s.fst s.snd) ⟨WalkingPair.right⟩).symm
Похожие утверждения