awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
f g : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu₁ : U ≤ basicOpen g
hu₂ : U ≤ basicOpen f
rw :
  Eq (α :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R R))
      (op U))
    (const (f * g) (g * f) U ⋯) 1
rw₁ :
  Eq (α :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R R))
      (op U))
    (const (f * g) (f * g) U ⋯) 1
rw₂ rw₃ :
  Eq.{u + 1} (α :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R R))
      (op U))
    1 1
⊢ HMul.hMul (α :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R R))
        (op U))
      (const f g U hu₁) (const g f U hu₂) =
    1

Tactic:
rw [const_mul, const_congr rfl (mul_comm g f), const_self]

Premises used: AlgebraicGeometry.StructureSheaf.const_self, AlgebraicGeometry.StructureSheaf.const_congr, mul_comm, AlgebraicGeometry.StructureSheaf.const_mul, rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
f g₁ g₂ : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
rw : g₂ • (f * g₁) = (g₁ * g₂) • f
⊢ HMul.hMul (α :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R R))
        (op U))
      (const f g₁ U hu₁) (const g₁ g₂ U hu₂) =
    const f g₂ U hu₂

Tactic:
rw [const_mul, const_ext]

Premises used: AlgebraicGeometry.StructureSheaf.const_ext, AlgebraicGeometry.StructureSheaf.const_mul
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
f g₁ g₂ : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
simp : g₂ * (f * g₁) = g₁ * g₂ * f
⊢ g₂ • (f * g₁) = (g₁ * g₂) • f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
f g₁ g₂ : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ g₂ * (f * g₁) = g₁ * g₂ * f

Tactic:
ring
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
f g₁ g₂ : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
rw :
  HMul.hMul (α :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R R))
        (op U))
      (const f g₁ U hu₁) (const g₁ g₂ U hu₂) =
    const f g₂ U hu₂
rw₁ rw₂ :
  Eq (α :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R R))
      (op U))
    (const f g₂ U hu₂) (const f g₂ U hu₂)
⊢ HMul.hMul (α :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R R))
        (op U))
      (const g₁ g₂ U hu₂) (const f g₁ U hu₁) =
    const f g₂ U hu₂

Tactic:
rw [mul_comm, const_mul_cancel]

Premises used: AlgebraicGeometry.StructureSheaf.const_mul_cancel, mul_comm
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f₁ f₂ : M
g₁ g₂ : R
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
H : g₁ • f₂ = g₂ • f₁
x : ↥(unop (op U))
⊢ Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
    ((↑(const f₁ g₁ U hu₁) : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x :
      Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
    ((↑(const f₂ g₂ U hu₂) : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))) x :
      Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))

Tactic:
simp [LocalizedModule.mk_eq, Localizations, Submonoid.smul_def, H]

Premises used: AlgebraicGeometry.StructureSheaf.Localizations, LocalizedModule.mk_eq, Submonoid.smul_def
-- 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
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
m : M
⊢ U ≤ basicOpen 1

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
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
x x_1 : M
⊢ const (x + x_1) 1 U ⋯ =
    HAdd.hAdd (α :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op U))
      (const x 1 U ⋯) (const x_1 1 U ⋯)

Tactic:
simp [const_add]

Premises used: AlgebraicGeometry.StructureSheaf.const_add
-- 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
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
x : R
x_1 : M
⊢ const (x • x_1) 1 U ⋯ =
    HSMul.hSMul (α := R) (β :=
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op U))
      ((RingHom.id R : (a : R) → R) x : R) (const x_1 1 U ⋯)

Tactic:
simp [smul_const]

Premises used: AlgebraicGeometry.StructureSheaf.smul_const
-- 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
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
f : M
⊢ U ≤ basicOpen 1

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
f : M
⊢ Eq (α :=
    Functor.obj
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op U))
    ((toOpenₗ R M U : (a : M) → (structureSheafInType R M).obj.obj (op U)) f :
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op U))
    (const f 1 U ⋯ :
      Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op U))

Tactic:
rfl

Premises used: AlgebraicGeometry.StructureSheaf.const, rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
f : R
⊢ LE.le (α := Opens (↑(PrimeSpectrum.Top R) : Type u)) (basicOpen f) (basicOpen 1)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
⊢ IsUnit (M :=
    Module.End
      (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R R))
        (op (basicOpen f)))
      (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen f))))
    ((algebraMap
            (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R R))
              (op (basicOpen f)))
            (Module.End
              (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                  (structureSheafInType R R))
                (op (basicOpen f)))
              (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                  (structureSheafInType R M))
                (op (basicOpen f)))) :
          (a : (structureSheafInType R R).obj.obj (op (basicOpen f))) →
            Module.End ((structureSheafInType R R).obj.obj (op (basicOpen f)))
              ((structureSheafInType R M).obj.obj (op (basicOpen f))))
        ((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)))
                  (structureSheafInType R R))
                (op (basicOpen f))) :
            (a : R) → (structureSheafInType R R).obj.obj (op (basicOpen f)))
          f) :
      Module.End
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R R))
          (op (basicOpen f)))
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op (basicOpen f))))

Tactic:
have := (isUnit_basicOpen f).map
    (algebraMap _ (Module.End Γ(R, basicOpen f) Γ(M, basicOpen f)))
-- 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
f : R
simp :
  ∀ (a : R) (b : Membership.mem (γ := Submonoid R) (Submonoid.powers f) a),
    IsUnit (M :=
      Module.End R
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op (basicOpen f))))
      ((algebraMap R
              (Module.End R
                (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                    (structureSheafInType R M))
                  (op (basicOpen f)))) :
            (a : R) → Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))
          a :
        Module.End R
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R M))
            (op (basicOpen f))))
