-- 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)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
i : I
V : TopologicalSpace.Opens ↥(D.obj i)
hV : IsAffineOpen V
hxV : Membership.mem (α := ↥(D.obj i)) (↑V : Set ↥(D.obj i)) ((c.π.app i) x : ↥(D.obj i))
this_1 : ∀ (j : (Over i)ᵒᵖ), IsAffine.{u} (Opposite.unop ((opensDiagram D i V).op.obj j))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i V).obj j)
r : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V) : Type u)
hrU : (Functor.obj (Functor.obj (Functor.const I) c.pt) i).basicOpen r ≤ U
hxr :
  (↑(Subtype.mk (p := fun (x : ↥(Functor.obj (Functor.obj (Functor.const I) c.pt) i)) ↦ x ∈ U) x hxU) :
      ↥(((Functor.const I).obj c.pt).obj i)) ∈
    (Functor.obj (Functor.obj (Functor.const I) c.pt) i).basicOpen r
obtain :
  ∀ (j : Over i)
    (s :
      ((opensDiagram D i V).op ⋙
            Scheme.Γ ⋙
              forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier)).obj
        (Opposite.op j))
    (hs :
      Eq (α :=
        (fun (X : Type u) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const (Over i)ᵒᵖ)
              ((Scheme.Γ ⋙
                      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier)).mapCocone
                  (opensCone D c i V).op).pt)
            (Opposite.op j)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (((Scheme.Γ ⋙
                            forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                              (CC := CommRingCat.carrier)).mapCocone
                        (opensCone D c i V).op).ι.app
                  (Opposite.op j)) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (((opensDiagram D i V).op ⋙ Scheme.Γ ⋙ forget CommRingCat).obj (Opposite.op j))) →
                (fun (X : Type u) ↦ X)
                  (((Functor.const (Over i)ᵒᵖ).obj
                        ((Scheme.Γ ⋙ forget CommRingCat).mapCocone (opensCone D c i V).op).pt).obj
                    (Opposite.op j)))
            s :
          (fun (X : Type u) ↦ X)
            (Functor.obj
              (Functor.obj (Functor.const (Over i)ᵒᵖ)
                ((Scheme.Γ ⋙
                        forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier)).mapCocone
                    (opensCone D c i V).op).pt)
              (Opposite.op j)))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (c.π.app i ⁻¹ᵁ V).topIso.inv :
              (a : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ V) : Type u)) →
                (↑Γ((↑(c.π.app i ⁻¹ᵁ V) : Scheme), ⊤) : Type u))
            r :
          (↑Γ((↑(c.π.app i ⁻¹ᵁ V) : Scheme), ⊤) : Type u))),
    ∃ (U' : TopologicalSpace.Opens ↥c.pt),
      Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
          {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
          U' ∧
        x ∈ U' ∧ U' ≤ U
⊢ ∃ (U' : TopologicalSpace.Opens ↥c.pt),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt))
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U

Tactic:
obtain ⟨⟨j⟩, s, hs⟩ := (Types.jointly_surjective_of_isColimit (isColimitOfPreserves
    (Scheme.Γ ⋙ forget _) (isLimitOpensCone D c hc i V).op) ((c.π.app i ⁻¹ᵁ V).topIso.inv r))

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.IsLimit.op, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Opens.topIso, AlgebraicGeometry.Scheme.Γ, CategoryTheory.Functor.comp, AlgebraicGeometry.isLimitOpensCone, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, CategoryTheory.forget, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, DFunLike.coe, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.Limits.isColimitOfPreserves