-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
S_1 : Type u
inst_5 : CommRing S_1
N : Type u
inst_6 : AddCommGroup N
inst_7 : Module S_1 N
σ : R →+* S_1
f_1 : M →ₛₗ[σ] N
S : Type u
inst_8 : CommRing S
P : Type u
inst_9 : CommRing P
f : R →+* S
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
r s :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (op U)) :
    Type u)
p : ↥(unop (op V))
⊢ (↑(AddHom.toFun (LinearMap.toAddHom (comapₗ f.toSemilinearMap U V hUV)) (r * s)) :
        (x : ↥(unop (op V))) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      p =
    (↑(HMul.hMul (α :=
            (↑(Functor.obj
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top S) : Type u)))
                    (structureSheaf S))
                  (op V)) :
              Type u))
            (AddHom.toFun (LinearMap.toAddHom (comapₗ f.toSemilinearMap U V hUV)) r)
            (AddHom.toFun (LinearMap.toAddHom (comapₗ f.toSemilinearMap U V hUV)) s)) :
        (x : ↥(unop (op V))) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      p
have dsimp : (↑((comapₗ f.toSemilinearMap U V hUV :
            (a : (structureSheafInType R R).obj.obj (op U)) → (structureSheafInType S S).obj.obj (op V))
          (r * s)) :
      (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    p =
  (↑(HMul.hMul (α :=
          (↑(Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top S) : Type u)))
                  (structureSheaf S))
                (op V)) :
            Type u))
          (β :=
          (↑(Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top S) : Type u)))
                  (structureSheaf S))
                (op V)) :
            Type u))
          ((comapₗ f.toSemilinearMap U V hUV :
                (a : (structureSheafInType R R).obj.obj (op U)) → (structureSheafInType S S).obj.obj (op V))
              r :
            Functor.obj
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top S) : Type u)))
                (structureSheafInType S S))
              (op V))
          ((comapₗ f.toSemilinearMap U V hUV :
                (a : (structureSheafInType R R).obj.obj (op U)) → (structureSheafInType S S).obj.obj (op V))
              s :
            Functor.obj
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top S) : Type u)))
                (structureSheafInType S S))
              (op V))) :
      (x : ↥V) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    p
Tactic: dsimp