-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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
⊢ ∃ (i : I) (V : (D.obj i).Opens), IsCompact (↑V : Set ↥(D.obj i)) ∧ c.π.app i ⁻¹ᵁ V = U
have 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)
                  sorry))
            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
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']
Cleared hypotheses: U, hU