-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
lemma stalkwise {P} (hP : RingHom.RespectsIso P) :
    HasRingHomProperty (stalkwise P) fun {_ S _ _} φ ↦
      ∀ (p : Ideal S) (_ : p.IsPrime), P (Localization.localRingHom _ p φ rfl)

Proof state:
case h.e'_2.h.h.h.h.h.a
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso P
this✝ : IsLocalAtTarget (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
this : IsLocalAtSource (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
R S : Type u_1
x✝¹ : CommRing R
x✝ : CommRing S
φ : R →+* S
⊢ (∀ (p : Ideal S) (x : p.IsPrime), P (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)) ↔
    AlgebraicGeometry.stalkwise (fun {R S} [CommRing R] [CommRing S] => P) (Spec.map (CommRingCat.ofHom φ))

Tactic:
exact (stalkwise_Spec_map_iff hP (CommRingCat.ofHom φ)).symm

Result:
no goals

Proof state:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso P
this : IsLocalAtTarget (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
⊢ HasRingHomProperty (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P) fun {x S} {x_1} {x_2} φ =>
    ∀ (p : Ideal S) (x_3 : p.IsPrime), P (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)

Tactic:
have := stalkwise_isLocalAtSource_of_respectsIso hP

Result:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso P
this✝ : IsLocalAtTarget (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
this : IsLocalAtSource (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
⊢ HasRingHomProperty (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P) fun {x S} {x_1} {x_2} φ =>
    ∀ (p : Ideal S) (x_3 : p.IsPrime), P (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)

Proof state:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso P
⊢ HasRingHomProperty (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P) fun {x S} {x_1} {x_2} φ =>
    ∀ (p : Ideal S) (x_3 : p.IsPrime), P (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)

Tactic:
have := stalkwiseIsLocalAtTarget_of_respectsIso hP

Result:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso P
this : IsLocalAtTarget (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
⊢ HasRingHomProperty (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P) fun {x S} {x_1} {x_2} φ =>
    ∀ (p : Ideal S) (x_3 : p.IsPrime), P (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)

Proof state:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso P
this✝ : IsLocalAtTarget (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
this : IsLocalAtSource (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
⊢ HasRingHomProperty (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P) fun {x S} {x_1} {x_2} φ =>
    ∀ (p : Ideal S) (x_3 : p.IsPrime), P (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)

Tactic:
convert of_isLocalAtSource_of_isLocalAtTarget (P := AlgebraicGeometry.stalkwise P) with R S _ _ φ

Result:
case h.e'_2.h.h.h.h.h.a
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso P
this✝ : IsLocalAtTarget (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
this : IsLocalAtSource (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
R S : Type u_1
x✝¹ : CommRing R
x✝ : CommRing S
φ : R →+* S
⊢ (∀ (p : Ideal S) (x : p.IsPrime), P (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)) ↔
    AlgebraicGeometry.stalkwise (fun {R S} [CommRing R] [CommRing S] => P) (Spec.map (CommRingCat.ofHom φ))