-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this :
  ReflectsFilteredColimits
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
refine_1 :
  ∀
    (x :
      Cocone.pt (F :=
        (D.op ⋙ Scheme.Γ) ⋙
          forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
        (Functor.mapCocone
          (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
          (Scheme.Γ.mapCocone c.op))),
    ∃ (i : Iᵒᵖ) (xi :
      (fun (X : Type u) ↦ X)
        (((D.op ⋙ Scheme.Γ) ⋙
              forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier)).obj
          i)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone
                    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier))
                    (Scheme.Γ.mapCocone c.op)))
                i) :
            (a : (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)) →
              (fun (X : Type u) ↦ X)
                (((Functor.const Iᵒᵖ).obj ((forget CommRingCat).mapCocone (Scheme.Γ.mapCocone c.op)).pt).obj i))
          xi
refine_2 :
  ∀ (i : Iᵒᵖ)
    (x y :
      (fun (X : Type u) ↦ X)
        (((D.op ⋙ Scheme.Γ) ⋙
              forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier)).obj
          i)),
    Eq (α :=
        (fun (X : Type u) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const Iᵒᵖ)
              (Cocone.pt (F :=
                (D.op ⋙ Scheme.Γ) ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier))
                (Functor.mapCocone
                  (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier))
                  (Scheme.Γ.mapCocone c.op))))
            i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (Cocone.ι
                    (Functor.mapCocone
                      (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier))
                      (Scheme.Γ.mapCocone c.op)))
                  i) :
              (a : (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)) →
                (fun (X : Type u) ↦ X)
                  (((Functor.const Iᵒᵖ).obj ((forget CommRingCat).mapCocone (Scheme.Γ.mapCocone c.op)).pt).obj i))
            x :
          (fun (X : Type u) ↦ X)
            (Functor.obj
              (Functor.obj (Functor.const Iᵒᵖ)
                (Cocone.pt (F :=
                  (D.op ⋙ Scheme.Γ) ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier))
                  (Functor.mapCocone
                    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier))
                    (Scheme.Γ.mapCocone c.op))))
              i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (Cocone.ι
                    (Functor.mapCocone
                      (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier))
                      (Scheme.Γ.mapCocone c.op)))
                  i) :
              (a : (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)) →
                (fun (X : Type u) ↦ X)
                  (((Functor.const Iᵒᵖ).obj ((forget CommRingCat).mapCocone (Scheme.Γ.mapCocone c.op)).pt).obj i))
            y :
          (fun (X : Type u) ↦ X)
            (Functor.obj
              (Functor.obj (Functor.const Iᵒᵖ)
                (Cocone.pt (F :=
                  (D.op ⋙ Scheme.Γ) ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier))
                  (Functor.mapCocone
                    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier))
                    (Scheme.Γ.mapCocone c.op))))
              i)) →
      ∃ (k : Iᵒᵖ) (f : i ⟶ k),
        Eq (α :=
          (fun (X : Type u) ↦ X)
            (((D.op ⋙ Scheme.Γ) ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier)).obj
              k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (((D.op ⋙ Scheme.Γ) ⋙
                        forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier)).map
                    f) :
                (a : (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)) →
                  (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj k))
              x :
            (fun (X : Type u) ↦ X)
              (((D.op ⋙ Scheme.Γ) ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier)).obj
                k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (((D.op ⋙ Scheme.Γ) ⋙
                        forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier)).map
                    f) :
                (a : (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)) →
                  (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj k))
              y :
            (fun (X : Type u) ↦ X)
              (((D.op ⋙ Scheme.Γ) ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier)).obj
                k))
⊢ Nonempty.{u + 2} (IsColimit (Scheme.Γ.mapCocone c.op))

Tactic:
refine ReflectsColimit.reflects (F := forget _) (Types.FilteredColimit.isColimitOf' _ _ ?_ ?_)

Premises used: CategoryTheory.Limits.ReflectsColimit.reflects, CategoryTheory.Limits.Types.FilteredColimit.isColimitOf'