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
α : stalk (moduleStructurePresheaf R R).presheaf x ≅
  (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).obj ((structurePresheafInCommRingCat R).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ToType ((moduleStructurePresheaf R R).presheaf.obj (op U))
this :
  germ (moduleStructurePresheaf R R).presheaf U x hxU ≫ α.hom =
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map ((structurePresheafInCommRingCat R).germ U x hxU)
⊢ (ConcreteCategory.hom α.hom)
      (r • (@AlgebraicGeometry.StructureSheaf.germₗ R R inst✝⁴ inst✝⁴.toAddCommGroup Semiring.toModule U x hxU) s) =
    (ConcreteCategory.hom (toStalk R x)) ((RingHom.id R) r) *
      (Limits.colimit.isoColimitCocone
              {
                cocone :=
                  (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).mapCocone
                    (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
                isColimit :=
                  Limits.isColimitOfPreserves (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
                    (Limits.colimit.isColimit
                      ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }).addCommGroupIsoToAddEquiv.toFun
        ((ConcreteCategory.hom (germ (moduleStructurePresheaf R R).presheaf U x hxU)) s)

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
α : stalk (moduleStructurePresheaf R R).presheaf x ≅
  (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).obj ((structurePresheafInCommRingCat R).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ToType ((moduleStructurePresheaf R R).presheaf.obj (op U))
this :
  germ (moduleStructurePresheaf R R).presheaf U x hxU ≫ α.hom =
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map ((structurePresheafInCommRingCat R).germ U x hxU)
⊢ (ConcreteCategory.hom α.hom)
      ((@AlgebraicGeometry.StructureSheaf.germₗ R R inst✝⁴ inst✝⁴.toAddCommGroup Semiring.toModule U x hxU) (r • s)) =
    (ConcreteCategory.hom (toStalk R x)) ((RingHom.id R) r) *
      (Limits.colimit.isoColimitCocone
              {
                cocone :=
                  (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).mapCocone
                    (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
                isColimit :=
                  Limits.isColimitOfPreserves (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
                    (Limits.colimit.isColimit
                      ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }).addCommGroupIsoToAddEquiv.toFun
        ((ConcreteCategory.hom (germ (moduleStructurePresheaf R R).presheaf U x hxU)) s)