-- 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))
simp :
  (Localization.localRingHom (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
          (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
        (a : Localization.AtPrime (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)) →
          Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
      ((↑(r * s) : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
          (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) =
    HMul.hMul (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u))) (β :=
      Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
      ((Localization.localRingHom (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
              (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
            (a : Localization.AtPrime (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)) →
              Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
          ((↑r : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
              (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) :
        Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
      ((Localization.localRingHom (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
              (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
            (a : Localization.AtPrime (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)) →
              Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
          ((↑s : (x : ↥U) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
            (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
              (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))) ⋯)) :
        Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
⊢ (↑((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)

Tactic:
simp only [comapₗ_eq_localRingHom, PrimeSpectrum.comap_asIdeal]

Premises used: PrimeSpectrum.comap_asIdeal, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom