-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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))) ⊤
⊢ ∃ (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))
have 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)) sorry
                    (PSigma.mk (β := fun (x_1 : i ∈ insert i (Finset.image j t)) ↦ j (↑x : ↥(D.obj i)) ⟶ i) sorry
                      (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))
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⟩)