⊢ ∀ (x : ↥(Submonoid.powers f)),
    IsUnit (M :=
      Module.End R
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op (basicOpen f))))
      ((algebraMap R
              (Module.End R
                (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                    (structureSheafInType R M))
                  (op (basicOpen f)))) :
            (a : R) → Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))
          (↑x : R) :
        Module.End R
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R M))
            (op (basicOpen f))))

Tactic:
simp only [Subtype.forall]

Premises used: Subtype.forall
-- 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
f : R
⊢ ∀ (a : R) (b : Membership.mem (γ := Submonoid R) (Submonoid.powers f) a),
    IsUnit (M :=
      Module.End R
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op (basicOpen f))))
      ((algebraMap R
              (Module.End R
                (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                    (structureSheafInType R M))
                  (op (basicOpen f)))) :
            (a : R) → Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))
          a :
        Module.End R
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R M))
            (op (basicOpen f))))

Tactic:
Submonoid.powers_le (P := (IsUnit.submonoid _).comap (algebraMap R _)).mpr
      (isUnit_basicOpen_end ..)

Premises used: Iff.mpr, Set.Mem, setOf, IsUnit, _private.0.AlgebraicGeometry.StructureSheaf.isUnit_basicOpen_end, Set.preimage, Submonoid.powers_le
-- 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
f : R
⊢ ∀ (a : R) (b : Membership.mem (γ := Submonoid R) (Submonoid.powers f) a),
    IsUnit (M :=
      Module.End R
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op (basicOpen f))))
      ((algebraMap R
              (Module.End R
                (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                    (structureSheafInType R M))
                  (op (basicOpen f)))) :
            (a : R) → Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))
          a :
        Module.End R
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R M))
            (op (basicOpen f))))

Tactic:
exact Submonoid.powers_le (P := (IsUnit.submonoid _).comap (algebraMap R _)).mpr
      (isUnit_basicOpen_end ..)

Premises used: Iff.mpr, _private.0.AlgebraicGeometry.StructureSheaf.isUnit_basicOpen_end, Submonoid.powers_le
-- 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 : R
f : M
g : ↥(Submonoid.powers s)
⊢ ∀ (n : ℕ), LE.le (α := Opens (PrimeSpectrum R)) (basicOpen s) (basicOpen (s ^ n))

Tactic:
have := PrimeSpectrum.le_basicOpen_pow s
-- 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 : R
f : M
g : ↥(Submonoid.powers s)
this : ∀ (n : ℕ), LE.le (α := Opens (PrimeSpectrum R)) (basicOpen s) (basicOpen (s ^ n))
⊢ LE.le (α := Opens (↑(PrimeSpectrum.Top R) : Type u)) (basicOpen s) (basicOpen (↑g : R))

Tactic:
aesop (add simp [Submonoid.mem_powers_iff])

Premises used: Submonoid.mem_powers_iff
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : R
f : M
g : ↥(Submonoid.powers s)
obtain :
  ∀ (n : ℕ),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen s)))
      ((toBasicOpenₗ R M s : (a : LocalizedModule.Away s M) → (structureSheafInType R M).obj.obj (op (basicOpen s)))
          (LocalizedModule.mk f
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers s) x)
              ((fun (x : ℕ) ↦ s ^ x) n) ⋯)) :
        Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op (basicOpen s)))
      (const f
          (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers s) x)
                ((fun (x : ℕ) ↦ s ^ x) n) ⋯) :
            R)
          (basicOpen s) ⋯ :
        Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op (basicOpen s)))
⊢ Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen s)))
    ((toBasicOpenₗ R M s : (a : LocalizedModule.Away s M) → (structureSheafInType R M).obj.obj (op (basicOpen s)))
        (LocalizedModule.mk f g) :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen s)))
    (const f (↑g : R) (basicOpen s) ⋯ :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen s)))

Tactic:
obtain ⟨_, n, rfl⟩ := g

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : R
f : M
n : ℕ
rw :
  Eq (α :=
    Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
      (ObjectProperty.FullSubcategory.obj (P :=
        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
        (structureSheafInType R M))
      (op (basicOpen s)))
    ((toOpenₗ R M (basicOpen s) : (a : M) → (structureSheafInType R M).obj.obj (op (basicOpen s))) f :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen s)))
    (const (s ^ n • f) (s ^ n) (basicOpen s) ⋯ :
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen s)))
⊢ HSMul.hSMul (β :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen s)))
      (s ^ n)
      ((IsLocalizedModule.lift (Submonoid.powers s) (LocalizedModule.mkLinearMap (Submonoid.powers s) M)
              (toOpenₗ R M (basicOpen s)) ⋯ :
            (a : LocalizedModule.Away s M) → (structureSheafInType R M).obj.obj (op (basicOpen s)))
          (LocalizedModule.mk f
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers s) x) (s ^ n) ⋯)) :
        Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
            (structureSheafInType R M))
          (op (basicOpen s))) =
    HSMul.hSMul (β :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen s)))
      (s ^ n) (const f (s ^ n) (basicOpen s) ⋯)

Tactic:
rw [← map_smul, LocalizedModule.smul'_mk, ← Submonoid.mk_smul (S := .powers s) _ ⟨n, rfl⟩,
    LocalizedModule.mk_cancel, ← LocalizedModule.mkLinearMap_apply, IsLocalizedModule.lift_apply,
    smul_const]

Premises used: LocalizedModule.mk_cancel, Submonoid.mk_smul, AlgebraicGeometry.StructureSheaf.smul_const, LocalizedModule.smul'_mk, Exists.intro, IsLocalizedModule.lift_apply, LocalizedModule.mkLinearMap_apply, rfl, map_smul
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : R
f : M
n : ℕ
⊢ HSMul.hSMul (α := R) 1 (s ^ n • f) = s ^ n • f

Tactic:
simp