-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : (↑R : Type u)),
    let U : TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u)) := PrimeSpectrum.basicOpen r;
    Eq (α := CommRingCat.of (↑R : Type u) ⟶ X.presheaf.obj ((TopologicalSpace.Opens.map β.hom.base).op.obj (op U)))
      ((CommRingCat.ofHom
            (algebraMap (↑R : Type u)
              (Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                  (structureSheafInType (↑R : Type u) (↑R : Type u)))
                (op U))) ≫
          α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯))
      (CommRingCat.ofHom
          (algebraMap (↑R : Type u)
            (Functor.obj
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (structureSheafInType (↑R : Type u) (↑R : Type u)))
              (op U))) ≫
        β.hom.c.app (op U))
r : (↑R : Type u)
h₁ :
  Eq (α :=
    CommRingCat.of (↑R : Type u) ⟶
      (Functor.obj (TopCat.Sheaf.pushforward CommRingCat β.hom.base) (SheafedSpace.sheaf X)).obj (P :=
            Presheaf.IsSheaf
              (Opens.grothendieckTopology (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u))).obj
        (op (PrimeSpectrum.basicOpen r)))
    (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                  (structureSheaf (↑R : Type u)))
                (op (PrimeSpectrum.basicOpen r))) :
            Type u)) ≫
      (α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen r)))
    (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                  (structureSheaf (↑R : Type u)))
                (op (PrimeSpectrum.basicOpen r))) :
            Type u)) ≫
      β.hom.c.app (op (PrimeSpectrum.basicOpen r)))
⊢ Eq (α :=
    (sheafedSpaceObj R).presheaf.obj (op (PrimeSpectrum.basicOpen r)) ⟶
      (Functor.obj (TopCat.Sheaf.pushforward CommRingCat β.hom.base) (SheafedSpace.sheaf X)).obj (P :=
            Presheaf.IsSheaf
              (Opens.grothendieckTopology (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u))).obj
        (op (PrimeSpectrum.basicOpen r)))
    ((α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen r)))
    (β.hom.c.app (op (PrimeSpectrum.basicOpen r)))

Tactic:
apply (StructureSheaf.to_basicOpen_epi R r).1

Premises used: CategoryTheory.Epi.left_cancellation