-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u)
x : PrimeSpectrum (Localization M)
simp :
  Function.Bijective (α :=
    Localization.AtPrime
      (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal))
    (β :=
    (↑(TopCat.Presheaf.stalk
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (Localization M)) : Type u)))
            (structureSheaf (Localization M)))
          x) :
      Type u))
    (Function.comp (β := Localization.AtPrime x.asIdeal)
      (⇑(↑(stalkIso (Localization M) x) :
            Localization.AtPrime x.asIdeal →+*
              (↑((structurePresheafInCommRingCat (Localization M)).stalk x) : Type u)) :
        (a : Localization.AtPrime x.asIdeal) →
          (↑(TopCat.Presheaf.stalk (structureSheaf (Localization M)).obj x) : Type u))
      (⇑(Localization.localRingHom
            (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)
            x.asIdeal (algebraMap (↑R : Type u) (Localization M)) ⋯) :
        (a : Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)) →
          Localization.AtPrime x.asIdeal))
⊢ Function.Bijective (α :=
    (↑(TopCat.Presheaf.stalk (X := Spec.topObj (CommRingCat.of (↑R : Type u)))
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheaf (↑R : Type u)))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (X := Spec.topObj (CommRingCat.of (Localization M))) (Y := Spec.topObj (CommRingCat.of (↑R : Type u)))
                (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))) :
              (a : PrimeSpectrum (Localization M)) → PrimeSpectrum (↑R : Type u))
            x)) :
      Type u))
    (β :=
    (↑(TopCat.Presheaf.stalk
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (Localization M)) : Type u)))
            (structureSheaf (Localization M)))
          x) :
      Type u))
    (Function.comp (β :=
      Localization.AtPrime
        (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal))
      (Function.comp (β := Localization.AtPrime x.asIdeal)
        (⇑(↑(stalkIso (Localization M) x) :
              Localization.AtPrime x.asIdeal →+*
                (↑((structurePresheafInCommRingCat (Localization M)).stalk x) : Type u)) :
          (a : Localization.AtPrime x.asIdeal) →
            (↑(TopCat.Presheaf.stalk (structureSheaf (Localization M)).obj x) : Type u))
        (⇑(Localization.localRingHom
              (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M))
                x.asIdeal)
              x.asIdeal (algebraMap (↑R : Type u) (Localization M)) ⋯) :
          (a : Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)) →
            Localization.AtPrime x.asIdeal))
      (⇑(AlgEquiv.symm (stalkIso (↑R : Type u) (PrimeSpectrum.comap (algebraMap (↑R : Type u) (Localization M)) x))) :
        (a :
            (↑(TopCat.Presheaf.stalk (structureSheaf (↑R : Type u)).obj
                  ((ConcreteCategory.hom (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))) :
                      (a : PrimeSpectrum (Localization M)) → PrimeSpectrum (↑R : Type u))
                    x)) :
              Type u)) →
          Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)))

Tactic:
simp only [EquivLike.bijective_comp]

Premises used: EquivLike.bijective_comp