awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u)
x : PrimeSpectrum (Localization M)
this :
  IsIso (X :=
    CommRingCat.of
      (Localization.AtPrime
        (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)))
    (Y := CommRingCat.of (Localization.AtPrime x.asIdeal))
    (Iso.hom
      (RingEquiv.toCommRingCatIso
        (AlgEquiv.toRingEquiv (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal))))
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Function.Bijective (α :=
        (↑(CommRingCat.of
              (Localization.AtPrime
                (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M))
                  x.asIdeal))) :
          Type u))
        (β := (↑(CommRingCat.of (Localization.AtPrime x.asIdeal)) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X :=
              CommRingCat.of
                (Localization.AtPrime
                  (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M))
                    x.asIdeal)))
              (Y := CommRingCat.of (Localization.AtPrime x.asIdeal))
              (Iso.hom
                (RingEquiv.toCommRingCatIso
                  (AlgEquiv.toRingEquiv
                    (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal))))) :
          (a :
              (↑(CommRingCat.of
                    (Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal))) :
                Type u)) →
            (↑(CommRingCat.of (Localization.AtPrime x.asIdeal)) : Type u))),
    Function.Bijective (α :=
      Localization.AtPrime
        (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal))
      (β := Localization.AtPrime x.asIdeal)
      (⇑(Localization.localRingHom
            (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)
            x.asIdeal (algebraMap (↑R : Type u) (Localization M)) ⋯) :
        (a : Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)) →
          Localization.AtPrime x.asIdeal)
⊢ Function.Bijective (α :=
    Localization.AtPrime
      (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal))
    (β := Localization.AtPrime x.asIdeal)
    (⇑(Localization.localRingHom
          (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)
          x.asIdeal (algebraMap (↑R : Type u) (Localization M)) ⋯) :
      (a : Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)) →
        Localization.AtPrime x.asIdeal)

Tactic:
rwa [ConcreteCategory.isIso_iff_bijective] at this

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u)
x : PrimeSpectrum (Localization M)
IsIso :
  CategoryTheory.IsIso (X :=
    CommRingCat.of
      (Localization.AtPrime
        (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)))
    (Y := CommRingCat.of (Localization.AtPrime x.asIdeal))
    (Iso.hom
      (RingEquiv.toCommRingCatIso
        (AlgEquiv.toRingEquiv (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal))))
⊢ Function.Bijective (α :=
    Localization.AtPrime
      (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal))
    (β := Localization.AtPrime x.asIdeal)
    (⇑(Localization.localRingHom
          (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)
          x.asIdeal (algebraMap (↑R : Type u) (Localization M)) ⋯) :
      (a : Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)) →
        Localization.AtPrime x.asIdeal)

Tactic:
suffices
    IsIso (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M
        x.asIdeal).toRingEquiv.toCommRingCatIso.hom by
    rwa [ConcreteCategory.isIso_iff_bijective] at this
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u)
x : PrimeSpectrum (Localization M)
⊢ IsIso (X :=
    CommRingCat.of
      (Localization.AtPrime
        (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)))
    (Y := CommRingCat.of (Localization.AtPrime x.asIdeal))
    (Iso.hom
      (RingEquiv.toCommRingCatIso
        (AlgEquiv.toRingEquiv (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal))))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑R : Type u)
rw :
  f ≫ toPushforwardStalk f p =
    CategoryStruct.comp (Y :=
      CommRingCat.of
        (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheafInType (↑R : Type u) (↑R : Type u)))
          (op ⊤)))
      (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheafInType (↑R : Type u) (↑R : Type u)))
            (op ⊤))))
      ((Spec.sheafedSpaceMap f).hom.c.app (op ⊤) ≫
        (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (Spec.sheafedSpaceMap f).hom.base)
              (Spec.sheafedSpaceObj S).presheaf).germ
          ⊤ p trivial)
⊢ f ≫ toPushforwardStalk f p =
    toStalk (↑R : Type u) p ≫
      CategoryTheory.Functor.map (TopCat.Presheaf.stalkFunctor CommRingCat p) (Spec.sheafedSpaceMap f).hom.c

Tactic:
rw [StructureSheaf.toStalk, Category.assoc, TopCat.Presheaf.stalkFunctor_map_germ]

Premises used: CategoryTheory.Category.assoc, TopCat.Presheaf.stalkFunctor_map_germ, AlgebraicGeometry.StructureSheaf.toStalk
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑R : Type u)
⊢ f ≫ toPushforwardStalk f p =
    CategoryStruct.comp (Y :=
      CommRingCat.of
        (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheafInType (↑R : Type u) (↑R : Type u)))
          (op ⊤)))
      (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheafInType (↑R : Type u) (↑R : Type u)))
            (op ⊤))))
      ((Spec.sheafedSpaceMap f).hom.c.app (op ⊤) ≫
        (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (Spec.sheafedSpaceMap f).hom.base)
              (Spec.sheafedSpaceObj S).presheaf).germ
          ⊤ p trivial)

