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 R
⊢ IsIso (X := stalk (structurePresheafInModuleCat R M) x) (stalkToLocalizationₗ R M x)

Tactic:
(stalkIsoₗ R M x).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Limits.colimit.desc, _private.0.AlgebraicGeometry.StructureSheaf.stalkIsoₗ, _private.0.AlgebraicGeometry.StructureSheaf.stalkToLocalizationₗ
-- 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 R
⊢ IsIso (X := ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)) (localizationtoStalkₗ R M x)

Tactic:
(stalkIsoₗ R M x).isIso_inv

Premises used: _private.0.AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ, CategoryTheory.Iso.isIso_inv, _private.0.AlgebraicGeometry.StructureSheaf.stalkIsoₗ
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : (↑(PrimeSpectrum.Top R) : Type u)
⊢ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x = 𝟙 (stalk (structurePresheafInModuleCat R M) x)

Tactic:
(stalkIsoₗ R M x).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, _private.0.AlgebraicGeometry.StructureSheaf.stalkIsoₗ
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : (↑(PrimeSpectrum.Top R) : Type u)
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))
      (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)))
    (localizationtoStalkₗ R M x ≫ stalkToLocalizationₗ R M x)
    (𝟙 (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)))

Tactic:
(stalkIsoₗ R M x).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, _private.0.AlgebraicGeometry.StructureSheaf.stalkIsoₗ
-- 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 (M' := (↑(stalk (structurePresheafInModuleCat R M) x) : Type u)) x.asIdeal.primeCompl
    ((↑(LinearEquiv.symm (Iso.toLinearEquiv (stalkIsoₗ R M x))) :
        LocalizedModule x.asIdeal.primeCompl M →ₗ[R] (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) ∘ₗ
      LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)

Tactic:
IsLocalizedModule.of_linearEquiv x.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) (stalkIsoₗ R M x).toLinearEquiv.symm

Premises used: LinearEquiv.symm, CategoryTheory.Iso.toLinearEquiv, _private.0.AlgebraicGeometry.StructureSheaf.stalkIsoₗ, LocalizedModule.mkLinearMap, 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)
h :
  Eq (α := (↑(ModuleCat.of R M) : Type u) →ₗ[R] (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    (ModuleCat.Hom.hom (toStalkₗ' R M x))
    ((↑(LinearEquiv.symm (Iso.toLinearEquiv (stalkIsoₗ R M x))) :
        LocalizedModule x.asIdeal.primeCompl M →ₗ[R] (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) ∘ₗ
      LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
⊢ IsLocalizedModule (M := (↑(ModuleCat.of R M) : Type u)) x.asIdeal.primeCompl (ModuleCat.Hom.hom (toStalkₗ' R M x))

Tactic:
convert!
    IsLocalizedModule.of_linearEquiv x.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) (stalkIsoₗ R M x).toLinearEquiv.symm

Premises used: LinearEquiv.symm, CategoryTheory.Iso.toLinearEquiv, _private.0.AlgebraicGeometry.StructureSheaf.stalkIsoₗ, LocalizedModule.mkLinearMap, 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)
h :
  ∀ (m : (↑(ModuleCat.of R M) : Type u)),
    Eq (α := (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
      ((ModuleCat.Hom.hom (toStalkₗ' R M x) :
            (a : (↑(ModuleCat.of R M) : Type u)) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
          m :
        (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
      (((↑(LinearEquiv.symm (Iso.toLinearEquiv (stalkIsoₗ R M x))) :
                LocalizedModule x.asIdeal.primeCompl M →ₗ[R]
                  (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) ∘ₗ
              LocalizedModule.mkLinearMap x.asIdeal.primeCompl M :
            (a : (↑(ModuleCat.of R M) : Type u)) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
          m :
        (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
⊢ Eq (α := (↑(ModuleCat.of R M) : Type u) →ₗ[R] (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    (ModuleCat.Hom.hom (toStalkₗ' R M x))
    ((↑(LinearEquiv.symm (Iso.toLinearEquiv (stalkIsoₗ R M x))) :
        LocalizedModule x.asIdeal.primeCompl M →ₗ[R] (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) ∘ₗ
      LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)

Tactic:
ext m
-- 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 : (↑(ModuleCat.of R M) : Type u)
⊢ Eq (α := (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((ModuleCat.Hom.hom (toStalkₗ' R M x) :
          (a : (↑(ModuleCat.of R M) : Type u)) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        m :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    (((↑(LinearEquiv.symm (Iso.toLinearEquiv (stalkIsoₗ R M x))) :
              LocalizedModule x.asIdeal.primeCompl M →ₗ[R] (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) ∘ₗ
            LocalizedModule.mkLinearMap x.asIdeal.primeCompl M :
          (a : (↑(ModuleCat.of R M) : Type u)) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        m :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))

Tactic:
.trans ?_ (localizationtoStalkₗ_mk ..).symm

Premises used: _private.0.AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ_mk, Eq.symm, Eq.trans
-- 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 : (↑(ModuleCat.of R M) : Type u)
h :
  Eq (α := (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((ModuleCat.Hom.hom (toStalkₗ' R M x) :
          (a : (↑(ModuleCat.of R M) : Type u)) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        m :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := Functor.obj (structurePresheafInModuleCat R M) (op (basicOpen (↑1 : R)))) (Y :=
            stalk (structurePresheafInModuleCat R M) x)
            (germ (structurePresheafInModuleCat R M) (basicOpen (↑1 : R)) x ⋯) :
          (a : (↑((structurePresheafInModuleCat R M).obj (op (basicOpen (↑1 : R)))) : Type u)) →
            (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        (const m (↑1 : R) (basicOpen (↑1 : R)) ⋯) :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
⊢ Eq (α := (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((ModuleCat.Hom.hom (toStalkₗ' R M x) :
          (a : (↑(ModuleCat.of R M) : Type u)) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        m :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    (((↑(LinearEquiv.symm (Iso.toLinearEquiv (stalkIsoₗ R M x))) :
              LocalizedModule x.asIdeal.primeCompl M →ₗ[R] (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) ∘ₗ
            LocalizedModule.mkLinearMap x.asIdeal.primeCompl M :
          (a : (↑(ModuleCat.of R M) : Type u)) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        m :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))

Tactic:
refine .trans ?_ (localizationtoStalkₗ_mk ..).symm
-- 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 : (↑(ModuleCat.of R M) : Type u)
h :
  Eq (α := (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    (((ModuleCat.Hom.hom (germ (structurePresheafInModuleCat R M) ⊤ x _root_.trivial) :
            (↑(ModuleCat.of 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 ⊤))) :
                Type u) →ₗ[R]
              (↑(stalk (structurePresheafInModuleCat R M) x) : Type u)) :
          (a : (structureSheafInType R M).obj.obj (op ⊤)) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        (const m 1 ⊤ ⋯) :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := Functor.obj (structurePresheafInModuleCat R M) (op (basicOpen 1))) (Y :=
              stalk (structurePresheafInModuleCat R M) x) (germ (structurePresheafInModuleCat R M) (basicOpen 1) x ⋯) :
            (↑(Functor.obj (structurePresheafInModuleCat R M) (op (basicOpen 1))) : Type u) →ₗ[R]
              (↑(stalk (structurePresheafInModuleCat R M) x) : Type u)) :
          (a : (structureSheafInType R M).obj.obj (op (basicOpen 1))) →
            (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        (const m 1 (basicOpen 1) ⋯) :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
⊢ Eq (α := (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((ModuleCat.Hom.hom (toStalkₗ' R M x) :
          (a : (↑(ModuleCat.of R M) : Type u)) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        m :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := Functor.obj (structurePresheafInModuleCat R M) (op (basicOpen (↑1 : R)))) (Y :=
            stalk (structurePresheafInModuleCat R M) x)
            (germ (structurePresheafInModuleCat R M) (basicOpen (↑1 : R)) x ⋯) :
          (a : (↑((structurePresheafInModuleCat R M).obj (op (basicOpen (↑1 : R)))) : Type u)) →
            (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        (const m (↑1 : R) (basicOpen (↑1 : R)) ⋯) :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))

Tactic:
dsimp +instances [toStalkₗ', toOpenₗ]

Premises used: AlgebraicGeometry.StructureSheaf.toOpenₗ, _private.0.AlgebraicGeometry.StructureSheaf.toStalkₗ'
-- 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 : (↑(ModuleCat.of R M) : Type u)
⊢ Eq (α := (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    (((ModuleCat.Hom.hom (germ (structurePresheafInModuleCat R M) ⊤ x _root_.trivial) :
            (↑(ModuleCat.of 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 ⊤))) :
                Type u) →ₗ[R]
              (↑(stalk (structurePresheafInModuleCat R M) x) : Type u)) :
          (a : (structureSheafInType R M).obj.obj (op ⊤)) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        (const m 1 ⊤ ⋯) :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := Functor.obj (structurePresheafInModuleCat R M) (op ⊤)) (Y :=
              stalk (structurePresheafInModuleCat R M) x) (germ (structurePresheafInModuleCat R M) ⊤ x ⋯) :
            (↑(Functor.obj (structurePresheafInModuleCat R M) (op ⊤)) : Type u) →ₗ[R]
              (↑(stalk (structurePresheafInModuleCat R M) x) : Type u)) :
          (a : (structureSheafInType R M).obj.obj (op ⊤)) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        (const m 1 ⊤ ⋯) :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))

Tactic:
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
x : (↑(PrimeSpectrum.Top R) : Type u)
m : 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)
r : R
m : M
⊢ 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 ⊤))
      r
      ((toOpenₗ R M ⊤ : (a : M) → (structureSheafInType R M).obj.obj (op ⊤)) m :
        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 ⊤)) =
    HSMul.hSMul (α :=
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (structurePresheafInCommRingCat R) (op ⊤)) :
        Type u))
      (β := (↑(PresheafOfModules.obj (moduleStructurePresheaf R M) (op ⊤)) : Type u))
      ((CommRingCat.Hom.hom'
              (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)))
                      (structureSheafInType R R))
                    (op ⊤)))) :
            (a : (↑(CommRingCat.of R) : Type u)) →
              (↑(CommRingCat.of ((structureSheafInType R R).obj.obj (op ⊤))) : Type u))
          r :
        (↑(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)))
                  (structureSheafInType R R))
                (op ⊤))) :
          Type u))
      ((toOpenₗ R M ⊤ : (a : M) → (structureSheafInType R M).obj.obj (op ⊤)) m :
        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 ⊤))

Tactic:
(IsScalarTower.algebraMap_smul Γ(R, _) (M := Γ(M, _)) _ _).symm

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, IsScalarTower.algebraMap_smul, Opposite.op, AlgebraicGeometry.structureSheafInType, Eq.symm, CategoryTheory.Functor.obj
-- 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)
r : R
m : M
⊢ 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 ⊤))
      r
      ((toOpenₗ R M ⊤ : (a : M) → (structureSheafInType R M).obj.obj (op ⊤)) m :
        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 ⊤)) =
    HSMul.hSMul (α :=
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (structurePresheafInCommRingCat R) (op ⊤)) :
        Type u))
      (β := (↑(PresheafOfModules.obj (moduleStructurePresheaf R M) (op ⊤)) : Type u))
      ((CommRingCat.Hom.hom'
              (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)))
                      (structureSheafInType R R))
                    (op ⊤)))) :
            (a : (↑(CommRingCat.of R) : Type u)) →
              (↑(CommRingCat.of ((structureSheafInType R R).obj.obj (op ⊤))) : Type u))
          r :
        (↑(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)))
                  (structureSheafInType R R))
                (op ⊤))) :
          Type u))
      ((toOpenₗ R M ⊤ : (a : M) → (structureSheafInType R M).obj.obj (op ⊤)) m :
        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 ⊤))

Tactic:
exact (IsScalarTower.algebraMap_smul Γ(R, _) (M := Γ(M, _)) _ _).symm

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, IsScalarTower.algebraMap_smul, Opposite.op, AlgebraicGeometry.structureSheafInType, Eq.symm, CategoryTheory.Functor.obj
-- 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 (M := (↑(ModuleCat.of R M) : Type u)) x.asIdeal.primeCompl
    ((↑(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))

Tactic:
IsLocalizedModule.of_linearEquiv x.asIdeal.primeCompl (toStalkₗ' R M x).hom
      (modulePresheafStalkIso R M x).symm

Premises used: LinearEquiv.symm, _private.0.AlgebraicGeometry.StructureSheaf.modulePresheafStalkIso, _private.0.AlgebraicGeometry.StructureSheaf.toStalkₗ', Ideal.primeCompl, IsLocalizedModule.of_linearEquiv, ModuleCat.Hom.hom, 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)
h :
  Eq (α := M →ₗ[R] (↑(stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u)) (toStalkₗ R M x)
    ((↑(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))
⊢ IsLocalizedModule (M' := (↑(stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u))
    x.asIdeal.primeCompl (toStalkₗ R M x)

Tactic:
convert!
    IsLocalizedModule.of_linearEquiv x.asIdeal.primeCompl (toStalkₗ' R M x).hom
      (modulePresheafStalkIso R M x).symm

Premises used: LinearEquiv.symm, _private.0.AlgebraicGeometry.StructureSheaf.modulePresheafStalkIso, _private.0.AlgebraicGeometry.StructureSheaf.toStalkₗ', Ideal.primeCompl, IsLocalizedModule.of_linearEquiv, ModuleCat.Hom.hom, 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)
h :
  ∀ (m : 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))
⊢ Eq (α := M →ₗ[R] (↑(stalk (PresheafOfModules.presheaf (moduleStructurePresheaf R M)) x) : Type u)) (toStalkₗ R M x)
    ((↑(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))

Tactic:
ext m