awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
f :
  Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
        (structureSheaf (↑(Γ.obj (op X)) : Type u)))
      (op (basicOpen r)) ⟶
    X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst :
  IsLocalization.Away r
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
            (structureSheaf (↑(Γ.obj (op X)) : Type u)))
          (op (basicOpen r))) :
      Type u)
h :
  Eq (α :=
    (↑(CommRingCat.of (↑(Γ.obj (op X)) : Type u)) : Type u) →+*
      (↑(X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))) : Type u))
    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) (X := CommRingCat.of (↑(Γ.obj (op X)) : Type u))
      (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)) : Type u)
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheafInType (↑(Γ.obj (op X)) : Type u) (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r)))) ≫
        f))
    (@RingHom.comp _
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
              (structureSheaf (↑(Γ.obj (op X)) : Type u)))
            (op (basicOpen r))) :
        Type u)
      _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.lift r ⋯)
      (algebraMap (↑(Γ.obj (op X)) : Type u)
        (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf
                  (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)))
                (structureSheaf (↑(Γ.obj (op X)) : Type u)))
              (op (basicOpen r))) :
          Type u)))
⊢ f = X.toΓSpecCApp r
have mp : CommRingCat.Hom.hom f = CommRingCat.Hom.hom (X.toΓSpecCApp r)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r_1 : (↑(Γ.obj (op X)) : Type u)
r s : (InducedCategory (C := (↑(Γ.obj (op X)) : Type u)) (Opens (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))) basicOpen)ᵒᵖ
f : r ⟶ s
e_1 :
  (CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        s) =
    (CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen (unop s))))
⊢ Eq (α :=
    CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        s)
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        r)
      (X.toToΓSpecMapBasicOpen (unop r))
      (CategoryTheory.Functor.map
        (Functor.op (inducedFunctor basicOpen) ⋙
          (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
        f))
    (X.toToΓSpecMapBasicOpen (unop s))
have h : Eq (α :=
  CommRingCat.of (↑(Γ.obj (op X)) : Type u) ⟶
    Functor.obj
      (Functor.op (inducedFunctor basicOpen) ⋙
        (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
          Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
      s)
  (X.toToΓSpecMapBasicOpen (unop s))
  (CategoryStruct.comp (Y :=
    Functor.obj
      (Functor.op (inducedFunctor basicOpen) ⋙
        (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
          Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
      r)
    (X.toToΓSpecMapBasicOpen (unop r))
    (CategoryTheory.Functor.map
      (Functor.op (inducedFunctor basicOpen) ⋙
        (Functor.obj (TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase) X.𝒪).obj (P :=
          Presheaf.IsSheaf (Opens.grothendieckTopology (↑(Spec.topObj (Γ.obj (op X))) : Type u))))
      f))
Tactic: symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
⊢ Membership.mem (α := (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)) (γ :=
    Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)) (basicOpen 1)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpecSheafedSpace.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
        x :
      (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
have rw : Membership.mem (α := (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)) (γ :=
  Opens (↑(PrimeSpectrum.Top (↑(Γ.obj (op X)) : Type u)) : Type u)) ⊤
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          X.toΓSpecSheafedSpace.hom.base :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
      x :
    (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
Tactic: rw [basicOpen_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
⊢ toStalk (↑(unop (op (Γ.obj (op X)))) : Type u)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpecSheafedSpace.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
          x) ≫
      PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x =
    X.presheaf.Γgerm x
have rw : Eq (α := CommRingCat.of (↑(unop (op (Γ.obj (op X)))) : Type u) ⟶ X.presheaf.stalk x)
  (CategoryStruct.comp (Y :=
      (Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).obj (op (basicOpen 1)))
      (X.toToΓSpecMapBasicOpen 1)
      ((Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).germ (basicOpen 1)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpecSheafedSpace.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
          x)
        sorry) ≫
    stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x)
  ((Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).germ ⊤
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpecSheafedSpace.hom.base :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
        x)
      True.intro ≫
    stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x)
Tactic: rw [PresheafedSpace.Hom.stalkMap,
    ← algebraMap_germ (basicOpen (1 : Γ.obj (op X))) _ (by rw [basicOpen_one]; trivial),
    ← Category.assoc, Category.assoc (CommRingCat.ofHom _), stalkFunctor_map_germ, ← Category.assoc,
    X.toΓSpecSheafedSpace_app_eq, X.toΓSpecCApp_spec, Γgerm,
    ← dsimp% stalkPushforward_germ _ _ X.presheaf ⊤]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
rw :
  Eq (α := CommRingCat.of (↑(unop (op (Γ.obj (op X)))) : Type u) ⟶ X.presheaf.stalk x)
    (CategoryStruct.comp (Y :=
        (Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).obj (op (basicOpen 1)))
        (X.toToΓSpecMapBasicOpen 1)
        ((Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                X.toΓSpecSheafedSpace.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
            x)
          ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x)
    ((Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).germ ⊤
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpecSheafedSpace.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
          x)
        True.intro ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x)
⊢ toStalk (↑(unop (op (Γ.obj (op X)))) : Type u)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpecSheafedSpace.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
          x) ≫
      PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x =
    X.presheaf.Γgerm x
have rw₁ : TopCat
Tactic: rw [PresheafedSpace.Hom.stalkMap,
    ← algebraMap_germ (basicOpen (1 : Γ.obj (op X))) _ (by rw [basicOpen_one]; trivial),
    ← Category.assoc, Category.assoc (CommRingCat.ofHom _), stalkFunctor_map_germ, ← Category.assoc,
    X.toΓSpecSheafedSpace_app_eq, X.toΓSpecCApp_spec, Γgerm,
    ← dsimp% stalkPushforward_germ _ _ X.presheaf ⊤]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
rw :
  Eq (α := CommRingCat.of (↑(unop (op (Γ.obj (op X)))) : Type u) ⟶ X.presheaf.stalk x)
    (CategoryStruct.comp (Y :=
        (Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).obj (op (basicOpen 1)))
        (X.toToΓSpecMapBasicOpen 1)
        ((Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                X.toΓSpecSheafedSpace.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
            x)
          ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x)
    ((Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf).germ ⊤
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpecSheafedSpace.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
          x)
        True.intro ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x)
rw₁ : TopCat
⊢ toStalk (↑(unop (op (Γ.obj (op X)))) : Type u)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpecSheafedSpace.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat) : Type u))
          x) ≫
      PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x =
    X.presheaf.Γgerm x
