-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J (Under R)
inst_2 :
  PreservesColimit (F ⋙ Under.forget R)
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))
c : Cocone F
hc : IsColimit c
i j : J
f₁ : (F ⋙ Functor.obj coyoneda (Opposite.op S)).obj i
f₂ : (F ⋙ Functor.obj coyoneda (Opposite.op S)).obj j
e_1 :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj.{vJ, u, uJ, u + 1}
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op S))
            (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)))
        i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op S)).mapCocone c).pt).obj i))
        f₁ :
      (fun (X : Type u) ↦ X)
        (Functor.obj.{vJ, u, uJ, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op S))
              (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)))
          i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)) j) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op S)).mapCocone c).pt).obj j))
        f₂ :
      (fun (X : Type u) ↦ X)
        (Functor.obj.{vJ, u, uJ, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op S))
              (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)))
          j))
k : J
hik : i ⟶ k
hjk : j ⟶ k
e : Under.Hom.right f₁ ≫ (F ⋙ Under.forget R).map hik = Under.Hom.right f₂ ≫ (F ⋙ Under.forget R).map hjk
⊢ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).map f) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i)) →
              (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj k))
          f₁ :
        (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).map g) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj k))
          f₂ :
        (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj k))

Tactic:
⟨k, hik, hjk, Under.UnderMorphism.ext e⟩

Premises used: CategoryTheory.Under.UnderMorphism.ext, Exists.intro