-- 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
U : (D.obj i).Opens
hU : IsCompact (↑U : Set ↥(D.obj i))
s : (↑Γ(D.obj i, U) : Type u)
hs :
  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))
        s :
      (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
    (0 : (↑Γ(((Functor.const I).obj c.pt).obj i, c.π.app i ⁻¹ᵁ U) : Type u))
this : CompactSpace.{u} ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hf :
  Eq (α := (↑Γ((↑(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)
            (Scheme.Hom.appTop (Scheme.Hom.resLE (D.map (Over.Hom.left f)) (D.map (𝟙 i) ⁻¹ᵁ U) (D.map j.hom ⁻¹ᵁ U) ⋯)) :
          (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, U)) (Y := Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤))
                ((D.obj i).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u))
            s :
          (↑Γ(D.obj i, (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤) : Type u)) :
      (↑Γ((↑(D.map j.hom ⁻¹ᵁ U) : Scheme), ⊤) : Type u))
    (0 : (↑Γ((opensDiagram D i U).obj j, ⊤) : Type u))
hf' : Over.Hom.left f = j.hom
⊢ Eq (α := (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ 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 (Over.Hom.left f)) U) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(D.obj i, U)) (Y := Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U))
            ((D.obj i).presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫
              Scheme.Hom.appTop (Scheme.Hom.resLE (D.map (Over.Hom.left f)) (D.map (𝟙 i) ⁻¹ᵁ U) (D.map j.hom ⁻¹ᵁ U) ⋯) ≫
                (D.obj j.left).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑Γ(D.obj i, U) : Type u)) → (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U) : Type u))
        s :
      (↑Γ(D.obj j.left, D.map (Over.Hom.left f) ⁻¹ᵁ U) : Type u))
have h : Scheme.Hom.app (D.map (Over.Hom.left f)) U =
  (D.obj i).presheaf.map (Quiver.Hom.op (homOfLE sorry)) ≫
    Scheme.Hom.appTop (Scheme.Hom.resLE (D.map (Over.Hom.left f)) (D.map (𝟙 i) ⁻¹ᵁ U) (D.map j.hom ⁻¹ᵁ U) sorry) ≫
      (D.obj j.left).presheaf.map (Quiver.Hom.op (homOfLE sorry))
Tactic: congr! 2