-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem localizationToStalk_stalkSpecializes {R : Type*} [CommRing R] {x y : PrimeSpectrum R}
    (h : x ⤳ y) :
    StructureSheaf.localizationToStalk R y ≫ (structureSheaf R).presheaf.stalkSpecializes h =
      CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫
        StructureSheaf.localizationToStalk R x

Proof state:
case hf.h
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (CommRingCat.Hom.hom (localizationToStalk R y ≫ (structureSheaf R).presheaf.stalkSpecializes h)).comp
      (algebraMap R (Localization.AtPrime y.asIdeal)) =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x)).comp
      (algebraMap R (Localization.AtPrime y.asIdeal))

Tactic:
rw [CommRingCat.hom_comp, RingHom.comp_assoc, CommRingCat.hom_comp, RingHom.comp_assoc]

Result:
case hf.h
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (CommRingCat.Hom.hom ((structureSheaf R).presheaf.stalkSpecializes h)).comp
      ((CommRingCat.Hom.hom (localizationToStalk R y)).comp (algebraMap R (Localization.AtPrime y.asIdeal))) =
    (CommRingCat.Hom.hom (localizationToStalk R x)).comp
      ((CommRingCat.Hom.hom (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h))).comp
        (algebraMap R (Localization.AtPrime y.asIdeal)))

Proof state:
case hf.h
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (CommRingCat.Hom.hom ((structureSheaf R).presheaf.stalkSpecializes h)).comp
      ((IsLocalization.lift ⋯).comp (algebraMap R (Localization.AtPrime y.asIdeal))) =
    (IsLocalization.lift ⋯).comp ((IsLocalization.lift ⋯).comp (algebraMap R (Localization.AtPrime y.asIdeal)))

Tactic:
rw [IsLocalization.lift_comp, IsLocalization.lift_comp, IsLocalization.lift_comp]

Result:
case hf.h
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (CommRingCat.Hom.hom ((structureSheaf R).presheaf.stalkSpecializes h)).comp (ConcreteCategory.hom (toStalk R y)) =
    ConcreteCategory.hom (toStalk R x)

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ localizationToStalk R y ≫ (structureSheaf R).presheaf.stalkSpecializes h =
    CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x

Tactic:
ext : 1

Result:
case hf
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ CommRingCat.Hom.hom (localizationToStalk R y ≫ (structureSheaf R).presheaf.stalkSpecializes h) =
    CommRingCat.Hom.hom (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x)

Proof state:
case hf
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ CommRingCat.Hom.hom (localizationToStalk R y ≫ (structureSheaf R).presheaf.stalkSpecializes h) =
    CommRingCat.Hom.hom (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x)

Tactic:
apply IsLocalization.ringHom_ext (S := Localization.AtPrime y.asIdeal) y.asIdeal.primeCompl

Result:
case hf.h
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (CommRingCat.Hom.hom (localizationToStalk R y ≫ (structureSheaf R).presheaf.stalkSpecializes h)).comp
      (algebraMap R (Localization.AtPrime y.asIdeal)) =
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x)).comp
      (algebraMap R (Localization.AtPrime y.asIdeal))

Proof state:
case hf.h
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (CommRingCat.Hom.hom ((structureSheaf R).presheaf.stalkSpecializes h)).comp
      ((CommRingCat.Hom.hom (localizationToStalk R y)).comp (algebraMap R (Localization.AtPrime y.asIdeal))) =
    (CommRingCat.Hom.hom (localizationToStalk R x)).comp
      ((CommRingCat.Hom.hom (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h))).comp
        (algebraMap R (Localization.AtPrime y.asIdeal)))

Tactic:
dsimp [localizationToStalk, PrimeSpectrum.localizationMapOfSpecializes]

Result:
case hf.h
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (CommRingCat.Hom.hom ((structureSheaf R).presheaf.stalkSpecializes h)).comp
      ((IsLocalization.lift ⋯).comp (algebraMap R (Localization.AtPrime y.asIdeal))) =
    (IsLocalization.lift ⋯).comp ((IsLocalization.lift ⋯).comp (algebraMap R (Localization.AtPrime y.asIdeal)))

Proof state:
case hf.h
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (CommRingCat.Hom.hom ((structureSheaf R).presheaf.stalkSpecializes h)).comp (ConcreteCategory.hom (toStalk R y)) =
    ConcreteCategory.hom (toStalk R x)

Tactic:
exact CommRingCat.hom_ext_iff.mp (toStalk_stalkSpecializes h)

Result:
no goals