Tactic:
Spec_Γ_naturality_assoc f _

Premises used: AlgebraicGeometry.Spec.topObj, Set.Mem, Set.univ, setOf, AlgebraicGeometry.Spec.topMap, TopCat.Presheaf.stalk, Set.preimage, AlgebraicGeometry.Spec_Γ_naturality_assoc, AlgebraicGeometry.PrimeSpectrum.Top, AlgebraicGeometry.structurePresheafInCommRingCat
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑R : Type u)
⊢ f ≫ toPushforwardStalk f p =
    CategoryStruct.comp (Y :=
      CommRingCat.of
        (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheafInType (↑R : Type u) (↑R : Type u)))
          (op ⊤)))
      (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheafInType (↑R : Type u) (↑R : Type u)))
            (op ⊤))))
      ((Spec.sheafedSpaceMap f).hom.c.app (op ⊤) ≫
        (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (Spec.sheafedSpaceMap f).hom.base)
              (Spec.sheafedSpaceObj S).presheaf).germ
          ⊤ p trivial)

Tactic:
exact Spec_Γ_naturality_assoc f _

Premises used: AlgebraicGeometry.Spec_Γ_naturality_assoc
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑R : Type u)
⊢ algebraMap (↑R : Type u)
      (↑((Functor.obj (TopCat.Presheaf.pushforward CommRingCat (Spec.topMap f))
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                  (structureSheaf (↑S : Type u)))).stalk
            p) :
        Type u) =
    CommRingCat.Hom.hom (f ≫ toPushforwardStalk f p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑R : Type u)
