-- 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
apply :
  ∀ (x : ↥(D.obj k)),
    Membership.mem (γ := TopologicalSpace.Opens ↥(D.obj k)) (Opposite.unop (Opposite.op ⊤)) x →
      ∃ (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))
⊢ Eq (α := (↑Γ(D.obj k, ⊤) : 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))
    (0 : (↑Γ(D.obj k, ⊤) : Type u))

Tactic:
apply (D.obj k).IsSheaf.section_ext

Premises used: TopCat.Presheaf.IsSheaf.section_ext, AlgebraicGeometry.SheafedSpace.IsSheaf, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace