-- 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
preserves :
  ∀
    (x :
      Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op S))
        (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)),
    ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj i)),
      x =
        (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))
          xi
preserves₁ :
  ∀ (i j : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj i))
    (xj : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj j)),
    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))
            xi :
          (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))
            xj :
          (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) (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))
              xi :
            (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))
              xj :
            (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj k))
⊢ Nonempty
    (IsColimit (F := F ⋙ Functor.obj coyoneda (Opposite.op S))
      (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c))

Tactic:
refine ⟨Types.FilteredColimit.isColimitOf _ _ ?_ ?_⟩