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
m : ↑(Presheaf.stalk (moduleStructurePresheaf R M).presheaf 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)) }).addCommGroupIsoToAddEquiv.toFun
      (r • m) =
    (RingHom.id R) r •
      (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
        m

Tactic:
let α : TopCat.Presheaf.stalk (moduleStructurePresheaf R M).presheaf x ≅
      (forget₂ _ _).obj ((structurePresheafInModuleCat R M).stalk x) :=
      Limits.colimit.isoColimitCocone ⟨_, Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
      (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙
        structurePresheafInModuleCat R M))⟩

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
m : ↑(Presheaf.stalk (moduleStructurePresheaf R M).presheaf x)
α : 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)) }
⊢ (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
      (r • m) =
    (RingHom.id R) r •
      (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
        m