-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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))
⊢ (↑((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)
have simp : (Localization.localRingHom (Ideal.comap f (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
        (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal f sorry :
      (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))) sorry)) =
  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 sorry :
          (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))) sorry)) :
      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 sorry :
          (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))) sorry)) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top S) : Type u)).asIdeal)
Tactic: simp only [comapₗ_eq_localRingHom, PrimeSpectrum.comap_asIdeal]