have rw₂ : (↑X.toPresheafedSpace : TopCat) ⟶ (↑(Spec.toSheafedSpace.obj (op (Γ.obj (op X)))).toPresheafedSpace : TopCat)
Tactic: rw [PresheafedSpace.Hom.stalkMap,
    ← algebraMap_germ (basicOpen (1 : Γ.obj (op X))) _ (by rw [basicOpen_one]; trivial),
    ← Category.assoc, Category.assoc (CommRingCat.ofHom _), stalkFunctor_map_germ, ← Category.assoc,
    X.toΓSpecSheafedSpace_app_eq, X.toΓSpecCApp_spec, Γgerm,
    ← dsimp% stalkPushforward_germ _ _ X.presheaf ⊤]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
x : (↑X.toTopCat : Type u)
p : PrimeSpectrum (↑(Γ.obj (op X)) : Type u) := X.toΓSpecFun x
⊢ IsLocalHom (R :=
    (↑((Spec.locallyRingedSpaceObj (Γ.obj (op X))).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                X.toΓSpecSheafedSpace.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑((Spec.locallyRingedSpaceObj (Γ.obj (op X))).presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) X.toΓSpecSheafedSpace.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                  (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x))
have map_nonunit : ∀
  (a :
    (↑((Spec.locallyRingedSpaceObj (Γ.obj (op X))).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                X.toΓSpecSheafedSpace.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u)),
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u))
      ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x) :
            (a :
                (↑((Spec.locallyRingedSpaceObj (Γ.obj (op X))).presheaf.stalk
                      ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base :
                          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                            (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
                        x)) :
                  Type u)) →
              (↑(X.presheaf.stalk x) : Type u))
          a :
        (↑(X.presheaf.stalk x) : Type u)) →
    IsUnit a
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r : (↑(Γ.obj (op X)) : Type u)
x : (↑X.toTopCat : Type u)
p : PrimeSpectrum (↑(Γ.obj (op X)) : Type u) := X.toΓSpecFun x
S : CommRingCat := stalk (TopCat.Sheaf.presheaf (structureSheaf (↑(Γ.obj (op X)) : Type u))) p
t : (↑S : Type u)
ht :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x) :
          (a :
              (↑((Spec.locallyRingedSpaceObj (Γ.obj (op X))).presheaf.stalk
                    ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base :
                        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
                      x)) :
                Type u)) →
            (↑(X.presheaf.stalk x) : Type u))
        t :
      (↑(X.presheaf.stalk x) : Type u))
