-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u)
x : PrimeSpectrum (Localization M)
⊢ 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)))
have 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)) sorry) :
      (a : Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)) →
        Localization.AtPrime x.asIdeal))
Tactic: simp only [EquivLike.bijective_comp]