-- 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)
i : I
inst_3 : CompactSpace.{u} ↥(D.obj i)
s : (↑Γ(D.obj i, ⊤) : Type u)
hs :
  Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop (c.π.app i)) :
          (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, ⊤) : Type u))
U : (x : ↥(D.obj i)) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : (x : ↥(D.obj i)) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H :
  ∀ (x : ↥(D.obj i)),
    Eq (α := (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(D.obj i, U x)) (Scheme.Hom.app (D.map (f x)) (U x)) :
            (a : (↑Γ(D.obj i, U x) : Type u)) → (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) s (U x) ⋯ :
            ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
              ((D.obj i).presheaf.obj (Opposite.op (U x)))) :
        (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
      (0 : (↑Γ(D.obj (j x), D.map (f x) ⁻¹ᵁ U x) : Type u))
t : Finset ↥(D.obj i)
ht : Eq.{u + 1} (α := Set ↥(D.obj i)) (⋃ x ∈ t, (↑(U x) : Set ↥(D.obj i))) ⊤
obtain :
  ∀ (k : I) (fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X))
    (hk :
      ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
        Membership.mem (γ :=
            Finset
              ((X : I) ×'
                (Y : I) ×' (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y)))
            (Finset.image
              (fun (x : ↥t) ↦
                PSigma.mk (β := fun (X : I) ↦
                  (Y : I) ×' (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y))
                  (j (↑x : ↥(D.obj i)))
                  (PSigma.mk (β := fun (Y : I) ↦
                    (_ : j (↑x : ↥(D.obj i)) ∈ insert i (Finset.image j t)) ×'
                      (_ : Y ∈ insert i (Finset.image j t)) ×' (j (↑x : ↥(D.obj i)) ⟶ Y))
                    i
                    (PSigma.mk (β := fun (x_1 : j (↑x : ↥(D.obj i)) ∈ insert i (Finset.image j t)) ↦
                      (_ : i ∈ insert i (Finset.image j t)) ×' (j (↑x : ↥(D.obj i)) ⟶ i)) ⋯
                      (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j t)) ↦ j (↑x : ↥(D.obj i)) ⟶ i) ⋯
                        (f (↑x : ↥(D.obj i)))))))
              t.attach)
            (PSigma.mk (β := fun (X : I) ↦
              (Y : I) ×' (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y)) X
              (PSigma.mk (β := fun (Y : I) ↦
                (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y)) Y
                (PSigma.mk (β := fun (x : X ∈ insert i (Finset.image j t)) ↦
                  (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y)) mX
                  (PSigma.mk (β := fun (x : Y ∈ insert i (Finset.image j t)) ↦ X ⟶ Y) mY f_1)))) →
          fk mX ≫ f_1 = fk mY),
    ∃ (j : I) (f : j ⟶ i),
      Eq (α := (↑Γ(D.obj j, ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop (D.map f)) :
              (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
            s :
          (↑Γ(D.obj j, ⊤) : Type u))
        (0 : (↑Γ(D.obj j, ⊤) : Type u))
⊢ ∃ (j : I) (f : j ⟶ i),
    Eq (α := (↑Γ(D.obj j, ⊤) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop (D.map f)) :
            (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ(D.obj j, ⊤) : Type u))
          s :
        (↑Γ(D.obj j, ⊤) : Type u))
      (0 : (↑Γ(D.obj j, ⊤) : Type u))

Tactic:
obtain ⟨k, fk, hk⟩ := IsCofiltered.inf_exists (insert i <| t.image j) (by
    exact t.attach.image fun x ↦ ⟨j x.1, i, Finset.mem_insert_of_mem
      (Finset.mem_image_of_mem _ x.2), by simp, f x.1⟩)

Premises used: Insert.insert, Finset.image, CategoryTheory.IsCofiltered.inf_exists