-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u
inst_1 : CommRing S
P : Type u
inst_2 : CommRing P
f : R →+* S
g : S →+* P
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
W : Opens (↑(PrimeSpectrum.Top P) : Type u)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
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 W))
rw :
  Eq (α := Localizations P (↑p : (↑(PrimeSpectrum.Top P) : Type u)))
    ((RingHom.comp (β := Localization.AtPrime (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal)
            (Localization.localRingHom (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal
              (↑p : (↑(PrimeSpectrum.Top P) : Type u)).asIdeal g ⋯)
            (Localization.localRingHom (PrimeSpectrum.comap (g.comp f) (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal
              (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal f ⋯) :
          (a : Localization.AtPrime (PrimeSpectrum.comap (g.comp f) (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal) →
            Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top P) : Type u)).asIdeal)
        ((↑s : (x : ↥(unop (op U))) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U))
            (PrimeSpectrum.comap (g.comp f) (↑p : (↑(PrimeSpectrum.Top P) : Type u))) ⋯)) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top P) : Type u)).asIdeal)
    ((↑(((comap g V W hVW).comp (comap f U V hUV) :
                (a : (↑((structureSheaf R).obj.obj (op U)) : Type u)) → (↑((structureSheaf P).obj.obj (op W)) : Type u))
              s) :
          (x : ↥(unop (op W))) → Localizations P (↑x : (↑(PrimeSpectrum.Top P) : Type u)))
        p :
      Localizations P (↑p : (↑(PrimeSpectrum.Top P) : Type u)))
hIJ :
  (PrimeSpectrum.comap (g.comp f) (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal =
    Ideal.comap f (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal
⊢ Eq.{u + 1} (α := Localizations P (↑p : (↑(PrimeSpectrum.Top P) : Type u)))
    ((↑((comap (g.comp f) U W ⋯ :
              (a : (↑((structureSheaf R).obj.obj (op U)) : Type u)) → (↑((structureSheaf P).obj.obj (op W)) : Type u))
            s) :
        (x : ↥(unop (op W))) → Localizations P (↑x : (↑(PrimeSpectrum.Top P) : Type u)))
      p)
    ((↑(((comap g V W hVW).comp (comap f U V hUV) :
              (a : (↑((structureSheaf R).obj.obj (op U)) : Type u)) → (↑((structureSheaf P).obj.obj (op W)) : Type u))
            s) :
        (x : ↥(unop (op W))) → Localizations P (↑x : (↑(PrimeSpectrum.Top P) : Type u)))
      p)
have hJK : (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal =
  Ideal.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u)).asIdeal
Tactic: rw [comap_apply, Localization.localRingHom_comp _ (PrimeSpectrum.comap g p.1).asIdeal]