∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X₁ X₂ S : C}
  (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S) [inst_3 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂) (CategoryTheory.forget C)]
  (x₁ : CategoryTheory.ToType X₁) (x₂ : CategoryTheory.ToType X₂)
  (h : (CategoryTheory.ConcreteCategory.hom f₁) x₁ = (CategoryTheory.ConcreteCategory.hom f₂) x₂),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f₁ f₂))
      (CategoryTheory.Limits.Concrete.pullbackMk f₁ f₂ x₁ x₂ h) =
    x₂