-- Module: Mathlib.AlgebraicGeometry.Stalk
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)
⊢ 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) ⋯) :
            (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:
simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Function.comp_apply, Spec_closedPoint,
        Scheme.fromSpecStalk_closedPoint]

Premises used: AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, AlgebraicGeometry.Spec_closedPoint, Function.comp_apply, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp