awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
x : (↑R : Type u)
⊢ Eq (α := Localization.AtPrime p.asIdeal)
    ((CommRingCat.Hom.hom
            (((stalkIso (↑R : Type u)
                          (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).toRingEquiv.toCommRingCatIso.symm.inv ≫
                PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p) ≫
              (stalkIso (↑S : Type u) p).toRingEquiv.toCommRingCatIso.symm.hom) :
          (a : Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal) →
            Localization.AtPrime p.asIdeal)
        ((algebraMap (↑R : Type u) (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal) :
            (a : (↑R : Type u)) → Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal)
          x) :
      Localization.AtPrime p.asIdeal)
    ((algebraMap (↑S : Type u) (Localization.AtPrime p.asIdeal) : (a : (↑S : Type u)) → Localization.AtPrime p.asIdeal)
        ((CommRingCat.Hom.hom f : (a : (↑R : Type u)) → (↑S : Type u)) x) :
      Localization.AtPrime p.asIdeal)
have dsimp : Eq (α := Localization.AtPrime p.asIdeal)
  (((stalkIso (↑S : Type u) p).toRingEquiv.symm :
        (a : (↑((structurePresheafInCommRingCat (↑S : Type u)).stalk p) : Type u)) → Localization.AtPrime p.asIdeal)
      ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p) :
          (a :
              (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
                Type u)) →
            (↑((structurePresheafInCommRingCat (↑S : Type u)).stalk p) : Type u))
        ((stalkIso (↑R : Type u) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) :
              (a : Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal)) →
                (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk
                      (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
                  Type u))
            ((algebraMap (↑R : Type u) (Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal)) :
                  (a : (↑R : Type u)) → Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal))
                x :
              Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal)) :
          (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u))
                (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
            Type u))) :
    Localization.AtPrime p.asIdeal)
  ((algebraMap (↑S : Type u) (Localization.AtPrime p.asIdeal) : (a : (↑S : Type u)) → Localization.AtPrime p.asIdeal)
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u)) → (↑S : Type u)) x) :
    Localization.AtPrime p.asIdeal)
Tactic: dsimp [-RingEquiv.symm_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
p : (↑(↑(locallyRingedSpaceObj S).toPresheafedSpace : TopCat) : Type u)
a :
  (↑((locallyRingedSpaceObj R).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (sheafedSpaceMap f).hom.base :
            (a : (↑(↑(locallyRingedSpaceObj S).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(locallyRingedSpaceObj R).toPresheafedSpace : TopCat) : Type u))
          p)) :
    Type u)
ha :
  IsUnit (M := (↑((locallyRingedSpaceObj S).presheaf.stalk p) : Type u))
    ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f).hom p) :
          (a :
              (↑((locallyRingedSpaceObj R).presheaf.stalk
                    ((ConcreteCategory.hom (sheafedSpaceMap f).hom.base :
                        (a : (↑(↑(locallyRingedSpaceObj S).toPresheafedSpace : TopCat) : Type u)) →
                          (↑(↑(locallyRingedSpaceObj R).toPresheafedSpace : TopCat) : Type u))
                      p)) :
                Type u)) →
            (↑((locallyRingedSpaceObj S).presheaf.stalk p) : Type u))
        a :
      (↑((locallyRingedSpaceObj S).presheaf.stalk p) : Type u))
⊢ IsUnit a
have ha₁ : IsUnit (M := (↑((locallyRingedSpaceObj S).presheaf.stalk p) : Type u))
  ((CommRingCat.Hom.hom
          (CommRingCat.ofHom
              (stalkIso (↑R : Type u) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).symm.toRingEquiv.toRingHom ≫
            CommRingCat.ofHom
                (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
                  (CommRingCat.Hom.hom f) sorry) ≫
              CommRingCat.ofHom (stalkIso (↑S : Type u) p).toRingEquiv.toRingHom) :
        (a :
            (↑((locallyRingedSpaceObj R).presheaf.stalk
                  ((ConcreteCategory.hom (sheafedSpaceMap f).hom.base :
                      (a : (↑(↑(locallyRingedSpaceObj S).toPresheafedSpace : TopCat) : Type u)) →
                        (↑(↑(locallyRingedSpaceObj R).toPresheafedSpace : TopCat) : Type u))
                    p)) :
              Type u)) →
          (↑((locallyRingedSpaceObj S).presheaf.stalk p) : Type u))
      a :
    (↑((locallyRingedSpaceObj S).presheaf.stalk p) : Type u))
Tactic: rw [← localRingHom_comp_stalkIso] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
p : (↑(↑(locallyRingedSpaceObj S).toPresheafedSpace : TopCat) : Type u)
a :
  (↑((locallyRingedSpaceObj R).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (sheafedSpaceMap f).hom.base :
            (a : (↑(↑(locallyRingedSpaceObj S).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(locallyRingedSpaceObj R).toPresheafedSpace : TopCat) : Type u))
          p)) :
    Type u)
