-- 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 : c.pt.Opens
hU : IsCompact (↑U : Set ↥c.pt)
obtain :
  ∀ (s : Set (TopologicalSpace.Opens ↥c.pt))
    (hs :
      s ⊆
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x})
    (hsf : s.Finite) (hU : IsCompact (↑(sSup s) : Set ↥c.pt)),
    ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
obtain₁ :
  ∀ (s : Set (TopologicalSpace.Opens ↥c.pt))
    (hs :
      s ⊆
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x})
    (hsf : s.Finite) (hU : IsCompact (↑(sSup s) : Set ↥c.pt)) (this : Finite.{u + 1} (↑s : Type u)),
    ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
obtain₂ :
  ∀ (s : Set (TopologicalSpace.Opens ↥c.pt))
    (hs :
      s ⊆
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x})
    (hsf : s.Finite) (hU : IsCompact (↑(sSup s) : Set ↥c.pt)) (this : Finite.{u + 1} (↑s : Type u))
    (i : (x : (↑s : Type u)) → I) (V : (x : (↑s : Type u)) → (D.obj (i x)).Opens)
    (hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x))
    (hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)),
    ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
obtain₃ :
  ∀ (s : Set (TopologicalSpace.Opens ↥c.pt))
    (hs :
      s ⊆
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x})
    (hsf : s.Finite) (hU : IsCompact (↑(sSup s) : Set ↥c.pt)) (this : Finite.{u + 1} (↑s : Type u))
    (i : (x : (↑s : Type u)) → I) (V : (x : (↑s : Type u)) → (D.obj (i x)).Opens)
    (hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x))
    (hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)) (j : I)
    (fj :
      ∀ {X : I},
        Membership.mem (γ := Finset I)
            (Finset.image
              (fun (x : ↥(hsf.toFinset (s := s))) ↦
                i
                  (Subtype.mk (p := fun (x : TopologicalSpace.Opens ↥c.pt) ↦ x ∈ s) (↑x : TopologicalSpace.Opens ↥c.pt)
                    ⋯))
              hsf.toFinset (s := s).attach)
            X →
          Nonempty.{u + 1} (j ⟶ X)),
    ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
obtain₄ :
  ∀ (s : Set (TopologicalSpace.Opens ↥c.pt))
    (hs :
      s ⊆
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x})
    (hsf : s.Finite) (hU : IsCompact (↑(sSup s) : Set ↥c.pt)) (this : Finite.{u + 1} (↑s : Type u))
    (i : (x : (↑s : Type u)) → I) (V : (x : (↑s : Type u)) → (D.obj (i x)).Opens)
    (hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x))
    (hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)) (j : I)
    (fj : (b : (↑s : Type u)) → j ⟶ i b),
    ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = sSup s
refine_1 :
  ∀ (s : Set (TopologicalSpace.Opens ↥c.pt))
    (hs :
      s ⊆
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x})
    (hsf : s.Finite) (hU : IsCompact (↑(sSup s) : Set ↥c.pt)) (this : Finite.{u + 1} (↑s : Type u))
    (i : (x : (↑s : Type u)) → I) (V : (x : (↑s : Type u)) → (D.obj (i x)).Opens)
    (hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x))
    (hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)) (j : I)
    (fj : (b : (↑s : Type u)) → j ⟶ i b), IsCompact (↑(⨆ (k : (↑s : Type u)), D.map (fj k) ⁻¹ᵁ V k) : Set ↥(D.obj j))
refine_2 refine_2₁ :
  ∀ (s : Set (TopologicalSpace.Opens ↥c.pt))
    (hs :
      s ⊆
        {x : TopologicalSpace.Opens ↥c.pt | ∃ (i : I) (V : (D.obj i).Opens) (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x})
    (hsf : s.Finite) (hU : IsCompact (↑(sSup s) : Set ↥c.pt)) (this : Finite.{u + 1} (↑s : Type u))
    (i : (x : (↑s : Type u)) → I) (V : (x : (↑s : Type u)) → (D.obj (i x)).Opens)
    (hV : ∀ (x : (↑s : Type u)), IsAffineOpen (V x))
    (hVi : ∀ (x : (↑s : Type u)), c.π.app (i x) ⁻¹ᵁ V x = (↑x : TopologicalSpace.Opens ↥c.pt)) (j : I)
    (fj : (b : (↑s : Type u)) → j ⟶ i b), c.π.app j ⁻¹ᵁ ⨆ (k : (↑s : Type u)), D.map (fj k) ⁻¹ᵁ V k = sSup s
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = U

Tactic:
classical
  obtain ⟨s, hs, hsf, rfl⟩ := (isBasis_preimage_isAffineOpen D c hc).exists_finite_of_isCompact hU
  have : Finite s := hsf
  choose i V hV hVi using fun x : s ↦ hs x.2
  obtain ⟨j, fj⟩ := IsCofiltered.inf_objs_exists (hsf.toFinset.attach.image
    fun x ↦ i ⟨x.1, (by simpa only [Set.Finite.mem_toFinset] using x.2)⟩:)
  replace fj : ∀ b : s, j ⟶ i b := fun b ↦ (@fj (i b) (by simpa using ⟨b.1, b.2, rfl⟩)).some
  refine ⟨j, ⨆ (k : s), D.map (fj _) ⁻¹ᵁ V k, ?_, ?_⟩
  · simp only [TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.carrier_eq_coe,
      TopologicalSpace.Opens.map_coe, TopologicalSpace.Opens.coe_mk]
    exact isCompact_iUnion fun i ↦ ((hV i).preimage _).isCompact
  · simp [-TopologicalSpace.Opens.iSup_mk, Scheme.Hom.preimage_iSup,
      ← Scheme.Hom.comp_preimage, c.w, hVi, sSup_eq_iSup']

Premises used: TopologicalSpace.Opens.map_coe, TopologicalSpace.Opens.iSup_mk, AlgebraicGeometry.Scheme.Hom.preimage_iSup, AlgebraicGeometry.isBasis_preimage_isAffineOpen, TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact, TopologicalSpace.Opens.coe_mk, AlgebraicGeometry.Scheme.Hom.comp_preimage, TopologicalSpace.Opens.carrier_eq_coe, CategoryTheory.Limits.Cone.w, rfl, sSup_eq_iSup'