-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ Functor.obj (Functor.const I) S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : LocallyOfFinitePresentation f
inst_3 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_4 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_5 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = CategoryTheory.Functor.map (Functor.const I) (a ≫ f)
𝒰 :
  IsOpenCover (X := ↥c.pt)
    fun
      (V :
        { x :
          TopologicalSpace.Opens ↥c.pt ×
            { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
              x.1 ∈ X.affineOpens ∧
                x.1 ≤
                  (Opens.comap (TopCat.Hom.hom f.base) : (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                    (↑x.2 : TopologicalSpace.Opens ↥S) } //
          Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt)) c.pt.affineOpens x.1 ∧
            x.1 ≤
              (Opens.comap (TopCat.Hom.hom a.base) : (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) ↦
    (↑V :
        TopologicalSpace.Opens ↥c.pt ×
          { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
            x.1 ∈ X.affineOpens ∧
              x.1 ≤
                (Opens.comap (TopCat.Hom.hom f.base) : (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                  (↑x.2 : TopologicalSpace.Opens ↥S) }).1
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
have obtain : ∀ (i : I)
  (s :
    Finset
      { x :
        TopologicalSpace.Opens ↥c.pt ×
          { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
            x.1 ∈ X.affineOpens ∧
              x.1 ≤
                (Opens.comap (TopCat.Hom.hom f.base) : (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                  (↑x.2 : TopologicalSpace.Opens ↥S) } //
        Membership.mem (γ := Set (TopologicalSpace.Opens ↥c.pt)) c.pt.affineOpens x.1 ∧
          x.1 ≤
            (Opens.comap (TopCat.Hom.hom a.base) : (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
              (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 })
  (𝒱 : ↥s → (D.obj i).Opens) (h𝒱 : IsOpenCover 𝒱)
  (h𝒱𝒰 :
    ∀ (j : ↥s),
      IsAffineOpen (𝒱 j) ∧
        (↑(↑j :
                  { x :
                    TopologicalSpace.Opens ↥c.pt ×
                      { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                        x.1 ∈ X.affineOpens ∧
                          x.1 ≤
                            (Opens.comap (TopCat.Hom.hom f.base) :
                                (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                              (↑x.2 : TopologicalSpace.Opens ↥S) } //
                    x.1 ∈ c.pt.affineOpens ∧
                      x.1 ≤
                        (Opens.comap (TopCat.Hom.hom a.base) :
                            (a : TopologicalSpace.Opens ↥X) → TopologicalSpace.Opens ↥c.pt)
                          (↑x.2 : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).1 }) :
              TopologicalSpace.Opens ↥c.pt ×
                { x : TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u) //
                  x.1 ∈ X.affineOpens ∧
                    x.1 ≤
                      (Opens.comap (TopCat.Hom.hom f.base) :
                          (a : TopologicalSpace.Opens ↥S) → TopologicalSpace.Opens ↥X)
                        (↑x.2 : TopologicalSpace.Opens ↥S) }).1 =
          c.π.app i ⁻¹ᵁ 𝒱 j),
  ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
Tactic: obtain ⟨i, s, 𝒱, h𝒱, h𝒱𝒰⟩ := Scheme.exists_isOpenCover_and_isAffine D c hc _ 𝒰 fun U ↦ U.2.1