-- 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)
s : (↑Γ(c.pt, ⊤) : Type u)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this_1 : CompactSpace.{u} ↥c.pt
this :
  ∀ (x : ↥c.pt),
    ∃ (i : I) (U : (D.obj i).Opens) (_ : IsAffineOpen U) (_ :
      Membership.mem (α := ↥(D.obj i)) U ((c.π.app i) x : ↥(D.obj i))) (t : (↑Γ(D.obj i, U) : Type u)),
      Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.app (c.π.app i) U) :
              (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
            t :
          (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) s (c.π.app i ⁻¹ᵁ U) ⋯ :
          ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
            (c.pt.presheaf.obj (Opposite.op (c.π.app i ⁻¹ᵁ U))))
⊢ ∃ (i : I) (t : (↑Γ(D.obj i, ⊤) : Type u)),
    s =
      (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))
        t
have choose : ∀ (i : (x : ↥c.pt) → I) (U : (x : ↥c.pt) → (D.obj (i x)).Opens) (hU : ∀ (x : ↥c.pt), IsAffineOpen (U x))
  (hxU : ∀ (x : ↥c.pt), Membership.mem (α := ↥(D.obj (i x))) (U x) ((c.π.app (i x)) x : ↥(D.obj (i x))))
  (t : (x : ↥c.pt) → (↑Γ(D.obj (i x), U x) : Type u))
  (ht :
    ∀ (x : ↥c.pt),
      Eq (α := (↑Γ(((Functor.const I).obj c.pt).obj (i x), c.π.app (i x) ⁻¹ᵁ U x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := Γ(((Functor.const I).obj c.pt).obj (i x), c.π.app (i x) ⁻¹ᵁ U x))
                (Scheme.Hom.app (c.π.app (i x)) (U x)) :
              (a : (↑Γ(D.obj (i x), U x) : Type u)) →
                (↑Γ(((Functor.const I).obj c.pt).obj (i x), c.π.app (i x) ⁻¹ᵁ U x) : Type u))
            (t x) :
          (↑Γ(((Functor.const I).obj c.pt).obj (i x), c.π.app (i x) ⁻¹ᵁ U x) : Type u))
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) s (c.π.app (i x) ⁻¹ᵁ U x) sorry :
          ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
            (c.pt.presheaf.obj (Opposite.op (c.π.app (i x) ⁻¹ᵁ U x))))),
  ∃ (i : I) (t : (↑Γ(D.obj i, ⊤) : Type u)),
    s =
      (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))
        t
Tactic: choose i U hU hxU t ht using this
Cleared hypotheses: this