inst : Algebra (↑R : Type u) (↑S : Type u)
x : (↑R : Type u)
hx : x ∈ p.asIdeal.primeCompl
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ IsUnit (M :=
    (↑(TopCat.Presheaf.stalk
          (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
            (TopCat.Presheaf.pushforward CommRingCat
              (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
              (structureSheaf (↑S : Type u))))
          p) :
      Type u))
    ((algebraMap (↑R : Type u)
            (↑(TopCat.Presheaf.stalk
                  (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
                    (TopCat.Presheaf.pushforward CommRingCat
                      (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
                    (ObjectProperty.FullSubcategory.obj (P :=
                      Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                      (structureSheaf (↑S : Type u))))
                  p) :
              Type u) :
          (a : (↑R : Type u)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat
                          (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                      (structureSheaf (↑S : Type u)).obj).stalk
                  p) :
              Type u))
        x :
      (↑(TopCat.Presheaf.stalk
            (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
              (TopCat.Presheaf.pushforward CommRingCat
                (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : Type u))))
            p) :
        Type u))

Tactic:
rw [algebraMap_pushforward_stalk, toPushforwardStalk_comp]

Premises used: AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp, AlgebraicGeometry.StructureSheaf.algebraMap_pushforward_stalk
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑R : Type u)
inst : Algebra (↑R : Type u) (↑S : Type u)
⊢ ∀
    (y :
      (↑(TopCat.Presheaf.stalk
            (Functor.obj (C := TopCat.Presheaf CommRingCat (Spec.topObj (CommRingCat.of (↑S : Type u))))
              (TopCat.Presheaf.pushforward CommRingCat
                (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                (structureSheaf (↑S : Type u))))
            p) :
        Type u)),
    ∃ (x : (↑S : Type u) × ↥p.asIdeal.primeCompl),
      x.2 • y =
        (toPushforwardStalkAlgHom R S p :
            (a : (↑S : Type u)) →
              (↑(((TopCat.Presheaf.pushforward CommRingCat
                            (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))).obj
                        (structureSheaf (↑S : Type u)).obj).stalk
                    p) :
                Type u))
          x.1

Tactic:
apply isLocalizedModule_toPushforwardStalkAlgHom_aux

Premises used: AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : (↑Γ(X, U) : Type u)
hf : x ∈ X.basicOpen f
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op U)) : Type u)) (β := (↑(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 U x hx)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
rw :
  ∀
    (H :
      ∀ (x_1 : (↑(X.presheaf.obj (Opposite.op U)) : Type u)),
        Eq (α := (↑(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 U x hx) :
                  (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
                x_1 :
              (↑(X.presheaf.stalk x) : Type u))
            (0 : (↑(X.presheaf.stalk x) : Type u)) →
          x_1 = 0)
    (x_1 : (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)),
    Eq (α := (↑(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.basicOpen f) x hf) :
              (a : (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            x_1 :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u)) →
      x_1 = 0
⊢ Function.Injective (α := (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)) (β :=
    (↑(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.basicOpen f) x hf)) :
      (a : (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))

Tactic:
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero] at H ⊢

Premises used: RingHom.ker_eq_bot_iff_eq_zero, RingHom.injective_iff_ker_eq_bot
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : (↑Γ(X, U) : Type u)
hf : x ∈ X.basicOpen f
H :
  ∀ (x_1 : (↑(X.presheaf.obj (Opposite.op U)) : Type u)),
    Eq (α := (↑(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 U x hx) :
              (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            x_1 :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u)) →
      x_1 = 0
t : (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)
ht :
  Eq (α := (↑(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.basicOpen f) x hf) :
          (a : (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        t :
      (↑(X.presheaf.stalk x) : Type u))
    (0 : (↑(X.presheaf.stalk x) : Type u))
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)

Tactic:
have := hU.isLocalization_basicOpen f
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : (↑Γ(X, U) : Type u)
hf : x ∈ X.basicOpen f
H :
  ∀ (x_1 : (↑(X.presheaf.obj (Opposite.op U)) : Type u)),
    Eq (α := (↑(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 U x hx) :
              (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            x_1 :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u)) →
      x_1 = 0
t : (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)
ht :
  Eq (α := (↑(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.basicOpen f) x hf) :
          (a : (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        t :
      (↑(X.presheaf.stalk x) : Type u))
    (0 : (↑(X.presheaf.stalk x) : Type u))
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
obtain :
  ∀ (t : (↑Γ(X, U) : Type u)) (s : ↥(Submonoid.powers f))
    (ht :
      Eq (α := (↑(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.basicOpen f) x hf) :
              (a : (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u) t s) :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u))),
    Eq (α := (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
      (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u) t s) 0
⊢ t = 0

Tactic:
obtain ⟨t, s, rfl⟩ := IsLocalization.exists_mk'_eq (.powers f) t

Premises used: Submonoid.powers, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : (↑Γ(X, U) : Type u)
hf : x ∈ X.basicOpen f
H :
  ∀ (x_1 : (↑(X.presheaf.obj (Opposite.op U)) : Type u)),
    Eq (α := (↑(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 U x hx) :
              (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            x_1 :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u)) →
      x_1 = 0
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
t : (↑Γ(X, U) : Type u)
s : ↥(Submonoid.powers f)
ht :
  Membership.mem (γ := Ideal (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
    (RingHom.ker (F :=
      (fun (R S : CommRingCat.{u}) ↦ RingHom.{u, u} (↑R : Type u) (↑S : Type u))
        (X.presheaf.obj (Opposite.op (X.basicOpen f))) (X.presheaf.stalk x))
      (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.basicOpen f) x hf)))
    (HMul.hMul (α := (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)) (β :=
      (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
      ((algebraMap (↑Γ(X, U) : Type u) (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u) :
            (a : (↑Γ(X, U) : Type u)) → (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
          t :
        (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
      (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u) 1 s :
        (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)))
⊢ IsUnit (M := (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
    (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u) 1 s)

Tactic:
@isUnit_of_invertible _ _ _ (@IsLocalization.invertible_mk'_one ..)

Premises used: isUnit_of_invertible
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : (↑Γ(X, U) : Type u)
hf : x ∈ X.basicOpen f
H :
  ∀ (x_1 : (↑(X.presheaf.obj (Opposite.op U)) : Type u)),
    Eq (α := (↑(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 U x hx) :
              (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            x_1 :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u)) →
      x_1 = 0
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
t : (↑Γ(X, U) : Type u)
s : ↥(Submonoid.powers f)
ht :
  Membership.mem (γ := Ideal (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
    (RingHom.ker (F :=
      (fun (R S : CommRingCat.{u}) ↦ RingHom.{u, u} (↑R : Type u) (↑S : Type u))
        (X.presheaf.obj (Opposite.op (X.basicOpen f))) (X.presheaf.stalk x))
      (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.basicOpen f) x hf)))
    (HMul.hMul (α := (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)) (β :=
      (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
      ((algebraMap (↑Γ(X, U) : Type u) (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u) :
            (a : (↑Γ(X, U) : Type u)) → (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
          t :
        (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
      (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u) 1 s :
        (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u)))
⊢ IsUnit (M := (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u))
    (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f))) : Type u) 1 s)

Tactic:
exact @isUnit_of_invertible _ _ _ (@IsLocalization.invertible_mk'_one ..)

Premises used: isUnit_of_invertible