case h
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ RingHom.comp (localizationToStalk R y ≫ stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h)
      (algebraMap R (Localization.AtPrime y.asIdeal)) =
    RingHom.comp (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x)
      (algebraMap R (Localization.AtPrime y.asIdeal))
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ localizationToStalk R y ≫ stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h =
    CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x
apply IsLocalization.ringHom_ext (S := Localization.AtPrime y.asIdeal) y.asIdeal.primeCompl
case h
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ RingHom.comp (stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h)
      (RingHom.comp (localizationToStalk R y) (algebraMap R (Localization.AtPrime y.asIdeal))) =
    RingHom.comp (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x)
      (algebraMap R (Localization.AtPrime y.asIdeal))
case h
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ RingHom.comp (localizationToStalk R y ≫ stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h)
      (algebraMap R (Localization.AtPrime y.asIdeal)) =
    RingHom.comp (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x)
      (algebraMap R (Localization.AtPrime y.asIdeal))
erw [RingHom.comp_assoc]
case h
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ RingHom.comp (stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h)
      (RingHom.comp (localizationToStalk R y) (algebraMap R (Localization.AtPrime y.asIdeal))) =
    RingHom.comp (localizationToStalk R x)
      (RingHom.comp (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h))
        (algebraMap R (Localization.AtPrime y.asIdeal)))
case h
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ RingHom.comp (stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h)
      (RingHom.comp (localizationToStalk R y) (algebraMap R (Localization.AtPrime y.asIdeal))) =
    RingHom.comp (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x)
      (algebraMap R (Localization.AtPrime y.asIdeal))
conv_rhs => erw [RingHom.comp_assoc]
case h
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ RingHom.comp (stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h)
      (RingHom.comp
        (IsLocalization.lift (_ : ∀ (f : { x // x ∈ Ideal.primeCompl y.asIdeal }), IsUnit (↑(toStalk R y) ↑f)))
        (algebraMap R (Localization.AtPrime y.asIdeal))) =
    RingHom.comp
      (IsLocalization.lift (_ : ∀ (f : { x_1 // x_1 ∈ Ideal.primeCompl x.asIdeal }), IsUnit (↑(toStalk R x) ↑f)))
      (RingHom.comp
        (IsLocalization.lift
          (_ :
            ∀ (y_1 : { x // x ∈ Ideal.primeCompl y.asIdeal }),
              IsUnit (↑(algebraMap R (Localization.AtPrime x.asIdeal)) ↑y_1)))
        (algebraMap R (Localization.AtPrime y.asIdeal)))
case h
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ RingHom.comp (stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h)
      (RingHom.comp (localizationToStalk R y) (algebraMap R (Localization.AtPrime y.asIdeal))) =
    RingHom.comp (localizationToStalk R x)
      (RingHom.comp (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h))
        (algebraMap R (Localization.AtPrime y.asIdeal)))
dsimp [CommRingCat.ofHom, localizationToStalk, PrimeSpectrum.localizationMapOfSpecializes]
case h
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ RingHom.comp (stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h) (toStalk R y) = toStalk R x
case h
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ RingHom.comp (stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h)
      (RingHom.comp
        (IsLocalization.lift (_ : ∀ (f : { x // x ∈ Ideal.primeCompl y.asIdeal }), IsUnit (↑(toStalk R y) ↑f)))
        (algebraMap R (Localization.AtPrime y.asIdeal))) =
    RingHom.comp
      (IsLocalization.lift (_ : ∀ (f : { x_1 // x_1 ∈ Ideal.primeCompl x.asIdeal }), IsUnit (↑(toStalk R x) ↑f)))
      (RingHom.comp
        (IsLocalization.lift
          (_ :
            ∀ (y_1 : { x // x ∈ Ideal.primeCompl y.asIdeal }),
              IsUnit (↑(algebraMap R (Localization.AtPrime x.asIdeal)) ↑y_1)))
        (algebraMap R (Localization.AtPrime y.asIdeal)))
rw [IsLocalization.lift_comp, IsLocalization.lift_comp, IsLocalization.lift_comp]
no goals
case h
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ RingHom.comp (stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h) (toStalk R y) = toStalk R x
exact toStalk_stalkSpecializes h