-- 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)
i : I
inst_3 : CompactSpace.{u} ↥(D.obj 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))
U : (x : ↥(D.obj i)) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : (x : ↥(D.obj i)) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H :
  ∀ (x : ↥(D.obj i)),
    Eq (α := (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(D.obj i, U x)) (Scheme.Hom.app (D.map (f x)) (U x)) :
            (a : (↑Γ(D.obj i, U x) : Type u)) → (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) s (U x) ⋯ :
            ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
              ((D.obj i).presheaf.obj (Opposite.op (U x)))) :
        (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
      (0 : (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
t : Finset ↥(D.obj i)
ht : Eq.{u + 1} (α := Set ↥(D.obj i)) (⋃ x ∈ t, (↑(U x) : Set ↥(D.obj i))) ⊤
k : I
fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
    Membership.mem (γ :=
        Finset
          ((X : I) ×'
            (Y : I) ×' (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y)))
        (Finset.image
          (fun (x : ↥t) ↦
            PSigma.mk (β := fun (X : I) ↦
              (Y : I) ×' (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y))
              (j (↑x : ↥(D.obj i)))
              (PSigma.mk (β := fun (Y : I) ↦
                (_ : j (↑x : ↥(D.obj i)) ∈ insert i (Finset.image j t)) ×'
                  (_ : Y ∈ insert i (Finset.image j t)) ×' (j (↑x : ↥(D.obj i)) ⟶ Y))
                i
                (PSigma.mk (β := fun (x_1 : j (↑x : ↥(D.obj i)) ∈ insert i (Finset.image j t)) ↦
                  (_ : i ∈ insert i (Finset.image j t)) ×' (j (↑x : ↥(D.obj i)) ⟶ i)) ⋯
                  (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j t)) ↦ j (↑x : ↥(D.obj i)) ⟶ i) ⋯
                    (f (↑x : ↥(D.obj i)))))))
          t.attach)
        (PSigma.mk (β := fun (X : I) ↦
          (Y : I) ×' (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y)) X
          (PSigma.mk (β := fun (Y : I) ↦
            (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y)) Y
            (PSigma.mk (β := fun (x : X ∈ insert i (Finset.image j t)) ↦
              (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y)) mX
              (PSigma.mk (β := fun (x : Y ∈ insert i (Finset.image j t)) ↦ X ⟶ Y) mY f_1)))) →
      fk mX ≫ f_1 = fk mY
x : ↥(D.obj k)
obtain :
  ∀ (l : ↥(D.obj i)) (hl : l ∈ t)
    (hlU : Membership.mem (α := ↥(D.obj i)) (↑(U l) : Set ↥(D.obj i)) ((D.map (fk ⋯)) x : ↥(D.obj i))),
    ∃ (V : TopologicalSpace.Opens ↥(D.obj k)) (hV : V ≤ Opposite.unop (Opposite.op ⊤)),
      x ∈ V ∧
        Eq (α := (↑((D.obj k).presheaf.obj (Opposite.op V)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) ((D.obj k).presheaf.map (homOfLE hV).op) :
                (a : (↑((D.obj k).presheaf.obj (Opposite.op (Opposite.unop (Opposite.op ⊤)))) : Type u)) →
                  (↑((D.obj k).presheaf.obj (Opposite.op V)) : Type u))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (Scheme.Hom.appTop (D.map (fk ⋯))) :
                    (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
                  s :
                (↑Γ(D.obj k, ⊤) : Type u)) :
            (↑((D.obj k).presheaf.obj (Opposite.op V)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) ((D.obj k).presheaf.map (homOfLE hV).op) :
                (a : (↑((D.obj k).presheaf.obj (Opposite.op (Opposite.unop (Opposite.op ⊤)))) : Type u)) →
                  (↑((D.obj k).presheaf.obj (Opposite.op V)) : Type u))
              0 :
            (↑((D.obj k).presheaf.obj (Opposite.op V)) : Type u))
⊢ ∃ (V : TopologicalSpace.Opens ↥(D.obj k)) (hV : V ≤ Opposite.unop (Opposite.op ⊤)),
    x ∈ V ∧
      Eq (α := (↑((D.obj k).presheaf.obj (Opposite.op V)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) ((D.obj k).presheaf.map (homOfLE hV).op) :
              (a : (↑((D.obj k).presheaf.obj (Opposite.op (Opposite.unop (Opposite.op ⊤)))) : Type u)) →
                (↑((D.obj k).presheaf.obj (Opposite.op V)) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Scheme.Hom.appTop (D.map (fk ⋯))) :
                  (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(D.obj k, ⊤) : Type u))
                s :
              (↑Γ(D.obj k, ⊤) : Type u)) :
          (↑((D.obj k).presheaf.obj (Opposite.op V)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) ((D.obj k).presheaf.map (homOfLE hV).op) :
              (a : (↑((D.obj k).presheaf.obj (Opposite.op (Opposite.unop (Opposite.op ⊤)))) : Type u)) →
                (↑((D.obj k).presheaf.obj (Opposite.op V)) : Type u))
            0 :
          (↑((D.obj k).presheaf.obj (Opposite.op V)) : Type u))

Tactic:
obtain ⟨l, hl, hlU⟩ := Set.mem_iUnion₂.mp (ht.ge (Set.mem_univ ((D.map (fk (by simp))).base x)))

Premises used: Eq.ge, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Set.mem_iUnion₂, CategoryTheory.Functor.map, Iff.mp, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe