-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
S : Type u
inst_1 : CommRing S
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
s_1 :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (op U)) :
    Type u)
p : ↥V
m : R
s : ↥(PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal.primeCompl
trans :
  Eq (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localizations.comapFun f.toSemilinearMap (↑p : (↑(PrimeSpectrum.Top S) : Type u)) :
          (a : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))) →
            Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
        (LocalizedModule.mk m s) :
      Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    (LocalizedModule.mk ((f : (a : R) → S) m)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
          ((f : (a : R) → S) (↑s : R)) ⋯) :
      LocalizedModule (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl S)
trans₁ :
  Eq (α := LocalizedModule (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl S)
    (LocalizedModule.mk ((f : (a : R) → S) m)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
          ((f : (a : R) → S) (↑s : R)) ⋯) :
      LocalizedModule (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl S)
    ((Localization.localRingHom (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal
            (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
          (a : Localization.AtPrime (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal) →
            Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
        (LocalizedModule.mk m s) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
⊢ Eq (α := Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localizations.comapFun f.toSemilinearMap (↑p : (↑(PrimeSpectrum.Top S) : Type u)) :
          (a : Localizations R (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)))) →
            Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
        (LocalizedModule.mk m s) :
      Localizations S (↑p : (↑(PrimeSpectrum.Top S) : Type u)))
    ((Localization.localRingHom (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal
            (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f ⋯ :
          (a : Localization.AtPrime (PrimeSpectrum.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u))).asIdeal) →
            Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
        (LocalizedModule.mk m s) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)

Tactic:
trans LocalizedModule.mk (f m) ⟨f ↑s, s.2⟩

Premises used: LocalizedModule.mk, Subtype.mk, Subtype.val, DFunLike.coe