awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
x : (↑(PrimeSpectrum.Top R) : Type u)
m : M
α : stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x ≅
  Functor.obj
    (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
      ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
    (stalk (structurePresheafInModuleCat R M) x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        Functor.mapCocone
          (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves
          (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
⊢ Eq (α := (↑(stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u))
    ((toStalkₗ R M x : (a : M) → (↑(stalk (moduleStructurePresheaf R M).presheaf x) : Type u)) m :
      (↑(stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u))
    (((↑(LinearEquiv.symm (modulePresheafStalkIso R M x)) :
              (↑((structurePresheafInModuleCat R M).stalk x) : Type u) →ₗ[R]
                (↑(stalk (moduleStructurePresheaf R M).presheaf x) : Type u)) ∘ₗ
            ModuleCat.Hom.hom (toStalkₗ' R M x) :
          (a : M) → (↑(stalk (moduleStructurePresheaf R M).presheaf x) : Type u))
        m :
      (↑(stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u))

Tactic:
α.addCommGroupIsoToAddEquiv.eq_symm_apply.mpr ?_

Premises used: Iff.mpr, AddEquiv.eq_symm_apply, CategoryTheory.Iso.addCommGroupIsoToAddEquiv
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
x : (↑(PrimeSpectrum.Top R) : Type u)
m : M
α : stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x ≅
  Functor.obj
    (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
      ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
    (stalk (structurePresheafInModuleCat R M) x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        Functor.mapCocone
          (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves
          (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
⊢ Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) ⊤ x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
x : (↑(PrimeSpectrum.Top R) : Type u)
m : M
α : stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x ≅
  Functor.obj
    (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
      ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
    (stalk (structurePresheafInModuleCat R M) x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        Functor.mapCocone
          (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves
          (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
⊢ germ (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) ⊤ x ⋯ ≫ α.hom =
    CategoryTheory.Functor.map
      (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
        ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
      (germ (structurePresheafInModuleCat R M) ⊤ x ⋯)

Tactic:
have : TopCat.Presheaf.germ (moduleStructurePresheaf R M).presheaf ⊤ x (by simp) ≫ α.hom =
      (forget₂ _ _).map ((structurePresheafInModuleCat R M).germ ⊤ x (by simp)) :=
    Limits.colimit.isoColimitCocone_ι_hom (C := Ab) ..
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
x : (↑(PrimeSpectrum.Top R) : Type u)
⊢ IsLocalization.AtPrime (↑(stalk (structurePresheafInCommRingCat R) x) : Type u) x.asIdeal

Tactic:
(isLocalizedModule_iff_isLocalization' _ _).mp ?_

Premises used: isLocalizedModule_iff_isLocalization', Iff.mp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
x : (↑(PrimeSpectrum.Top R) : Type u)
refine :
  IsLocalizedModule (M' := (↑(stalk (structurePresheafInCommRingCat R) x) : Type u)) x.asIdeal.primeCompl
    (Algebra.linearMap R (↑(stalk (structurePresheafInCommRingCat R) x) : Type u))
⊢ IsLocalization.AtPrime (↑(stalk (structurePresheafInCommRingCat R) x) : Type u) x.asIdeal

Tactic:
refine (isLocalizedModule_iff_isLocalization' _ _).mp ?_

Premises used: isLocalizedModule_iff_isLocalization', Iff.mp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
x : (↑(PrimeSpectrum.Top R) : Type u)
⊢ IsLocalizedModule x.asIdeal.primeCompl
    ((↑(commRingCatStalkEquivModuleStalk R x) :
        (↑(stalk (moduleStructurePresheaf R R).presheaf x) : Type u) →ₗ[R]
          (↑((structurePresheafInCommRingCat R).stalk x) : Type u)) ∘ₗ
      toStalkₗ R R x)

Tactic:
IsLocalizedModule.of_linearEquiv x.asIdeal.primeCompl (toStalkₗ R R x)
      (commRingCatStalkEquivModuleStalk R x)

Premises used: AlgebraicGeometry.StructureSheaf.commRingCatStalkEquivModuleStalk, AlgebraicGeometry.StructureSheaf.toStalkₗ, Ideal.primeCompl, IsLocalizedModule.of_linearEquiv, PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
x : (↑(PrimeSpectrum.Top R) : Type u)
e_5 : Eq.{u + 1} (α := AddCommMonoid R) NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid
e_7 : HEq.{u + 1} (α := Module R R) Semiring.toModule (β := Module R R) Semiring.toModule
α : stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R R)) x ≅
  Functor.obj
    (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier) ⋙
      forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
    (stalk (structurePresheafInCommRingCat R) x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        Functor.mapCocone
          (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
              RingCat.carrier) ⋙
            forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
              AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
      isColimit :=
        Limits.isColimitOfPreserves
          (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
              RingCat.carrier) ⋙
            forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
              AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }
⊢ Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) ⊤ x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
x : (↑(PrimeSpectrum.Top R) : Type u)
e_5 : Eq.{u + 1} (α := AddCommMonoid R) NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid
e_7 : HEq.{u + 1} (α := Module R R) Semiring.toModule (β := Module R R) Semiring.toModule
α : stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R R)) x ≅
  Functor.obj
    (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier) ⋙
      forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommGrpCat.carrier))
    (stalk (structurePresheafInCommRingCat R) x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        Functor.mapCocone
          (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
              RingCat.carrier) ⋙
            forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
              AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
      isColimit :=
        Limits.isColimitOfPreserves
          (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
              RingCat.carrier) ⋙
            forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
              AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }
this :
  germ (PresheafOfModules.presheaf (moduleStructurePresheaf R R)) ⊤ x ⋯ ≫ α.hom =
    CategoryTheory.Functor.map
      (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
          RingCat.carrier) ⋙
        forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
          AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
          AddCommGrpCat.carrier))
      (germ (structurePresheafInCommRingCat R) ⊤ x ⋯)
⊢ Membership.mem (γ := Opens (↑(PrimeSpectrum.Top R) : Type u)) ⊤ x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
U V : (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ
i : V ⟶ U
⊢ Eq (α :=
    CommRingCat.of R ⟶
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        U)
    (CommRingCat.ofHom
        (algebraMap R
          (Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R R))
            V)) ≫
      CategoryTheory.Functor.map
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        i)
    (CommRingCat.ofHom
      (algebraMap R
        (Functor.obj
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R R))
          U)))

Tactic:
rfl

Premises used: Set.Mem, setOf, AlgebraicGeometry.StructureSheaf.sectionsSubalgebra, RingHom.codRestrict, rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
p : PrimeSpectrum R
r : R
⊢ Eq (α := (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf R)) p) : Type u))
    ((algebraMap R (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf R)) p) : Type u) :
          (a : R) → (↑((structureSheaf R).presheaf.stalk p) : Type u))
        r :
      (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf R)) p) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (toStalk R p) :
          (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk p) : Type u))
        r :
      (↑(Presheaf.stalk (structurePresheafInCommRingCat R) p) : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
p : PrimeSpectrum R
⊢ IsLocalization.AtPrime (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf R)) p) : Type u) p.asIdeal

Tactic:
inferInstanceAs (IsLocalization.AtPrime ((structurePresheafInCommRingCat R).stalk p) p.asIdeal)

Premises used: _private.0.AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk._proof_1
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
r : R
⊢ IsLocalization.Away r
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheaf R))
          (op (basicOpen r))) :
      Type u)

Tactic:
inferInstanceAs (IsLocalization.Away r Γ(R, basicOpen r))

Premises used: _private.0.AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen._proof_1
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
r : R
⊢ Epi (X := CommRingCat.of R) (Y :=
    CommRingCat.of
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op (basicOpen r))) :
        Type u))
    (CommRingCat.ofHom
      (algebraMap R
        (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheaf R))
              (op (basicOpen r))) :
          Type u)))

Tactic:
⟨fun _ _ h => CommRingCat.hom_ext (IsLocalization.ringHom_ext (Submonoid.powers r)
    (CommRingCat.hom_ext_iff.mp h))⟩

Premises used: CommRingCat.hom_ext, CategoryTheory.Epi.mk, CommRingCat.hom_ext_iff, Submonoid.powers, Iff.mp, IsLocalization.ringHom_ext
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : CommRingCat
⊢ Eq.{u_1 + 1} (α :=
    CommRingCat.of (↑R : Type u_1) ⟶
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf
            (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
          (structureSheaf (↑R : Type u_1)))
        (op ⊤))
    (Iso.hom (globalSectionsIso (↑R : Type u_1)))
    (CommRingCat.ofHom
      (algebraMap (↑R : Type u_1)
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf
              (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
            (structureSheafInType (↑R : Type u_1) (↑R : Type u_1)))
          (op ⊤))))

Tactic:
rfl

Premises used: Set.Mem, setOf, AlgebraicGeometry.StructureSheaf.sectionsSubalgebra, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, RingHom.codRestrict, rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u_1
inst : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ Eq (α := CommRingCat.of R ⟶ Presheaf.stalk (Sheaf.presheaf (structureSheaf R)) x)
    (CategoryStruct.comp (Y :=
        CommRingCat.of
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u_1))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u_1)))
              (structureSheafInType R R))
            (op ⊤)))
        (CommRingCat.ofHom
          (algebraMap R
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u_1))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u_1)))
                (structureSheafInType R R))
              (op ⊤))))
        (Presheaf.germ (structurePresheafInCommRingCat R) ⊤ y _root_.trivial) ≫
      Presheaf.stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h)
    (CategoryStruct.comp (Y :=
      CommRingCat.of
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u_1))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u_1)))
            (structureSheafInType R R))
          (op ⊤)))
      (CommRingCat.ofHom
        (algebraMap R
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u_1))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u_1)))
              (structureSheafInType R R))
            (op ⊤))))
      (Presheaf.germ (structurePresheafInCommRingCat R) ⊤ x _root_.trivial))

Tactic:
simp [structureSheaf]

Premises used: AlgebraicGeometry.Spec.structureSheaf
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
S : Type u
inst_5 : CommRing S
N : Type u
inst_6 : AddCommGroup N
inst_7 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : (↑(PrimeSpectrum.Top S) : Type u)
this_1 : Module R N := Module.compHom N σ
this_2 : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
⊢ IsUnit (M := Module.End S (LocalizedModule y.asIdeal.primeCompl N))
    ((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
          (a : S) → Module.End S (LocalizedModule y.asIdeal.primeCompl N))
        (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑x : R)) ⋯) : S) :
      Module.End S (LocalizedModule y.asIdeal.primeCompl N))

Tactic:
have := IsLocalizedModule.map_units (S := y.asIdeal.primeCompl)
        (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ⟨σ x, x.2⟩