-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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))
change :
  (↑((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 (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
      ((↑((comapₗ f.toSemilinearMap U V hUV :
                (a : (structureSheafInType R R).obj.obj (op U)) → (structureSheafInType S S).obj.obj (op V))
              r) :
          (x : ↥(unop (op V))) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
        p)
      ((↑((comapₗ f.toSemilinearMap U V hUV :
                (a : (structureSheafInType R R).obj.obj (op U)) → (structureSheafInType S S).obj.obj (op V))
              s) :
          (x : ↥(unop (op V))) → Localizations S (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
        p)
⊢ (↑((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:
change _ = (comapₗ f.toSemilinearMap U V hUV r).1 p * (comapₗ f.toSemilinearMap U V hUV s).1 p

Premises used: AlgebraicGeometry.StructureSheaf.comapₗ, Subtype.val, RingHom.toSemilinearMap, DFunLike.coe