-- Mathlib/AlgebraicGeometry/Spec.lean
theorem isLocalizedModule_toPushforwardStalkAlgHom_aux (y) :
    ∃ x : S × p.asIdeal.primeCompl, x.2 • y = toPushforwardStalkAlgHom R S p x.1

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).val).stalk
      p)
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).val).obj
      (op (PrimeSpectrum.basicOpen r)))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).val).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
        ↑(s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 =
    (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
      (s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1
⊢ (ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).val).germ
            (PrimeSpectrum.basicOpen r) p hpr))
        ((ConcreteCategory.hom
            (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                  (structureSheaf ↑S).val).map
              (homOfLE ⋯).op))
          ((ConcreteCategory.hom (toOpen ↑(CommRingCat.of ↑S) ⊤))
            ((ConcreteCategory.hom (CommRingCat.ofHom (algebraMap ↑R ↑S))) ↑(s, ⟨r, hpr⟩ ^ n).2))) *
      y =
    (toPushforwardStalkAlgHom R S p) (s, ⟨r, hpr⟩ ^ n).1

Tactic:
erw [← (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).germ_res_apply
  (homOfLE le_top) p hpr]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).val).stalk
      p)
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).val).obj
      (op (PrimeSpectrum.basicOpen r)))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).val).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
        ↑(s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 =
    (algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
      (s, ⟨(fun x => (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1
⊢ (ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).val).germ
            (PrimeSpectrum.basicOpen r) p hpr))
        ((ConcreteCategory.hom
            (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                  (structureSheaf ↑S).val).map
              (homOfLE ⋯).op))
          ((ConcreteCategory.hom (toOpen ↑(CommRingCat.of ↑S) ⊤))
            ((ConcreteCategory.hom (CommRingCat.ofHom (algebraMap ↑R ↑S))) ↑(s, ⟨r, hpr⟩ ^ n).2))) *
      y =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).val).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).val).map
            (homOfLE ⋯).op))
        ((toOpen ↑(CommRingCat.of ↑S) ⊤).hom' (s, ⟨r, hpr⟩ ^ n).1))

Proof state:
case intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).val).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).val).obj
      (op U))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).val).germ
          U p hp))
      s =
    y
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Tactic:
replace e :=
  ((Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).germ_res_apply
    (homOfLE hrU) p hpr _).trans e

Result:
case intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).val).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).val).obj
      (op U))
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).val).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).val).map
            (homOfLE hrU).op))
        s) =
    y
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Proof state:
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).val).stalk
      p)
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Tactic:
obtain ⟨U, hp, s, e⟩ := TopCat.Presheaf.germ_exist _ _ y

Result:
case intro.intro.intro
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).val).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).val).obj
      (op U))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).val).germ
          U p hp))
      s =
    y
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1