∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S}
  (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.lift
        (CategoryTheory.Limits.equalizer.lift
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.equalizer.ι
              (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
                (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
              (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
                (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
            (CategoryTheory.Limits.pullback.fst s v))
          ⋯)
        (CategoryTheory.Limits.pullback.lift
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.equalizer.ι
              (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
                (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
              (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
                (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
            (CategoryTheory.Limits.pullback.fst s v))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.equalizer.ι
              (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
                (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
              (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
                (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
            (CategoryTheory.Limits.pullback.snd s v))
          ⋯)
        ⋯)
      (CategoryTheory.Limits.equalizer.lift
        (CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.equalizer.ι f g)
          (CategoryTheory.Limits.pullback.fst s v) s v (CategoryTheory.Limits.equalizer.ι f g)
          (CategoryTheory.Limits.pullback.snd s v) s ⋯ ⋯)
        ⋯) =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.Limits.equalizer
        (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
        (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))