ha :
  IsUnit (M :=
    (↑(TopCat.Presheaf.stalk
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
            (structureSheaf (↑S : Type u)))
          p) :
      Type u))
    (((↑(stalkIso (↑S : Type u) p) :
            Localization.AtPrime p.asIdeal →+* (↑((structurePresheafInCommRingCat (↑S : Type u)).stalk p) : Type u)) :
          (a : Localization.AtPrime p.asIdeal) →
            (↑(TopCat.Presheaf.stalk (structureSheaf (↑S : Type u)).obj p) : Type u))
        ((Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f)
                ⋯ :
              (a : Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal)) →
                Localization.AtPrime p.asIdeal)
            (((stalkIso (↑R : Type u) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).symm :
                (a :
                    (↑(TopCat.Presheaf.stalk (structureSheaf (↑R : Type u)).obj
                          ((ConcreteCategory.hom (topMap f) :
                              (a : PrimeSpectrum (↑S : Type u)) → PrimeSpectrum (↑R : Type u))
                            p)) :
                      Type u)) →
                  Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal))
              a) :
          Localization.AtPrime p.asIdeal) :
      (↑(TopCat.Presheaf.stalk
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
              (structureSheaf (↑S : Type u)))
            p) :
        Type u))
⊢ IsUnit a
have this : IsLocalHom (R := Localization.AtPrime p.asIdeal) (S :=
  (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u)) (stalkIso (↑S : Type u) p)
Tactic: have : IsLocalHom (stalkIso S p) := isLocalHom_equiv _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
p : (↑(↑(locallyRingedSpaceObj S).toPresheafedSpace : TopCat) : Type u)
a :
  (↑((locallyRingedSpaceObj R).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (sheafedSpaceMap f).hom.base :
            (a : (↑(↑(locallyRingedSpaceObj S).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(locallyRingedSpaceObj R).toPresheafedSpace : TopCat) : Type u))
          p)) :
    Type u)
ha :
  IsUnit (M :=
    (↑(TopCat.Presheaf.stalk
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
            (structureSheaf (↑S : Type u)))
          p) :
      Type u))
    (((↑(stalkIso (↑S : Type u) p) :
            Localization.AtPrime p.asIdeal →+* (↑((structurePresheafInCommRingCat (↑S : Type u)).stalk p) : Type u)) :
          (a : Localization.AtPrime p.asIdeal) →
            (↑(TopCat.Presheaf.stalk (structureSheaf (↑S : Type u)).obj p) : Type u))
        ((Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal) p.asIdeal (CommRingCat.Hom.hom f)
                ⋯ :
              (a : Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal)) →
                Localization.AtPrime p.asIdeal)
            (((stalkIso (↑R : Type u) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).symm :
                (a :
                    (↑(TopCat.Presheaf.stalk (structureSheaf (↑R : Type u)).obj
                          ((ConcreteCategory.hom (topMap f) :
                              (a : PrimeSpectrum (↑S : Type u)) → PrimeSpectrum (↑R : Type u))
                            p)) :
                      Type u)) →
                  Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal))
              a) :
          Localization.AtPrime p.asIdeal) :
      (↑(TopCat.Presheaf.stalk
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
              (structureSheaf (↑S : Type u)))
            p) :
        Type u))
this :
  IsLocalHom (R := Localization.AtPrime p.asIdeal) (S :=
    (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u)) (stalkIso (↑S : Type u) p)
⊢ IsUnit a
have this₁ : IsLocalHom (R :=
  (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u))
        (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
    Type u))
  (S := Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal)
  (stalkIso (↑R : Type u) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).symm
