-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u
inst_3 : CommRing S
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
hs_1 :
  PrelocalPredicate.pred (T := Localizations M)
    (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) s
this_1 : Module R N := Module.compHom N σ
this_2 : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
p : (↑(PrimeSpectrum.Top S) : Type u)
hpV : p ∈ V
W : Opens (↑(PrimeSpectrum.Top R) : Type u)
m :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ p) ⋯) :
      (↑(PrimeSpectrum.Top R) : Type u)) ∈
    W
iWU : W ⟶ U
a : M
b : R
h_frac :
  ∀ (x : ↥W),
    ∃ (hs : b ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
      Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        ((fun (x : ↥W) ↦
            (s ((iWU : (a : ↥W) → ↥U) x) :
              Localizations (R := R) M (↑((iWU : (a : ↥W) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x)
        (LocalizedModule.mk a
          (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) b hs))
q : (↑(PrimeSpectrum.Top S) : Type u)
hqW :
  q ∈
    (↑{ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ : Opens (↑(PrimeSpectrum.Top S) : Type u) } :
      Set (↑(PrimeSpectrum.Top S) : Type u))
hqV : q ∈ (↑V : Set (↑(PrimeSpectrum.Top S) : Type u))
hs :
  b ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (PrimeSpectrum.comap σ q) hqW) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal
H :
  Eq (α :=
    Localizations M
      (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (PrimeSpectrum.comap σ q) hqW) :
        (↑(PrimeSpectrum.Top R) : Type u)))
    ((fun (x : ↥W) ↦
        (s ((iWU : (a : ↥W) → ↥U) x) :
          Localizations (R := R) M (↑((iWU : (a : ↥W) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
      (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (PrimeSpectrum.comap σ q) hqW))
    (LocalizedModule.mk a
      (Subtype.mk (p := fun (x : R) ↦
        x ∈
          (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (PrimeSpectrum.comap σ q) hqW) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        b hs))
⊢ Eq (α :=
    Localizations N
      (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦
            x ∈
              { carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                  Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
                V)
            q ⋯) :
        (↑(PrimeSpectrum.Top S) : Type u)))
    ((fun
            (x :
              ↥({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                    Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
                  V)) ↦
          (comapFun f U V hUV s
              (({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                        Opens (↑(PrimeSpectrum.Top S) : Type u) }.infLERight
                    V :
                  (a : ↥({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ } ⊓ V)) → ↥V)
                x) :
            Localizations (R := S) N
              (↑(({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                            Opens (↑(PrimeSpectrum.Top S) : Type u) }.infLERight
                        V :
                      (a : ↥({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ } ⊓ V)) → ↥V)
                    x) :
                (↑(PrimeSpectrum.Top S) : Type u))))
        (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦
          x ∈
            { carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
              V)
          q ⋯) :
      Localizations (R := S) N
        (↑(({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                      Opens (↑(PrimeSpectrum.Top S) : Type u) }.infLERight
                  V :
                (a : ↥({ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ } ⊓ V)) → ↥V)
              (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦
                x ∈
                  { carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                      Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
                    V)
                q ⋯)) :
          (↑(PrimeSpectrum.Top S) : Type u)))
    (LocalizedModule.mk ((f : (a : M) → N) a)
        (Subtype.mk (p := fun (x : S) ↦
          x ∈
            (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦
                      x ∈
                        { carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                            Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
                          V)
                      q ⋯) :
                  (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl)
          ((σ : (a : R) → S) b) hs) :
      LocalizedModule
        (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦
                  x ∈
                    { carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ :
                        Opens (↑(PrimeSpectrum.Top S) : Type u) } ⊓
                      V)
                  q ⋯) :
              (↑(PrimeSpectrum.Top S) : Type u)).asIdeal.primeCompl
        N)
have dsimp : Eq (α := Localizations N q)
  ((Localizations.comapFun f q : (a : Localizations M (PrimeSpectrum.comap σ q)) → Localizations N q)
      (s (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ q) sorry)) :
    Localizations N q)
  (LocalizedModule.mk ((f : (a : M) → N) a)
      (Subtype.mk (p := fun (x : S) ↦ x ∈ q.asIdeal.primeCompl) ((σ : (a : R) → S) b) hs) :
    LocalizedModule q.asIdeal.primeCompl N)
Tactic: dsimp [comapFun] at H ⊢