awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
⊢ Eq (α := CommRingCat.of (↑R : Type u) ⟶ (Spec.sheafedSpaceObj S).presheaf.stalk p)
    (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      CategoryStruct.comp (Y :=
        CommRingCat.of
          (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                  (structureSheaf (↑S : Type u)))
                (op
                  ((TopologicalSpace.Opens.comap
                        { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ :
                          C(PrimeSpectrum (↑S : Type u), PrimeSpectrum (↑R : Type u)) } :
                      (a : TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u))) →
                        TopologicalSpace.Opens (PrimeSpectrum (↑S : Type u)))
                    ⊤))) :
            Type u))
        (CommRingCat.ofHom
          (algebraMap (↑S : Type u)
            (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                    (structureSheaf (↑S : Type u)))
                  (op
                    ((TopologicalSpace.Opens.comap
                          { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ :
                            C(PrimeSpectrum (↑S : Type u), PrimeSpectrum (↑R : Type u)) } :
                        (a : TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u))) →
                          TopologicalSpace.Opens (PrimeSpectrum (↑S : Type u)))
                      ⊤))) :
              Type u)))
        ((Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).hom.base).obj ⊤) p
          trivial))
    (f ≫
      CategoryStruct.comp (Y :=
        CommRingCat.of
          (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
              (structureSheafInType (↑S : Type u) (↑S : Type u)))
            (op ⊤)))
        (CommRingCat.ofHom
          (algebraMap (↑S : Type u)
            (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                (structureSheafInType (↑S : Type u) (↑S : Type u)))
              (op ⊤))))
        (TopCat.Presheaf.germ (structurePresheafInCommRingCat (↑S : Type u)) ⊤ p trivial))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
x : (↑R : Type u)
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)
⊢ 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)

Tactic:
dsimp [-RingEquiv.symm_mk]

Premises used: RingEquiv.symm_mk
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
x : (↑R : Type u)
⊢ Eq (α := (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u))
    ((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))
        ((algebraMap (↑R : Type u)
                (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u))
                      (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
                  Type u) :
              (a : (↑R : Type u)) →
                (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk
                      (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
                  Type u))
            x :
          (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u))
                (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
            Type u)) :
      (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u))
    ((algebraMap (↑S : Type u) (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u) :
          (a : (↑S : Type u)) → (↑((structurePresheafInCommRingCat (↑S : Type u)).stalk p) : Type u))
        ((CommRingCat.Hom.hom f : (a : (↑R : Type u)) → (↑S : Type u)) x : (↑S : Type u)) :
      (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u))

Tactic:
stalkMap_toStalk_apply f p x

Premises used: AlgebraicGeometry.Spec.topObj, AlgebraicGeometry.stalkMap_toStalk_apply, AlgebraicGeometry.PrimeSpectrum.Top, AlgebraicGeometry.structurePresheafInCommRingCat
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
x : (↑R : Type u)
⊢ Eq (α := (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u))
    ((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))
        ((algebraMap (↑R : Type u)
                (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u))
                      (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
                  Type u) :
              (a : (↑R : Type u)) →
                (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk
                      (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
                  Type u))
            x :
          (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u))
                (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
            Type u)) :
      (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u))
    ((algebraMap (↑S : Type u) (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u) :
          (a : (↑S : Type u)) → (↑((structurePresheafInCommRingCat (↑S : Type u)).stalk p) : Type u))
        ((CommRingCat.Hom.hom f : (a : (↑R : Type u)) → (↑S : Type u)) x : (↑S : Type u)) :
      (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u))

Tactic:
exact stalkMap_toStalk_apply f p x

Premises used: AlgebraicGeometry.stalkMap_toStalk_apply
-- Module: Mathlib.AlgebraicGeometry.Spec
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 (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) ⋯) ≫
                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

Premises used: AlgebraicGeometry.localRingHom_comp_stalkIso
-- Module: Mathlib.AlgebraicGeometry.Spec
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))
⊢ 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 _
-- Module: Mathlib.AlgebraicGeometry.Spec
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)
⊢ 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 _
-- Module: Mathlib.AlgebraicGeometry.Spec
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_1 :
  IsLocalHom (R := Localization.AtPrime p.asIdeal) (S :=
    (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u)) (stalkIso (↑S : Type u) p)
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
⊢ IsUnit a

Tactic:
((ha.of_map (stalkIso S p)).of_map _).of_map (stalkIso R (p.comap f.hom)).symm

Premises used: CommRingCat.Hom.hom, CommRingCat.carrier, AlgEquiv.symm, AlgebraicGeometry.Spec.topObj, IsUnit.of_map, AlgebraicGeometry.StructureSheaf.stalkIso, AlgebraicGeometry.structurePresheafInCommRingCat, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.Spec
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_1 :
  IsLocalHom (R := Localization.AtPrime p.asIdeal) (S :=
    (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u)) (stalkIso (↑S : Type u) p)
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
⊢ IsUnit a

Tactic:
exact ((ha.of_map (stalkIso S p)).of_map _).of_map (stalkIso R (p.comap f.hom)).symm

Premises used: CommRingCat.Hom.hom, CommRingCat.carrier, AlgEquiv.symm, IsUnit.of_map, AlgebraicGeometry.StructureSheaf.stalkIso, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
rw : InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R)) = LocallyRingedSpace.Hom.toHom (𝟙 (locallyRingedSpaceObj R))
⊢ (locallyRingedSpaceMap (𝟙 R)).toHom = LocallyRingedSpace.Hom.toHom (𝟙 (locallyRingedSpaceObj R))

Tactic:
rw [Spec.locallyRingedSpaceMap_toHom, Spec.sheafedSpaceMap_id]

Premises used: AlgebraicGeometry.Spec.locallyRingedSpaceMap_toHom, AlgebraicGeometry.Spec.sheafedSpaceMap_id
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
⊢ InducedCategory.Hom.hom (𝟙 (sheafedSpaceObj R)) = LocallyRingedSpace.Hom.toHom (𝟙 (locallyRingedSpaceObj R))

Tactic:
rfl