Tactic: have : IsLocalHom (stalkIso R (p.comap f.hom)).symm := isLocalHom_equiv _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R : CommRingCat
⊢ (locallyRingedSpaceMap (𝟙 R)).toHom = LocallyRingedSpace.Hom.toHom (𝟙 (locallyRingedSpaceObj R))
have rw : InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R)) = LocallyRingedSpace.Hom.toHom (𝟙 (locallyRingedSpaceObj R))
Tactic: rw [Spec.locallyRingedSpaceMap_toHom, Spec.sheafedSpaceMap_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (locallyRingedSpaceMap (f ≫ g)).toHom = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).toHom
have rw : (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).toHom
Tactic: rw [Spec.locallyRingedSpaceMap_toHom, Spec.sheafedSpaceMap_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R : CommRingCatᵒᵖ
⊢ locallyRingedSpaceMap (𝟙 (unop R)) = 𝟙 (locallyRingedSpaceObj (unop R))
have rw : 𝟙 (locallyRingedSpaceObj (unop R)) = 𝟙 (locallyRingedSpaceObj (unop R))
Tactic: rw [Spec.locallyRingedSpaceMap_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
X Y Z : CommRingCatᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ locallyRingedSpaceMap (g.unop ≫ f.unop) = locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop
have rw : locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop =
  locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop
Tactic: rw [Spec.locallyRingedSpaceMap_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op
have hf : ∀ (x : (↑R : Type u)),
  Eq (α := (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
    ((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
          (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
        x :
      (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
    ((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
          (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
        x :
      (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
x : (↑R : Type u)
⊢ Eq (α := (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
    ((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
          (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
        x :
      (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
    ((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
          (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
        x :
      (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
have hf : ∀ (x' : ↥(unop (op ⊤))),
  Eq.{u + 1} (α :=
    Localizations (↑(unop (op S)) : Type u) (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
    ((↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')
    ((↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')
Tactic: refine Subtype.ext <| funext fun x' => ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
x : (↑R : Type u)
x' : ↥(unop (op ⊤))
⊢ Eq.{u + 1} (α :=
    Localizations (↑(unop (op S)) : Type u) (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
    ((↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')
    ((↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')
have hf : Eq.{u + 1} (α :=
  Localizations (↑(unop (op S)) : Type u) (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
  ((↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
            (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
          x) :
      (x : ↥(unop (op ⊤))) →
        Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
    x')
  ((↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
            (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
          x) :
      (x : ↥(unop (op ⊤))) →
        Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
    x')
Tactic: symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
x : (↑R : Type u)
x' : ↥(unop (op ⊤))
⊢ Eq.{u + 1} (α :=
    Localizations (↑(unop (op S)) : Type u) (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
    ((↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')
    ((↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')
have hf : Eq (α := Localizations (↑(unop (op S)) : Type u) (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
  ((Localization.localRingHom
        (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop)
            (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u))).asIdeal
        (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)).asIdeal (CommRingCat.Hom.hom f.op.unop) sorry :
      (a :
          Localization.AtPrime
            (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop)
                (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u))).asIdeal) →
        Localization.AtPrime (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)).asIdeal)
    ((↑(((toSpecΓ R).hom' : (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op R)))) : Type u)) x) :
        (x : ↥(unop (op (unop (op ⊤))))) →
          Localizations (↑(unop (op R)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op R)) : Type u)) : Type u)))
      (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top (↑(unop (op R)) : Type u)) : Type u)) ↦
        Membership.mem (γ := TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑(unop (op R)) : Type u)) : Type u))
          (unop (op (unop (op ⊤)))) x)
        (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop)
          (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
        sorry)))
  ((↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
            (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
          x) :
      (x : ↥(unop (op ⊤))) →
        Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
    x')
Tactic: erw [comap_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u)
x : PrimeSpectrum (Localization M)
⊢ IsIso (X :=
    (Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))).presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (Localization M)))) : TopCat)) (Y :=
            (↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))) : TopCat))
            (PresheafedSpace.Hom.base
              (Spec.toPresheafedSpace.map
                (Quiver.Hom.op (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))))) :
          (a : (↑(↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (Localization M)))) : TopCat) : Type u)) →
            (↑(↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))) : TopCat) : Type u))
        x))
    (PresheafedSpace.Hom.stalkMap
      (Spec.toPresheafedSpace.map (Quiver.Hom.op (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M))))) x)
have dsimp : IsIso.{u, u + 1} (X :=
  (Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))).presheaf.stalk
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
          (↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (Localization M)))) : TopCat)) (Y :=
          (↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))) : TopCat))
          (PresheafedSpace.Hom.base
            (InducedCategory.Hom.hom
              (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))))) :
        (a : (↑(↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (Localization M)))) : TopCat) : Type u)) →
          (↑(↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))) : TopCat) : Type u))
      x))
  (PresheafedSpace.Hom.stalkMap
    (InducedCategory.Hom.hom (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M))))) x)
Tactic: dsimp only [Spec.toPresheafedSpace_map, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u)
x : PrimeSpectrum (Localization M)
⊢ IsIso.{u, u + 1} (X :=
    (Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))).presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (Localization M)))) : TopCat)) (Y :=
            (↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))) : TopCat))
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom
                (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))))) :
          (a : (↑(↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (Localization M)))) : TopCat) : Type u)) →
            (↑(↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))) : TopCat) : Type u))
        x))
    (PresheafedSpace.Hom.stalkMap
      (InducedCategory.Hom.hom (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))))
      x)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [← localRingHom_comp_stalkIso, ConcreteCategory.isIso_iff_bijective]