-- 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)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
J : Type u_1
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
have have₁ have₂ :
  ∀ (this : CompactSpace.{u} ↥c.pt),
    ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
      IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j
have₃ :
  ∀ (this : CompactSpace.{u} ↥c.pt) (j : (k : J) → I) (V : (k : J) → (D.obj (j k)).Opens)
    (hV : ∀ (k : J), IsAffineOpen (V k)) (hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k),
    ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
      IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j
have₄ :
  ∀ (this : CompactSpace.{u} ↥c.pt) (j : (k : J) → I) (V : (k : J) → (D.obj (j k)).Opens)
    (hV : ∀ (k : J), IsAffineOpen (V k)) (hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k) (s : Finset J)
    (hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))),
    ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
      IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j
have₅ :
  ∀ (this : CompactSpace.{u} ↥c.pt) (j : (k : J) → I) (V : (k : J) → (D.obj (j k)).Opens)
    (hV : ∀ (k : J), IsAffineOpen (V k)) (hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k) (s : Finset J)
    (hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))) (i : I)
    (fi : ∀ {X : I}, X ∈ Finset.image j s → Nonempty.{u + 1} (i ⟶ X)),
    ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
      IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j
⊢ ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
    IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j
have have₆ : ∀ (this : CompactSpace.{u} ↥c.pt) (j : (k : J) → I) (V : (k : J) → (D.obj (j k)).Opens)
  (hV : ∀ (k : J), IsAffineOpen (V k)) (hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k) (s : Finset J)
  (hs : Subset.{u} (α := Set ↥c.pt) Set.univ (⋃ i ∈ s, (↑(U i) : Set ↥c.pt))) (i : I)
  (fi : (k : J) → k ∈ s → (i ⟶ j k)),
  ∃ (i : I) (s : Finset J) (V : ↥s → (D.obj i).Opens),
    IsOpenCover V ∧ ∀ (j : ↥s), IsAffineOpen (V j) ∧ U (↑j : J) = c.π.app i ⁻¹ᵁ V j
Tactic: classical
  have := compactSpace_of_isLimit D c hc
  choose j V hV hVU using fun k ↦ exists_isAffineOpen_preimage_eq D c hc (U k) (hU' k)
  obtain ⟨s, hs⟩ := isCompact_univ.elim_finite_subcover _
    (fun i ↦ (U i).isOpen) hU.iSup_set_eq_univ.ge
  obtain ⟨i, fi⟩ := IsCofiltered.inf_objs_exists (s.image j)
  replace fi : ∀ k ∈ s, i ⟶ j k := fun k hk ↦ (fi (Finset.mem_image_of_mem _ hk)).some
  obtain ⟨k, fkj, e⟩ := exists_map_eq_top D c hc (⨆ (k) (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k) (by
    simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, c.w, hVU]
    exact top_le_iff.mp fun x _ ↦ by simpa using hs (Set.mem_univ x))
  refine ⟨k, s, fun x ↦ D.map (fkj ≫ fi x.1 x.2) ⁻¹ᵁ V _, ?_, fun k ↦ ⟨(hV k).preimage _, ?_⟩⟩
  · refine top_le_iff.mp (e.symm.trans_le ?_)
    simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, iSup_subtype, ← D.map_comp]
    simp
  · rw [← hVU, ← Hom.comp_preimage, c.w]