isLimitAux — Mathlib

Lean4
/-- This is a slightly more convenient method to verify that a pullback cone is a limit cone. It
only asks for a proof of facts that carry any mathematical content -/
def isLimitAux (t : PullbackCone f g) (lift : ∀ s : PullbackCone f g, s.pt ⟶ t.pt)
    (fac_left : ∀ s : PullbackCone f g, lift s ≫ t.fst = s.fst)
    (fac_right : ∀ s : PullbackCone f g, lift s ≫ t.snd = s.snd)
    (uniq :
      ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt) (_ : ∀ j : WalkingCospan, m ≫ t.π.app j = s.π.app j), m = lift s) :
    IsLimit t :=
  { lift
    fac := fun s j =>
      Option.casesOn j
        (by
          rw [← s.w inl, ← t.w inl, ← Category.assoc]
          congr
          exact fac_left s)
        fun j' => WalkingPair.casesOn j' (fac_left s) (fac_right s)
    uniq := uniq }
Похожие утверждения