-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
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
⊢ Nonempty
    (IsColimit (F := F ⋙ Functor.obj coyoneda (Opposite.op S))
      (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c))
have 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))
Tactic: refine ⟨Types.FilteredColimit.isColimitOf _ _ ?_ ?_⟩