-- 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 : I), IsAffine.{u} (D.obj i)
i : I
s : (↑Γ(D.obj i, ⊤) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
this : ∀ (i : Iᵒᵖ), IsAffine.{u} (Opposite.unop (D.op.obj i))
obtain :
  ∀ (j : Iᵒᵖ) (f : Opposite.op i ⟶ j)
    (hj :
      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
            j))
        ((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 (Opposite.op i))) →
                (fun (X : Type u) ↦ X) ((D.op ⋙ Scheme.Γ ⋙ forget CommRingCat).obj j))
            s :
          (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
              j))
        ((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 (Opposite.op i))) →
                (fun (X : Type u) ↦ X) ((D.op ⋙ Scheme.Γ ⋙ forget CommRingCat).obj j))
            0 :
          (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
              j))),
    ∃ (j : I) (f : j ⟶ i),
      Eq (α := (↑Γ(D.obj j, ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop (D.map f)) :
              (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
            s :
          (↑Γ(D.obj j, ⊤) : Type u))
        (0 : (↑Γ(D.obj j, ⊤) : Type u))
⊢ ∃ (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop (D.map f)) :
            (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
          s :
        (↑Γ(D.obj j, ⊤) : Type u))
      (0 : (↑Γ(D.obj j, ⊤) : Type u))

Tactic:
obtain ⟨j, f, hj⟩ := (Types.FilteredColimit.isColimit_eq_iff'
    (isColimitOfPreserves (Scheme.Γ ⋙ forget _) hc.op) s (0 : Γ(D.obj i, ⊤))).mp
    (by dsimp at hs ⊢; simpa)

Premises used: CategoryTheory.Limits.IsLimit.op, AlgebraicGeometry.Scheme.Γ, CategoryTheory.Functor.comp, CategoryTheory.forget, Iff.mp, OfNat.ofNat, CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff', CategoryTheory.Limits.isColimitOfPreserves