-- 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))
⊢ ∀ (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))

Tactic:
fun i s t e ↦ ⟨_, Quiver.Hom.op _,
      (exists_app_map_eq_map_of_isLimit _ _ hc isCompact_univ s t e).choose_spec.choose_spec⟩

Premises used: Exists.choose_spec, Classical.indefiniteDescription, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, AlgebraicGeometry.Scheme.Hom.app, Opposite.op, AlgebraicGeometry.exists_app_map_eq_map_of_isLimit, Exists.intro, Exists.choose, Top.top, Subtype.val, Eq, DFunLike.coe