awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
⊢ Eq (α :=
    CommRingCat.of (↑(unop (op (Γ.obj (op X)))) : Type u) ⟶
      Functor.obj
        (stalkFunctor CommRingCat
          ((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))
        (Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf))
    (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)
        ⋯))
    ((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)

Tactic:
(X.toΓSpecBase _* X.presheaf).germ_res le_top.hom _ _

Premises used: PrimeSpectrum.basicOpen, AlgebraicGeometry.Spec.topObj, Set.Mem, Quiver.Hom.op, Set.univ, setOf, AlgebraicGeometry.LocallyRingedSpace.toTopCat, LE.le.hom, TopCat.Presheaf.stalk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.Presheaf.germ_res, Set.preimage, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.PrimeSpectrum.Top, AlgebraicGeometry.LocallyRingedSpace.toΓSpecBase, TopCat.Presheaf.pushforward, TopologicalSpace.Opens.leTop, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
⊢ Eq (α :=
    CommRingCat.of (↑(unop (op (Γ.obj (op X)))) : Type u) ⟶
      Functor.obj
        (stalkFunctor CommRingCat
          ((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))
        (Functor.obj (pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base) X.presheaf))
    (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)
        ⋯))
    ((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)

Tactic:
exact (X.toΓSpecBase _* X.presheaf).germ_res le_top.hom _ _

Premises used: LE.le.hom, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.Presheaf.germ_res, le_top, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.LocallyRingedSpace.toΓSpecBase, TopCat.Presheaf.pushforward, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
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
⊢ 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))

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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))
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
⊢ IsUnit t

Tactic:
obtain ⟨⟨r, s⟩, he⟩ := IsLocalization.surj p.asIdeal.primeCompl t

Premises used: IsLocalization.surj, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
he :
  HMul.hMul (β := (↑S : Type u)) t
      ((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)) :
        (↑S : Type u)) =
    (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
        (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
      r
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))
⊢ t * t' =
    (algebraMap (↑(X.presheaf.obj (op ⊤)) : Type u) (↑S : Type u) :
        (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑S : Type u))
      r

Tactic:
change t * t' = _ at he
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
map_nonunit : IsUnit (t * t')
⊢ IsUnit t

Tactic:
apply isUnit_of_mul_isUnit_left (y := t')

Premises used: isUnit_of_mul_isUnit_left
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
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))
⊢ IsUnit (t * t')

Tactic:
rw [he]
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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))

Tactic:
IsLocalization.map_units S (⟨r, ?_⟩ : p.asIdeal.primeCompl)

Premises used: CommRingCat.carrier, Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
map_nonunit : r ∈ p.asIdeal.primeCompl
⊢ 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:
refine IsLocalization.map_units S (⟨r, ?_⟩ : p.asIdeal.primeCompl)

Premises used: CommRingCat.carrier, Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
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
map_nonunit :
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.Γgerm x) :
          (a : (↑(X.presheaf.obj (op ⊤)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        r :
      (↑(X.presheaf.stalk x) : Type u))
⊢ r ∈ p.asIdeal.primeCompl

Tactic:
apply (notMem_prime_iff_unit_in_stalk _ _ _).mpr

Premises used: Iff.mpr, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
s : Set (↑(X.presheaf.obj (op ⊤)) : Type u)
i : (↑(Γ.obj (op X)) : Type u)
h : i ∈ s
symm :
  Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpec.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (Opens.carrier (basicOpen i))ᶜ =
    (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ
⊢ (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ =
    Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            X.toΓSpec.base) :
        (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
      (Opens.carrier (basicOpen i))ᶜ

Tactic:
symm
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
s : Set (↑(X.presheaf.obj (op ⊤)) : Type u)
i : (↑(Γ.obj (op X)) : Type u)
h : i ∈ s
erw erw₁ :
  (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ =
    (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ
⊢ ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpec.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u)) ⁻¹'
        (↑(basicOpen i) : Set (PrimeSpectrum (↑(Γ.obj (op X)) : Type u))))ᶜ =
    (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ

Tactic:
erw [X.toΓSpec_preimage_basicOpen_eq i]

Premises used: AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq
-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
X : LocallyRingedSpace
s : Set (↑(X.presheaf.obj (op ⊤)) : Type u)
⊢ ∀ i ∈ s,
    (↑(X.toRingedSpace.basicOpen i) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ =
      Set.preimage (β := (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              X.toΓSpec.base) :
          (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.locallyRingedSpaceObj (Γ.obj (op X))).toPresheafedSpace : TopCat) : Type u))
        (Opens.carrier (basicOpen i))ᶜ

Tactic:
have (i : LocallyRingedSpace.Γ.obj (op X)) (_ : i ∈ s) :
      (SetLike.coe (X.toRingedSpace.basicOpen i))ᶜ =
        X.toΓSpec.base ⁻¹' ((PrimeSpectrum.basicOpen i).carrier)ᶜ := by
    symm
    rw [Set.preimage_compl, Opens.carrier_eq_coe]
    erw [X.toΓSpec_preimage_basicOpen_eq i]