⊢ IsUnit t
have map_nonunit : ∀ (r : (↑(Γ.obj (op X)) : Type u)) (s : ↥p.asIdeal.primeCompl)
  (he :
    HMul.hMul (β := (↑S : Type u)) t
        ((algebraMap (↑(Γ.obj (op X)) : Type u) (↑S : Type u) : (a : (↑(Γ.obj (op X)) : Type u)) → (↑S : Type u))
            (↑(r, s).2 : (↑(Γ.obj (op X)) : Type u)) :
          (↑S : Type u)) =
      (algebraMap (↑(Γ.obj (op X)) : Type u) (↑S : Type u) : (a : (↑(Γ.obj (op X)) : Type u)) → (↑S : Type u))
        (r, s).1),
  IsUnit t
Tactic: obtain ⟨⟨r, s⟩, he⟩ := IsLocalization.surj p.asIdeal.primeCompl t
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r_1 : (↑(Γ.obj (op X)) : Type u)
x : (↑X.toTopCat : Type u)
p : PrimeSpectrum (↑(Γ.obj (op X)) : Type u) := X.toΓSpecFun x
S : CommRingCat := stalk (TopCat.Sheaf.presheaf (structureSheaf (↑(Γ.obj (op X)) : Type u))) p
t : (↑S : Type u)
ht :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x) :
          (a :
              (↑((Spec.locallyRingedSpaceObj (Γ.obj (op X))).presheaf.stalk
                    ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base :
                        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
                      x)) :
                Type u)) →
            (↑(X.presheaf.stalk x) : Type u))
        t :
      (↑(X.presheaf.stalk x) : Type u))
r : (↑(Γ.obj (op X)) : Type u)
s : ↥p.asIdeal.primeCompl
t' : (↑S : Type u) :=
  (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
      (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
    (↑s : (↑(X.presheaf.obj (op ⊤)) : Type u))
he :
  t * t' =
    (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
        (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
      r
⊢ IsUnit t
have map_nonunit : IsUnit (t * t')
Tactic: apply isUnit_of_mul_isUnit_left (y := t')
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r_1 : (↑(Γ.obj (op X)) : Type u)
x : (↑X.toTopCat : Type u)
p : PrimeSpectrum (↑(Γ.obj (op X)) : Type u) := X.toΓSpecFun x
S : CommRingCat := stalk (TopCat.Sheaf.presheaf (structureSheaf (↑(Γ.obj (op X)) : Type u))) p
t : (↑S : Type u)
ht :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x) :
          (a :
              (↑((Spec.locallyRingedSpaceObj (Γ.obj (op X))).presheaf.stalk
                    ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base :
                        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
                      x)) :
                Type u)) →
            (↑(X.presheaf.stalk x) : Type u))
        t :
      (↑(X.presheaf.stalk x) : Type u))
r : (↑(Γ.obj (op X)) : Type u)
s : ↥p.asIdeal.primeCompl
t' : (↑S : Type u) :=
  (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
      (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
    (↑s : (↑(X.presheaf.obj (op ⊤)) : Type u))
he :
  t * t' =
    (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
        (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
      r
⊢ IsUnit (t * t')
have map_nonunit : IsUnit (M := (↑S : Type u))
  ((algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
        (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
      r :
    (↑S : Type u))
Tactic: rw [he]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.GammaSpecAdjunction (goal)
Goal:
X : LocallyRingedSpace
r_1 : (↑(Γ.obj (op X)) : Type u)
x : (↑X.toTopCat : Type u)
p : PrimeSpectrum (↑(Γ.obj (op X)) : Type u) := X.toΓSpecFun x
S : CommRingCat := stalk (TopCat.Sheaf.presheaf (structureSheaf (↑(Γ.obj (op X)) : Type u))) p
t : (↑S : Type u)
ht :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x) :
          (a :
              (↑((Spec.locallyRingedSpaceObj (Γ.obj (op X))).presheaf.stalk
                    ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base :
                        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
                          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
                      x)) :
                Type u)) →
            (↑(X.presheaf.stalk x) : Type u))
        t :
      (↑(X.presheaf.stalk x) : Type u))
r : (↑(Γ.obj (op X)) : Type u)
s : ↥p.asIdeal.primeCompl
t' : (↑S : Type u) :=
  (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
      (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
    (↑s : (↑(X.presheaf.obj (op ⊤)) : Type u))
he :
  t * t' =
    (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
        (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
      r
⊢ IsUnit (M := (↑S : Type u))
    ((algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
          (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
        r :
      (↑S : Type u))
have map_nonunit : r ∈ p.asIdeal.primeCompl
Tactic: refine IsLocalization.map_units S (⟨r, ?_⟩ : p.asIdeal.primeCompl)