awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
f : R
hf : Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen f) x
this :
  Function.Bijective (α := (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) (β :=
    (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
    (⇑((algebraMap (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
                (Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
                  (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
              (a : (↑((structurePresheafInCommRingCat R).stalk x) : Type u)) →
                Module.End (↑((structurePresheafInCommRingCat R).stalk x) : Type u)
                  (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (toStalk R x) :
                (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
              f) :
          Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
            (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
      (a : (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) →
        (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
⊢ Function.Bijective (α := (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) (β :=
    (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
    (⇑((algebraMap (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
                (Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
                  (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
              (a : (↑((structurePresheafInCommRingCat R).stalk x) : Type u)) →
                Module.End (↑((structurePresheafInCommRingCat R).stalk x) : Type u)
                  (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (toStalk R x) :
                (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
              f) :
          Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
            (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
      (a : (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) →
        (↑((structurePresheafInModuleCat R M).stalk x) : Type u))

Tactic:
this
-- 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)
f : R
hf : Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen f) x
this :
  Function.Bijective (α := (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) (β :=
    (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
    (⇑((algebraMap (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
                (Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
                  (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
              (a : (↑((structurePresheafInCommRingCat R).stalk x) : Type u)) →
                Module.End (↑((structurePresheafInCommRingCat R).stalk x) : Type u)
                  (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (toStalk R x) :
                (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
              f) :
          Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
            (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
      (a : (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) →
        (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
a : (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)
h h₁ : f • a = f • a
⊢ f • a =
    HSMul.hSMul (α := (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (toStalk R x) :
            (a : R) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
          f :
        (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
      a

Tactic:
rw [toStalk_smul]

Premises used: _private.0.AlgebraicGeometry.StructureSheaf.toStalk_smul
-- 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)
f : M
s : ↥x.asIdeal.primeCompl
h :
  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 : R))))
    (const f 1 (basicOpen (↑s : R)) ⋯) (const ((↑s : R) • f) (↑s : R) (basicOpen (↑s : R)) ⋯)
⊢ Eq (α := (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
    (((ModuleCat.Hom.hom (Presheaf.germ (structurePresheafInModuleCat R M) (basicOpen (↑s : R)) x ⋯) :
            (↑(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 (basicOpen (↑s : R))))) :
                Type u) →ₗ[R]
              (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
          (a : (structureSheafInType R M).obj.obj (op (basicOpen (↑s : R)))) →
            (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        (const f 1 (basicOpen (↑s : R)) ⋯) :
      (↑(Presheaf.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 (↑s : R)))) (Y :=
            Presheaf.stalk (structurePresheafInModuleCat R M) x)
            (Presheaf.germ (structurePresheafInModuleCat R M) (basicOpen (↑s : R)) x ⋯) :
          (a : (structureSheafInType R M).obj.obj (op (basicOpen (↑s : R)))) →
            (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        (const ((↑s : R) • f) (↑s : R) (basicOpen (↑s : R)) ⋯) :
      (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))

Tactic:
congr 1
-- 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)
f : M
s : ↥x.asIdeal.primeCompl
⊢ HSMul.hSMul (α := R) 1 ((↑s : R) • f) = (↑s : R) • f

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)
x : (↑(PrimeSpectrum.Top R) : Type u)
hx : x ∈ U
⊢ Eq (α :=
    Functor.obj (structurePresheafInModuleCat R M) (op U) ⟶ ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))
    (Presheaf.germ (structurePresheafInModuleCat R M) U x hx ≫ stalkToLocalizationₗ R M x)
    (openToLocalizationₗ R M U x hx)

Tactic:
Limits.colimit.ι_desc _ _

Premises used: Set.Mem, CategoryTheory.Functor.comp, _private.0.AlgebraicGeometry.StructureSheaf.openToLocalizationₗ, CategoryTheory.Limits.colimit.ι_desc
-- 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)
rw :
  Eq (α := Quiver.Hom (V := ModuleCat R) (ModuleCat.of R M) (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)))
    (CategoryStruct.comp (Y :=
      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 ⊤)))
      (ModuleCat.ofHom (toOpenₗ R M ⊤)) (openToLocalizationₗ R M ⊤ x _root_.trivial))
    (ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M))
⊢ Eq (α := Quiver.Hom (V := ModuleCat R) (ModuleCat.of R M) (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)))
    (toStalkₗ' R M x ≫ stalkToLocalizationₗ R M x)
    (ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M))

Tactic:
rw [toStalkₗ', Category.assoc, germ_stalkToLocalizationₗ]

Premises used: CategoryTheory.Category.assoc, _private.0.AlgebraicGeometry.StructureSheaf.germ_stalkToLocalizationₗ, _private.0.AlgebraicGeometry.StructureSheaf.toStalkₗ'
-- 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 M) (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)))
    (CategoryStruct.comp (Y :=
      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 ⊤)))
      (ModuleCat.ofHom (toOpenₗ R M ⊤)) (openToLocalizationₗ R M ⊤ x _root_.trivial))
    (ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M))

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)
ih :
  ∀ (U : Opens (↑(PrimeSpectrum.Top R) : Type u)) (hxU : x ∈ U),
    germ (structurePresheafInModuleCat R M) U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x =
      germ (structurePresheafInModuleCat R M) U x hxU ≫ 𝟙 (stalk (structurePresheafInModuleCat R M) x)
⊢ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x = 𝟙 (stalk (structurePresheafInModuleCat R M) x)

Tactic:
apply stalk_hom_ext

Premises used: TopCat.Presheaf.stalk_hom_ext
-- 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)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxU : x ∈ U
ih :
  ∀ (s : (↑(Functor.obj (structurePresheafInModuleCat R M) (op U)) : Type u)),
    Eq (α := (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
      ((ModuleCat.Hom.hom
              (germ (structurePresheafInModuleCat R M) U x hxU ≫
                stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x) :
            (a : (↑((structurePresheafInModuleCat R M).obj (op U)) : Type u)) →
              (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
          s :
        (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
      ((ModuleCat.Hom.hom
              (germ (structurePresheafInModuleCat R M) U x hxU ≫ 𝟙 (stalk (structurePresheafInModuleCat R M) x)) :
            (a : (↑((structurePresheafInModuleCat R M).obj (op U)) : Type u)) →
              (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
          s :
        (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
⊢ germ (structurePresheafInModuleCat R M) U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x =
    germ (structurePresheafInModuleCat R M) U x hxU ≫ 𝟙 (stalk (structurePresheafInModuleCat R M) x)

Tactic:
ext 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
x : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxU : x ∈ U
s : (↑(Functor.obj (structurePresheafInModuleCat R M) (op U)) : Type u)
ih :
  ∀ (g : R) (hxg : Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen g) x) (igU : basicOpen g ≤ U) (f : M)
    (hs :
      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 g)))
        (const f g (basicOpen g) ⋯)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                  (structureSheafInType R M))
                igU.hom.op) :
            (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
              (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen g))))
          s)),
    Eq (α := (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
      ((ModuleCat.Hom.hom
              (germ (structurePresheafInModuleCat R M) U x hxU ≫
                stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x) :
            (a : (↑((structurePresheafInModuleCat R M).obj (op U)) : Type u)) →
              (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
          s :
        (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
      ((ModuleCat.Hom.hom
              (germ (structurePresheafInModuleCat R M) U x hxU ≫ 𝟙 (stalk (structurePresheafInModuleCat R M) x)) :
            (a : (↑((structurePresheafInModuleCat R M).obj (op U)) : Type u)) →
              (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
          s :
        (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
⊢ Eq (α := (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((ModuleCat.Hom.hom
            (germ (structurePresheafInModuleCat R M) U x hxU ≫
              stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x) :
          (a : (↑((structurePresheafInModuleCat R M).obj (op U)) : Type u)) →
            (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        s :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((ModuleCat.Hom.hom
            (germ (structurePresheafInModuleCat R M) U x hxU ≫ 𝟙 (stalk (structurePresheafInModuleCat R M) x)) :
          (a : (↑((structurePresheafInModuleCat R M).obj (op U)) : Type u)) →
            (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        s :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))

Tactic:
obtain ⟨g, hxg, igU, f, hs⟩ :=
      exists_const _ s x hxU

Premises used: AlgebraicGeometry.StructureSheaf.exists_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
x : (↑(PrimeSpectrum.Top R) : Type u)
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hxU : x ∈ U
s : (↑(Functor.obj (structurePresheafInModuleCat R M) (op U)) : Type u)
g : R
hxg : Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen g) x
igU : basicOpen g ≤ U
f : M
hs :
  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 g)))
    (const f g (basicOpen g) ⋯)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheafInType R M))
            igU.hom.op) :
        (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
          (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen g))))
      s)
⊢ Eq (α := (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((ModuleCat.Hom.hom (openToLocalizationₗ R M U x hxU ≫ localizationtoStalkₗ R M x) :
          (a : (↑((structurePresheafInModuleCat R M).obj (op U)) : Type u)) →
            (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        s :
      (↑(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 g))) (Y :=
            stalk (structurePresheafInModuleCat R M) x) (germ (structurePresheafInModuleCat R M) (basicOpen g) x hxg) :
          (a : (↑((structurePresheafInModuleCat R M).obj (op (basicOpen g))) : Type u)) →
            (↑((structurePresheafInModuleCat R M).stalk 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 U))
                (CategoryTheory.Functor.map (structurePresheafInModuleCat R M) igU.hom.op) :
              (a : (↑((structurePresheafInModuleCat R M).obj (op U)) : Type u)) →
                (↑((structurePresheafInModuleCat R M).obj (op (basicOpen g))) : Type u))
            s :
          (↑(Functor.obj (structurePresheafInModuleCat R M) (op (basicOpen g))) : Type u)) :
      (↑(stalk (structurePresheafInModuleCat R M) x) : Type u))

Tactic:
congr(localizationtoStalkₗ R M x (openToLocalizationₗ R M _ x hxg $hs)).symm.trans ?_

Premises used: PrimeSpectrum.basicOpen, congrArg, CategoryTheory.ConcreteCategory.hom, Set.Mem, _private.0.AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ, LocalizedModule.liftOn, id, _private.0.AlgebraicGeometry.StructureSheaf.openToLocalizationₗ, LocalizedModule.lift', Eq.symm, DFunLike.coe, 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)
hf :
  Eq (α :=
    (↑(ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)) : Type u) →ₗ[R]
      (↑(ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)) : Type u))
    (ModuleCat.Hom.hom (localizationtoStalkₗ R M x ≫ stalkToLocalizationₗ R M x))
    (ModuleCat.Hom.hom (𝟙 (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))))
⊢ 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:
ext1
-- 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)
⊢ Eq (α :=
    (↑(ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)) : Type u) →ₗ[R]
      (↑(ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)) : Type u))
    (ModuleCat.Hom.hom (localizationtoStalkₗ R M x ≫ stalkToLocalizationₗ R M x))
    (ModuleCat.Hom.hom (𝟙 (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))))

Tactic:
IsLocalizedModule.ext x.asIdeal.primeCompl (LocalizedModule.mkLinearMap ..)
      (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap ..)) ?_

Premises used: OreLocalization, IsLocalizedModule.ext, Quotient, LocalizedModule.mkLinearMap, Ideal.primeCompl, IsLocalizedModule.map_units, 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)
hf :
  ∀ (x_1 : M),
    Eq (α := LocalizedModule x.asIdeal.primeCompl M)
      ((ModuleCat.Hom.hom (localizationtoStalkₗ R M x ≫ stalkToLocalizationₗ R M x) ∘ₗ
              LocalizedModule.mkLinearMap x.asIdeal.primeCompl M :
            (a : M) → LocalizedModule x.asIdeal.primeCompl M)
          x_1 :
        LocalizedModule x.asIdeal.primeCompl M)
      (((ModuleCat.Hom.hom (𝟙 (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))) ∘ₗ
                LocalizedModule.mkLinearMap x.asIdeal.primeCompl M :
              M →ₗ[R] LocalizedModule x.asIdeal.primeCompl M) :
            (a : M) → LocalizedModule x.asIdeal.primeCompl M)
          x_1 :
        LocalizedModule x.asIdeal.primeCompl M)
⊢ Eq (α := M →ₗ[R] LocalizedModule x.asIdeal.primeCompl M)
    (ModuleCat.Hom.hom (localizationtoStalkₗ R M x ≫ stalkToLocalizationₗ R M x) ∘ₗ
      LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
    (ModuleCat.Hom.hom (𝟙 (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))) ∘ₗ
      LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)

Tactic:
ext
-- 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)
x_1 : M
hf :
  Eq (α := LocalizedModule x.asIdeal.primeCompl M)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of R M)
            (ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)) :
          (a : M) → LocalizedModule x.asIdeal.primeCompl M)
        x_1 :
      LocalizedModule x.asIdeal.primeCompl M)
    ((LocalizedModule.mkLinearMap x.asIdeal.primeCompl M : (a : M) → LocalizedModule x.asIdeal.primeCompl M) x_1 :
      LocalizedModule x.asIdeal.primeCompl M)
⊢ Eq (α := LocalizedModule x.asIdeal.primeCompl M)
    ((ModuleCat.Hom.hom (stalkToLocalizationₗ R M x) :
          (a : (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) → LocalizedModule x.asIdeal.primeCompl M)
        ((IsLocalizedModule.lift x.asIdeal.primeCompl (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)
              (ModuleCat.Hom.hom (toStalkₗ' R M x)) ⋯ :
            (a : LocalizedModule x.asIdeal.primeCompl M) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
          (LocalizedModule.mk x_1 1)) :
      LocalizedModule x.asIdeal.primeCompl M)
    (LocalizedModule.mk x_1 1 : LocalizedModule x.asIdeal.primeCompl M)

Tactic:
rw [← LocalizedModule.mkLinearMap_apply, IsLocalizedModule.lift_apply,
      elementwise_of% toStalkₗ'_stalkToFiberRingHom (M := M) x]

Premises used: _private.0.AlgebraicGeometry.StructureSheaf.toStalkₗ'_stalkToFiberRingHom, IsLocalizedModule.lift_apply, LocalizedModule.mkLinearMap_apply
-- 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)
x_1 : M
⊢ Eq (α := LocalizedModule x.asIdeal.primeCompl M)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of R M)
            (ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)) :
          (a : M) → LocalizedModule x.asIdeal.primeCompl M)
        x_1 :
      LocalizedModule x.asIdeal.primeCompl M)
    ((LocalizedModule.mkLinearMap x.asIdeal.primeCompl M : (a : M) → LocalizedModule x.asIdeal.primeCompl M) x_1 :
      LocalizedModule x.asIdeal.primeCompl M)

Tactic:
simp