-- 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 : ↥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))
    ((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))))
have refine_1 : 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)) =
  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))))
Tactic: refine SpecToEquivOfLocalRing_eq_iff.mpr ⟨?_, ?_⟩