-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X Y : Scheme
f_1 : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
⊢ Eq (α :=
    X.presheaf.stalk
        (Sigma.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
          (Sigma.mk (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
            x
            (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f hf))) ⟶
      R)
    (↑(Sigma.snd (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
          (Sigma.mk (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
            x
            (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f hf))) :
      X.presheaf.stalk ⟨x, ⟨f, hf⟩⟩.fst ⟶ R)
    (CategoryStruct.comp (Y :=
      X.presheaf.stalk
        (Sigma.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
          ((fun (f : Spec R ⟶ X) ↦
              (Sigma.mk (β := fun (x : ↥X) ↦
                  { f : X.presheaf.stalk x ⟶ R //
                    IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
                  (f (closedPoint (↑R : Type u)))
                  (Subtype.mk (p := fun (f_2 : X.presheaf.stalk (f (closedPoint (↑R : Type u))) ⟶ R) ↦
                    IsLocalHom (R := (↑(X.presheaf.stalk (f (closedPoint (↑R : Type u)))) : Type u)) (S :=
                      (↑R : Type u)) (CommRingCat.Hom.hom f_2))
                    (Scheme.stalkClosedPointTo f) ⋯) :
                (x : ↥X) ×
                  { f : X.presheaf.stalk x ⟶ R //
                    IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }))
            ((fun
                  (xf :
                    (x : ↥X) ×
                      { f : X.presheaf.stalk x ⟶ R //
                        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                          (CommRingCat.Hom.hom f) }) ↦
                Spec.map
                    (↑(xf.snd (β := fun (x : ↥X) ↦
                          { f : X.presheaf.stalk x ⟶ R //
                            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                              (CommRingCat.Hom.hom f) })) :
                      X.presheaf.stalk xf.fst ⟶ R) ≫
                  X.fromSpecStalk
                    (xf.fst (β := fun (x : ↥X) ↦
                      { f : X.presheaf.stalk x ⟶ R //
                        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                          (CommRingCat.Hom.hom f) })))
              (Sigma.mk (β := fun (x : ↥X) ↦
                { f : X.presheaf.stalk x ⟶ R //
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
                x
                (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f
                  hf))))))
      (Iso.hom (X.presheaf.stalkCongr ⋯))
      (↑(Sigma.snd (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
              ((fun (f : Spec R ⟶ X) ↦
                  (Sigma.mk (β := fun (x : ↥X) ↦
                      { f : X.presheaf.stalk x ⟶ R //
                        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                          (CommRingCat.Hom.hom f) })
                      (f (closedPoint (↑R : Type u)))
                      (Subtype.mk (p := fun (f_2 : X.presheaf.stalk (f (closedPoint (↑R : Type u))) ⟶ R) ↦
                        IsLocalHom (R := (↑(X.presheaf.stalk (f (closedPoint (↑R : Type u)))) : Type u)) (S :=
                          (↑R : Type u)) (CommRingCat.Hom.hom f_2))
                        (Scheme.stalkClosedPointTo f) ⋯) :
                    (x : ↥X) ×
                      { f : X.presheaf.stalk x ⟶ R //
                        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                          (CommRingCat.Hom.hom f) }))
                ((fun
                      (xf :
                        (x : ↥X) ×
                          { f : X.presheaf.stalk x ⟶ R //
                            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                              (CommRingCat.Hom.hom f) }) ↦
                    Spec.map
                        (↑(xf.snd (β := fun (x : ↥X) ↦
                              { f : X.presheaf.stalk x ⟶ R //
                                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                  (CommRingCat.Hom.hom f) })) :
                          X.presheaf.stalk xf.fst ⟶ R) ≫
                      X.fromSpecStalk
                        (xf.fst (β := fun (x : ↥X) ↦
                          { f : X.presheaf.stalk x ⟶ R //
                            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                              (CommRingCat.Hom.hom f) })))
                  (Sigma.mk (β := fun (x : ↥X) ↦
                    { f : X.presheaf.stalk x ⟶ R //
                      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
                    x
                    (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
                      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f
                      hf)))) :
            { f_2 :
              X.presheaf.stalk
                  (Sigma.fst (β := fun (x : ↥X) ↦
                    { f : X.presheaf.stalk x ⟶ R //
                      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
                    ((fun (f : Spec R ⟶ X) ↦
                        (Sigma.mk (β := fun (x : ↥X) ↦
                            { f : X.presheaf.stalk x ⟶ R //
                              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                (CommRingCat.Hom.hom f) })
                            (f (closedPoint (↑R : Type u)))
                            (Subtype.mk (p := fun (f_2 : X.presheaf.stalk (f (closedPoint (↑R : Type u))) ⟶ R) ↦
                              IsLocalHom (R := (↑(X.presheaf.stalk (f (closedPoint (↑R : Type u)))) : Type u)) (S :=
                                (↑R : Type u)) (CommRingCat.Hom.hom f_2))
                              (Scheme.stalkClosedPointTo f) ⋯) :
                          (x : ↥X) ×
                            { f : X.presheaf.stalk x ⟶ R //
                              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                (CommRingCat.Hom.hom f) }))
                      ((fun
                            (xf :
                              (x : ↥X) ×
                                { f : X.presheaf.stalk x ⟶ R //
                                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                    (CommRingCat.Hom.hom f) }) ↦
                          Spec.map
                              (↑(xf.snd (β := fun (x : ↥X) ↦
                                    { f : X.presheaf.stalk x ⟶ R //
                                      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                        (CommRingCat.Hom.hom f) })) :
                                X.presheaf.stalk xf.fst ⟶ R) ≫
                            X.fromSpecStalk
                              (xf.fst (β := fun (x : ↥X) ↦
                                { f : X.presheaf.stalk x ⟶ R //
                                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                    (CommRingCat.Hom.hom f) })))
                        (Sigma.mk (β := fun (x : ↥X) ↦
                          { f : X.presheaf.stalk x ⟶ R //
                            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                              (CommRingCat.Hom.hom f) })
                          x
                          (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
                            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                              (CommRingCat.Hom.hom f))
                            f hf))))) ⟶
                R //
              IsLocalHom (R :=
                (↑(X.presheaf.stalk
                      (Sigma.fst (β := fun (x : ↥X) ↦
                        { f : X.presheaf.stalk x ⟶ R //
                          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                            (CommRingCat.Hom.hom f) })
                        ((fun (f : Spec R ⟶ X) ↦
                            (Sigma.mk (β := fun (x : ↥X) ↦
                                { f : X.presheaf.stalk x ⟶ R //
                                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                    (CommRingCat.Hom.hom f) })
                                (f (closedPoint (↑R : Type u)))
                                (Subtype.mk (p := fun (f_3 : X.presheaf.stalk (f (closedPoint (↑R : Type u))) ⟶ R) ↦
                                  IsLocalHom (R := (↑(X.presheaf.stalk (f (closedPoint (↑R : Type u)))) : Type u)) (S :=
                                    (↑R : Type u)) (CommRingCat.Hom.hom f_3))
                                  (Scheme.stalkClosedPointTo f) ⋯) :
                              (x : ↥X) ×
                                { f : X.presheaf.stalk x ⟶ R //
                                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                    (CommRingCat.Hom.hom f) }))
                          ((fun
                                (xf :
                                  (x : ↥X) ×
                                    { f : X.presheaf.stalk x ⟶ R //
                                      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                        (CommRingCat.Hom.hom f) }) ↦
                              Spec.map
                                  (↑(xf.snd (β := fun (x : ↥X) ↦
                                        { f : X.presheaf.stalk x ⟶ R //
                                          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                            (CommRingCat.Hom.hom f) })) :
                                    X.presheaf.stalk xf.fst ⟶ R) ≫
                                X.fromSpecStalk
                                  (xf.fst (β := fun (x : ↥X) ↦
                                    { f : X.presheaf.stalk x ⟶ R //
                                      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                        (CommRingCat.Hom.hom f) })))
                            (Sigma.mk (β := fun (x : ↥X) ↦
                              { f : X.presheaf.stalk x ⟶ R //
                                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                  (CommRingCat.Hom.hom f) })
                              x
                              (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
                                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                  (CommRingCat.Hom.hom f))
                                f hf)))))) :
                  Type u))
                (S := (↑R : Type u)) (CommRingCat.Hom.hom f_2) }) :
        X.presheaf.stalk
            ((fun (f : Spec R ⟶ X) ↦ ⟨f (closedPoint (↑R : Type u)), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
                ((fun (xf : (x : ↥X) × { f : X.presheaf.stalk x ⟶ R // IsLocalHom (CommRingCat.Hom.hom f) }) ↦
                    Spec.map (↑xf.snd : X.presheaf.stalk xf.fst ⟶ R) ≫ X.fromSpecStalk xf.fst)
                  ⟨x, ⟨f, hf⟩⟩)).fst ⟶
          R))
have refine_2 : ∀ (U : Opens ↥X)
  (hxU :
    Sigma.fst (β := fun (x : ↥X) ↦
        { f : X.presheaf.stalk x ⟶ R //
          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
        (Sigma.mk (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
          x
          (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f hf)) ∈
      U),
  Eq (α := X.presheaf.obj (op U) ⟶ R)
    (CategoryStruct.comp (Y :=
      X.presheaf.stalk
        (Sigma.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
          (Sigma.mk (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
            x
            (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f hf))))
      (X.presheaf.germ U
        (Sigma.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
          (Sigma.mk (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
            x
            (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f hf)))
        hxU)
      (↑(Sigma.snd (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
            (Sigma.mk (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
              x
              (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f
                hf))) :
        X.presheaf.stalk ⟨x, ⟨f, hf⟩⟩.fst ⟶ R))
    (CategoryStruct.comp (Y :=
      X.presheaf.stalk
        (Sigma.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
          (Sigma.mk (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
            x
            (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f hf))))
      (X.presheaf.germ U
        (Sigma.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
          (Sigma.mk (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
            x
            (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f hf)))
        hxU)
      (CategoryStruct.comp (Y :=
        X.presheaf.stalk
          (Sigma.fst (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
            ((fun (f : Spec R ⟶ X) ↦
                (Sigma.mk (β := fun (x : ↥X) ↦
                    { f : X.presheaf.stalk x ⟶ R //
                      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
                    (f (closedPoint (↑R : Type u)))
                    (Subtype.mk (p := fun (f_2 : X.presheaf.stalk (f (closedPoint (↑R : Type u))) ⟶ R) ↦
                      IsLocalHom (R := (↑(X.presheaf.stalk (f (closedPoint (↑R : Type u)))) : Type u)) (S :=
                        (↑R : Type u)) (CommRingCat.Hom.hom f_2))
                      (Scheme.stalkClosedPointTo f) sorry) :
                  (x : ↥X) ×
                    { f : X.presheaf.stalk x ⟶ R //
                      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                        (CommRingCat.Hom.hom f) }))
              ((fun
                    (xf :
                      (x : ↥X) ×
                        { f : X.presheaf.stalk x ⟶ R //
                          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                            (CommRingCat.Hom.hom f) }) ↦
                  Spec.map
                      (↑(xf.snd (β := fun (x : ↥X) ↦
                            { f : X.presheaf.stalk x ⟶ R //
                              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                (CommRingCat.Hom.hom f) })) :
                        X.presheaf.stalk xf.fst ⟶ R) ≫
                    X.fromSpecStalk
                      (xf.fst (β := fun (x : ↥X) ↦
                        { f : X.presheaf.stalk x ⟶ R //
                          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                            (CommRingCat.Hom.hom f) })))
                (Sigma.mk (β := fun (x : ↥X) ↦
                  { f : X.presheaf.stalk x ⟶ R //
                    IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
                  x
                  (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
                    IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f
                    hf))))))
        (Iso.hom (X.presheaf.stalkCongr sorry))
        (↑(Sigma.snd (β := fun (x : ↥X) ↦
                { f : X.presheaf.stalk x ⟶ R //
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
                ((fun (f : Spec R ⟶ X) ↦
                    (Sigma.mk (β := fun (x : ↥X) ↦
                        { f : X.presheaf.stalk x ⟶ R //
                          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                            (CommRingCat.Hom.hom f) })
                        (f (closedPoint (↑R : Type u)))
                        (Subtype.mk (p := fun (f_2 : X.presheaf.stalk (f (closedPoint (↑R : Type u))) ⟶ R) ↦
                          IsLocalHom (R := (↑(X.presheaf.stalk (f (closedPoint (↑R : Type u)))) : Type u)) (S :=
                            (↑R : Type u)) (CommRingCat.Hom.hom f_2))
                          (Scheme.stalkClosedPointTo f) sorry) :
                      (x : ↥X) ×
                        { f : X.presheaf.stalk x ⟶ R //
                          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                            (CommRingCat.Hom.hom f) }))
                  ((fun
                        (xf :
                          (x : ↥X) ×
                            { f : X.presheaf.stalk x ⟶ R //
                              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                (CommRingCat.Hom.hom f) }) ↦
                      Spec.map
                          (↑(xf.snd (β := fun (x : ↥X) ↦
                                { f : X.presheaf.stalk x ⟶ R //
                                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                    (CommRingCat.Hom.hom f) })) :
                            X.presheaf.stalk xf.fst ⟶ R) ≫
                        X.fromSpecStalk
                          (xf.fst (β := fun (x : ↥X) ↦
                            { f : X.presheaf.stalk x ⟶ R //
                              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                (CommRingCat.Hom.hom f) })))
                    (Sigma.mk (β := fun (x : ↥X) ↦
                      { f : X.presheaf.stalk x ⟶ R //
                        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                          (CommRingCat.Hom.hom f) })
                      x
                      (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
                        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f))
                        f hf)))) :
              { f_2 :
                X.presheaf.stalk
                    (Sigma.fst (β := fun (x : ↥X) ↦
                      { f : X.presheaf.stalk x ⟶ R //
                        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                          (CommRingCat.Hom.hom f) })
                      ((fun (f : Spec R ⟶ X) ↦
                          (Sigma.mk (β := fun (x : ↥X) ↦
                              { f : X.presheaf.stalk x ⟶ R //
                                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                  (CommRingCat.Hom.hom f) })
                              (f (closedPoint (↑R : Type u)))
                              (Subtype.mk (p := fun (f_2 : X.presheaf.stalk (f (closedPoint (↑R : Type u))) ⟶ R) ↦
                                IsLocalHom (R := (↑(X.presheaf.stalk (f (closedPoint (↑R : Type u)))) : Type u)) (S :=
                                  (↑R : Type u)) (CommRingCat.Hom.hom f_2))
                                (Scheme.stalkClosedPointTo f) sorry) :
                            (x : ↥X) ×
                              { f : X.presheaf.stalk x ⟶ R //
                                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                  (CommRingCat.Hom.hom f) }))
                        ((fun
                              (xf :
                                (x : ↥X) ×
                                  { f : X.presheaf.stalk x ⟶ R //
                                    IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                      (CommRingCat.Hom.hom f) }) ↦
                            Spec.map
                                (↑(xf.snd (β := fun (x : ↥X) ↦
                                      { f : X.presheaf.stalk x ⟶ R //
                                        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                          (CommRingCat.Hom.hom f) })) :
                                  X.presheaf.stalk xf.fst ⟶ R) ≫
                              X.fromSpecStalk
                                (xf.fst (β := fun (x : ↥X) ↦
                                  { f : X.presheaf.stalk x ⟶ R //
                                    IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                      (CommRingCat.Hom.hom f) })))
                          (Sigma.mk (β := fun (x : ↥X) ↦
                            { f : X.presheaf.stalk x ⟶ R //
                              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                (CommRingCat.Hom.hom f) })
                            x
                            (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
                              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                (CommRingCat.Hom.hom f))
                              f hf))))) ⟶
                  R //
                IsLocalHom (R :=
                  (↑(X.presheaf.stalk
                        (Sigma.fst (β := fun (x : ↥X) ↦
                          { f : X.presheaf.stalk x ⟶ R //
                            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                              (CommRingCat.Hom.hom f) })
                          ((fun (f : Spec R ⟶ X) ↦
                              (Sigma.mk (β := fun (x : ↥X) ↦
                                  { f : X.presheaf.stalk x ⟶ R //
                                    IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                      (CommRingCat.Hom.hom f) })
                                  (f (closedPoint (↑R : Type u)))
                                  (Subtype.mk (p := fun (f_3 : X.presheaf.stalk (f (closedPoint (↑R : Type u))) ⟶ R) ↦
                                    IsLocalHom (R := (↑(X.presheaf.stalk (f (closedPoint (↑R : Type u)))) : Type u))
                                      (S := (↑R : Type u)) (CommRingCat.Hom.hom f_3))
                                    (Scheme.stalkClosedPointTo f) sorry) :
                                (x : ↥X) ×
                                  { f : X.presheaf.stalk x ⟶ R //
                                    IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                      (CommRingCat.Hom.hom f) }))
                            ((fun
                                  (xf :
                                    (x : ↥X) ×
                                      { f : X.presheaf.stalk x ⟶ R //
                                        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                          (CommRingCat.Hom.hom f) }) ↦
                                Spec.map
                                    (↑(xf.snd (β := fun (x : ↥X) ↦
                                          { f : X.presheaf.stalk x ⟶ R //
                                            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                              (CommRingCat.Hom.hom f) })) :
                                      X.presheaf.stalk xf.fst ⟶ R) ≫
                                  X.fromSpecStalk
                                    (xf.fst (β := fun (x : ↥X) ↦
                                      { f : X.presheaf.stalk x ⟶ R //
                                        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                          (CommRingCat.Hom.hom f) })))
                              (Sigma.mk (β := fun (x : ↥X) ↦
                                { f : X.presheaf.stalk x ⟶ R //
                                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                    (CommRingCat.Hom.hom f) })
                                x
                                (Subtype.mk (p := fun (f : X.presheaf.stalk x ⟶ R) ↦
                                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u))
                                    (CommRingCat.Hom.hom f))
                                  f hf)))))) :
                    Type u))
                  (S := (↑R : Type u)) (CommRingCat.Hom.hom f_2) }) :
          X.presheaf.stalk
              ((fun (f : Spec R ⟶ X) ↦ ⟨f (closedPoint (↑R : Type u)), ⟨Scheme.stalkClosedPointTo f, sorry⟩⟩)
                  ((fun (xf : (x : ↥X) × { f : X.presheaf.stalk x ⟶ R // IsLocalHom (CommRingCat.Hom.hom f) }) ↦
                      Spec.map (↑xf.snd : X.presheaf.stalk xf.fst ⟶ R) ≫ X.fromSpecStalk xf.fst)
                    ⟨x, ⟨f, hf⟩⟩)).fst ⟶
            R)))
Tactic: refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_