-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
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
⊢ ∃ (k : I) (hik : k ⟶ i), D.map hik ≫ a = D.map hik ≫ b
have 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')) sorry
                    (PSigma.mk (β := fun (x : A.i' ∈ O) ↦ k (Cover.idx A.𝒰D (↑i : ↥(D.obj A.i'))) ⟶ A.i') sorry
                      (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
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⟩))