Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ 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
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₂
h𝒲 : IsOpenCover fun k_1 ↦
  (Opens.comap (TopCat.Hom.hom (D.map flk).base)) ((Opens.comap (TopCat.Hom.hom (D.map fki).base)) (𝒱 k_1)) :=
  IsOpenCover.comap (IsOpenCover.comap h𝒱 (TopCat.Hom.hom (D.map fki).base)) (TopCat.Hom.hom (D.map flk).base)
𝒲 : (D.obj l).OpenCover := (D.obj l).openCoverOfIsOpenCover (fun x ↦ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 x) h𝒲
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i

Tactic:
let F := 𝒲.glueMorphisms (fun j ↦ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j) (fun j₁ j₂ ↦ by
      rw [← cancel_epi (isPullback_opens_inf _ _).isoPullback.hom]
      simpa [𝒲] using! hl j₁ j₂)

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ 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
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₂
h𝒲 : IsOpenCover fun k_1 ↦
  (Opens.comap (TopCat.Hom.hom (D.map flk).base)) ((Opens.comap (TopCat.Hom.hom (D.map fki).base)) (𝒱 k_1)) :=
  IsOpenCover.comap (IsOpenCover.comap h𝒱 (TopCat.Hom.hom (D.map fki).base)) (TopCat.Hom.hom (D.map flk).base)
𝒲 : (D.obj l).OpenCover := (D.obj l).openCoverOfIsOpenCover (fun x ↦ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 x) h𝒲
F : D.obj l ⟶ X := Cover.glueMorphisms 𝒲 (fun j ↦ D.map flk ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j) ⋯
⊢ ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i