-- Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit
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
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
fi'i : i' ⟶ i
hi' :
  ∀ (j : ↥s),
    D.map fi'i ⁻¹ᵁ 𝒱 j ≤
      t.app i' ⁻¹ᵁ
        (↑(↑(↑(↑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) }).2 :
                TopologicalSpace.Opens ↥X × (↑S.affineOpens : Type u)).2 :
          TopologicalSpace.Opens ↥S)
k : I
fki : k ⟶ i
ak : (j : ↥s) → (↑(D.map fki ⁻¹ᵁ 𝒱 j) : Scheme) ⟶ X
hak : ∀ (j : ↥s), ak j ≫ f = (D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app k
hak' : ∀ (j : ↥s), c.π.app k ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j = (c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ a
obtain :
  ∀ (l : I) (flk : l ⟶ k)
    (hl :
      ∀ (j₁ j₂ : ↥s),
        (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₁ ≫ ak j₁ =
          (D.obj l).homOfLE ⋯ ≫ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j₂ ≫ ak j₂),
    ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i
⊢ ∃ (i : I) (g : D.obj i ⟶ X), c.π.app i ≫ g = a ∧ g ≫ f = t.app i

Tactic:
obtain ⟨l, flk, hl⟩ : ∃ (l : I) (flk : l ⟶ k), ∀ j₁ j₂, Scheme.homOfLE _ inf_le_left ≫
      D.map flk ∣_ _ ≫ ak j₁ = Scheme.homOfLE _ inf_le_right ≫ D.map flk ∣_ _ ≫ ak j₂ := by
    let 𝒱' := (D.map fki ⁻¹ᵁ 𝒱 ·)
    have (j₁ j₂ : s) : ∃ (l : I) (flk : l ⟶ k), Scheme.homOfLE _ inf_le_left ≫ D.map flk ∣_ _ ≫
        ak j₁ = Scheme.homOfLE _ inf_le_right ≫ D.map flk ∣_ _ ≫ ak j₂ := by
      have _ (x) : CompactSpace ↥((opensDiagram D k (𝒱' j₁ ⊓ 𝒱' j₂)).obj x) :=
        isCompact_iff_compactSpace.mp (QuasiCompact.isCompact_preimage _ (𝒱' j₁ ⊓ 𝒱' j₂).isOpen
          (((h𝒱𝒰 _).1.preimage _).isCompact.inter_of_isOpen ((h𝒱𝒰 _).1.preimage _).isCompact
            (D.map fki ⁻¹ᵁ 𝒱 j₁).2 (D.map fki ⁻¹ᵁ 𝒱 j₂).2))
      obtain ⟨⟨l, ⟨⟨⟩⟩, flk⟩, ⟨flk', ⟨⟨⟨⟩⟩⟩, h⟩, e⟩ :=
        Scheme.exists_hom_comp_eq_comp_of_locallyOfFiniteType _
          (opensDiagramι .. ≫ (Over.forget k).whiskerLeft t) f _
          (isLimitOpensCone D c hc k (𝒱' j₁ ⊓ 𝒱' j₂)) (i := .mk (𝟙 k))
          (Scheme.homOfLE _ (by simp [𝒱']) ≫ ak j₁) (Scheme.homOfLE _ (by simp [𝒱']) ≫ ak j₂)
          (by simp [hak]) (by simp [hak]) (by simp; simp [Hom.resLE, hak'])
      obtain rfl : flk = flk' := by simpa using h.symm
      refine ⟨l, flk, by simpa [← Scheme.Hom.resLE_eq_morphismRestrict] using e⟩
    choose l flk hflk using this
    obtain ⟨l', fl'k, fl'l, hl'⟩ := IsCofiltered.wideCospan (I := s × s) fun x ↦ flk x.1 x.2
    refine ⟨l', fl'k, fun j₁ j₂ ↦ ?_⟩
    have H : (D.map fl'k ≫ D.map fki) ⁻¹ᵁ (𝒱 j₁ ⊓ 𝒱 j₂) ≤
        (D.map (fl'l (j₁, j₂)) ≫ D.map (flk j₁ j₂) ≫ D.map fki) ⁻¹ᵁ (𝒱 j₁ ⊓ 𝒱 j₂) := by
      simp only [← Functor.map_comp, reassoc_of% hl']; rfl
    simpa [← Scheme.Hom.resLE_eq_morphismRestrict, Scheme.Hom.resLE_comp_resLE_assoc,
      ← Functor.map_comp, hl'] using congr((D.map (fl'l (j₁, j₂))).resLE _ _ H ≫ $(hflk j₁ j₂))