-- 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)
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
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
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)) (k : I) (fkj : k ⟶ i)
    (e : D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V 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
refine_1 :
  ∀ (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)) (k : I) (fkj : k ⟶ i)
    (e : D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k = ⊤),
    IsOpenCover.{u_1, u} (X := ↥(D.obj k)) fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)
refine_2 refine_2₁ :
  ∀ (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)) (k : I) (fkj : k ⟶ i)
    (e : D.map fkj ⁻¹ᵁ ⨆ (k : J), ⨆ (hk : k ∈ s), D.map (fi k hk) ⁻¹ᵁ V k = ⊤) (k_1 : ↥s),
    U (↑k_1 : J) = c.π.app k ⁻¹ᵁ (fun (x : ↥s) ↦ D.map (fkj ≫ fi (↑x : J) ⋯) ⁻¹ᵁ V (↑x : J)) k_1
⊢ ∃ (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]

Premises used: AlgebraicGeometry.exists_isAffineOpen_preimage_eq, Eq.ge, TopologicalSpace.IsOpenCover.iSup_set_eq_univ, iSup_subtype, AlgebraicGeometry.Scheme.Hom.preimage_iSup, AlgebraicGeometry.Scheme.Hom.comp_preimage, IsCompact.elim_finite_subcover, TopologicalSpace.Opens.isOpen, isCompact_univ, CategoryTheory.Limits.Cone.w, CategoryTheory.Functor.map_comp