Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
r : R
α : Presheaf.stalk (moduleStructurePresheaf R M).presheaf x ≅
  (forget₂ (ModuleCat R) Ab).obj ((structurePresheafInModuleCat R M).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ (ModuleCat R) Ab).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ToType ((moduleStructurePresheaf R M).presheaf.obj (op U))
this✝ :
  Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU ≫ α.hom =
    (forget₂ (ModuleCat R) Ab).map ((structurePresheafInModuleCat R M).germ U x hxU)
this :
  ∀ (m : ↑((moduleStructurePresheaf R M).presheaf.obj (op U))),
    (ConcreteCategory.hom α.hom)
        ((ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) m) =
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ U x hxU)) m
⊢ (ConcreteCategory.hom α.hom) (r • (germₗ M U x hxU) s) =
    r •
      have this :=
        (Limits.colimit.isoColimitCocone
                {
                  cocone :=
                    (forget₂ (ModuleCat R) Ab).mapCocone
                      (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
                  isColimit :=
                    Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
                      (Limits.colimit.isColimit
                        ((OpenNhds.inclusion x).op ⋙
                          structurePresheafInModuleCat R M)) }).addCommGroupIsoToAddEquiv.toFun
          ((ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) s);
      this

Tactic:
← map_smul

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
r : R
α : Presheaf.stalk (moduleStructurePresheaf R M).presheaf x ≅
  (forget₂ (ModuleCat R) Ab).obj ((structurePresheafInModuleCat R M).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ (ModuleCat R) Ab).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ToType ((moduleStructurePresheaf R M).presheaf.obj (op U))
this✝ :
  Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU ≫ α.hom =
    (forget₂ (ModuleCat R) Ab).map ((structurePresheafInModuleCat R M).germ U x hxU)
this :
  ∀ (m : ↑((moduleStructurePresheaf R M).presheaf.obj (op U))),
    (ConcreteCategory.hom α.hom)
        ((ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) m) =
      (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ U x hxU)) m
⊢ (ConcreteCategory.hom α.hom) ((germₗ M U x hxU) (r • s)) =
    r •
      have this :=
        (Limits.colimit.isoColimitCocone
                {
                  cocone :=
                    (forget₂ (ModuleCat R) Ab).mapCocone
                      (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
                  isColimit :=
                    Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
                      (Limits.colimit.isColimit
                        ((OpenNhds.inclusion x).op ⋙
                          structurePresheafInModuleCat R M)) }).addCommGroupIsoToAddEquiv.toFun
          ((ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) s);
      this