-- 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
dsimp :
  HSMul.hSMul (β := (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) (↑s : R)
      ((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 f s) :
        (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) =
    HSMul.hSMul (β := (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) (↑s : R)
      ((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 f (↑s : R) (basicOpen (↑s : R)) ⋯) :
        (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
⊢ Eq (α := (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((((algebraMap R (Module.End R (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
                (a : R) → Module.End R (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
              (↑s : R) :
            Module.End R (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
          (a : (↑((structurePresheafInModuleCat R M).stalk x) : 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 := ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))
                (localizationtoStalkₗ R M x) :
              (a : (↑(ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)) : Type u)) →
                (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
            (LocalizedModule.mk f s) :
          (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
      (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((((algebraMap R (Module.End R (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
                (a : R) → Module.End R (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
              (↑s : R) :
            Module.End R (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
          (a : (↑((structurePresheafInModuleCat R M).stalk x) : 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 (basicOpen (↑s : R)))) (Y :=
                Presheaf.stalk (structurePresheafInModuleCat R M) x)
                (Presheaf.germ (structurePresheafInModuleCat R M) (basicOpen (↑s : R)) x ⋯) :
              (a : (↑((structurePresheafInModuleCat R M).obj (op (basicOpen (↑s : R)))) : Type u)) →
                (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
            (const f (↑s : R) (basicOpen (↑s : R)) ⋯) :
          (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
      (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))

Tactic:
dsimp [localizationtoStalkₗ]

Premises used: _private.0.AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