-- 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))
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ (↑U : Set ↥(D.obj i))
this : ∀ (j : Over i), IsAffine.{u} ((opensDiagram D i U).obj j)
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hj :
  Eq (α := (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop ((opensDiagram D i U).map f)) :
          (a : (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u)) →
            (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ((Over.forget i ⋙ D).obj (Over.mk (𝟙 i)), ⊤))
                (Scheme.Hom.appTop ((opensDiagramι D i U).app (Over.mk (𝟙 i)))) :
              (a : (↑Γ((Over.forget i ⋙ D).obj (Over.mk (𝟙 i)), ⊤) : Type u)) →
                (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u))
            s :
          (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u)) :
      (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
    (0 : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
hf : Over.Hom.left f = j.hom
t' : Γ((↑(D.map j.hom ⁻¹ᵁ U) : Scheme), ⊤) ⟶ Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) :=
  (D.obj j.left).presheaf.map (Quiver.Hom.op (eqToHom ⋯))
⊢ Eq (α := (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app (D.map j.hom) U) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) s U ⋯ :
          ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
            ((D.obj i).presheaf.obj (Opposite.op U))) :
      (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) t' :
          (a : (↑Γ((↑(D.map j.hom ⁻¹ᵁ U) : Scheme), ⊤) : Type u)) → (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop ((opensDiagram D i U).map f)) :
              (a : (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u)) →
                (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X := Γ((Over.forget i ⋙ D).obj (Over.mk (𝟙 i)), ⊤))
                    (Scheme.Hom.appTop ((opensDiagramι D i U).app (Over.mk (𝟙 i)))) :
                  (a : (↑Γ((Over.forget i ⋙ D).obj (Over.mk (𝟙 i)), ⊤) : Type u)) →
                    (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u))
                s :
              (↑Γ((opensDiagram D i U).obj (Over.mk (𝟙 i)), ⊤) : Type u)) :
          (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u)) :
      (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
have h : Eq (α := (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.app (D.map j.hom) U) :
        (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := (D.obj i).presheaf.obj (Opposite.op ⊤)) (Y :=
              (D.obj i).presheaf.obj (Opposite.op U)) ((D.obj i).presheaf.map (Quiver.Hom.op (homOfLE sorry))) :
            (a : (↑((D.obj i).presheaf.obj (Opposite.op ⊤)) : Type u)) →
              (↑((D.obj i).presheaf.obj (Opposite.op U)) : Type u))
          s :
        (↑((D.obj i).presheaf.obj (Opposite.op U)) : Type u)) :
    (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) t' :
        (a : (↑Γ((↑(D.map j.hom ⁻¹ᵁ U) : Scheme), ⊤) : Type u)) → (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier)
              (Scheme.Hom.appTop
                (Scheme.Hom.resLE (D.map (Over.Hom.left f)) (D.map (𝟙 i) ⁻¹ᵁ U) (D.map j.hom ⁻¹ᵁ U) sorry)) :
            (a : (↑Γ((↑(D.map (𝟙 i) ⁻¹ᵁ U) : Scheme), ⊤) : Type u)) → (↑Γ((↑(D.map j.hom ⁻¹ᵁ U) : Scheme), ⊤) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Γ(D.obj i, ⊤)) (Y := Γ((↑(D.map (𝟙 i) ⁻¹ᵁ U) : Scheme), ⊤))
                  ((D.obj i).presheaf.map (Quiver.Hom.op (homOfLE sorry))) :
                (a : (↑Γ(D.obj i, ⊤) : Type u)) → (↑Γ((↑(D.map (𝟙 i) ⁻¹ᵁ U) : Scheme), ⊤) : Type u))
              s :
            (↑Γ((↑(D.map (𝟙 i) ⁻¹ᵁ U) : Scheme), ⊤) : Type u)) :
        (↑Γ((↑(D.map j.hom ⁻¹ᵁ U) : Scheme), ⊤) : Type u)) :
    (↑Γ(D.obj j.left, D.map j.hom ⁻¹ᵁ U) : Type u))
Tactic: dsimp [TopCat.Presheaf.restrictOpen, TopCat.Presheaf.restrict]