-- 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 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_2 : LocallyOfFiniteType f
inst_3 : IsCofiltered I
inst_4 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun (i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀) ↦
      ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover,
    h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)) → I
hki' : (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)) → k j ⟶ A.i'
heq :
  ∀ (j : PreZeroHypercover.I₀ (S := D.obj A.i') (Precoverage.ZeroHypercover.toPreZeroHypercover A.𝒰D)),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := OpenCover.finiteSubcover A.𝒰D
h : Nonempty.{u + 1} ↥(D.obj A.i')
O : Finset I := {A.i'} ∪ Finset.image (fun (i : 𝒰Df.I₀) ↦ k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i')))) Finset.univ
o : 𝒰Df.I₀ := Nonempty.some ⋯
ho : k (Cover.idx A.𝒰D (↑o : ↥(D.obj A.i'))) ∈ O
inr :
  ∀ (l : I) (hl1 : {X : I} → X ∈ O → (l ⟶ X))
    (hl2 :
      ∀ {X_1 Y : I} (mX : X_1 ∈ O) (mY : Y ∈ O) {f_1 : X_1 ⟶ Y},
        Membership.mem (γ := Finset ((X : I) ×' (Y : I) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)))
            (Finset.image
              (fun (i : 𝒰Df.I₀) ↦
                PSigma.mk (β := fun (X : I) ↦ (Y : I) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
                  (k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))))
                  (PSigma.mk (β := fun (Y : I) ↦
                    (_ : k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))) ∈ O) ×'
                      (_ : Y ∈ O) ×' (k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))) ⟶ Y))
                    A.i'
                    (PSigma.mk (β := fun (x : k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))) ∈ O) ↦
                      (_ : A.i' ∈ O) ×' (k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))) ⟶ A.i')) ⋯
                      (PSigma.mk (β := fun (x : A.i' ∈ O) ↦ k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))) ⟶ A.i') ⋯
                        (hki' (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))))))))
              Finset.univ)
            (PSigma.mk (β := fun (X : I) ↦ (Y : I) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X_1
              (PSigma.mk (β := fun (Y : I) ↦ (_ : X_1 ∈ O) ×' (_ : Y ∈ O) ×' (X_1 ⟶ Y)) Y
                (PSigma.mk (β := fun (x : X_1 ∈ O) ↦ (_ : Y ∈ O) ×' (X_1 ⟶ Y)) mX
                  (PSigma.mk (β := fun (x : Y ∈ O) ↦ X_1 ⟶ Y) mY f_1)))) →
          hl1 mX ≫ f_1 = hl1 mY),
    ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b
⊢ ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b

Tactic:
obtain ⟨l, hl1, hl2⟩ := IsCofiltered.inf_exists O
    (Finset.univ.image (fun i : 𝒰Df.I₀ ↦
      ⟨k <| A.𝒰D.idx i.1, A.i', by simp [O], by simp [O], hki' <| A.𝒰D.idx i.1⟩))

Premises used: Finset.univ, AlgebraicGeometry.ExistsHomHomCompEqCompAux.i', PSigma.mk, AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰D, AlgebraicGeometry.Scheme.Cover.idx, Subtype.val, Finset.image, CategoryTheory.IsCofiltered.inf_exists