-- 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
rw :
  Eq (α := (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((ModuleCat.Hom.hom
            (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 (basicOpen (↑s : R)))))
              (ModuleCat.ofHom (toOpenₗ R M (basicOpen (↑s : R))))
              (Presheaf.germ (structurePresheafInModuleCat R M) (basicOpen (↑s : R)) x ⋯)) :
          (a : M) → (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        f :
      (↑(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))
⊢ 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))

Tactic:
rw [← map_smul, LocalizedModule.smul'_mk, ← Submonoid.smul_def, LocalizedModule.mk_cancel,
    ← LocalizedModule.mkLinearMap_apply, IsLocalizedModule.lift_apply, ← map_smul,
    ← toOpenₗ_germ (basicOpen ↑s) _ s.2, smul_const]

Premises used: PrimeSpectrum.basicOpen, LocalizedModule.mk_cancel, AlgebraicGeometry.StructureSheaf.smul_const, _private.0.AlgebraicGeometry.StructureSheaf.toOpenₗ_germ, LocalizedModule.smul'_mk, Submonoid.smul_def, IsLocalizedModule.lift_apply, LocalizedModule.mkLinearMap_apply, map_smul