-- Mathlib/RingTheory/LocalProperties/Basic.lean
lemma RingHom.PropertyIsLocal.HoldsForLocalizationAway (hP : RingHom.PropertyIsLocal @P)
    (hPi : ContainsIdentities P) :
    RingHom.HoldsForLocalizationAway @P

Proof state:
case a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : algebraMap R S = (algebraMap R S).comp (id R)
⊢ P (id R)

Tactic:
apply hPi

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ algebraMap R S = (algebraMap R S).comp (id R)

Tactic:
simp

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ P (algebraMap R S)

Tactic:
have : algebraMap R S = (algebraMap R S).comp (RingHom.id R) := by simp

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : algebraMap R S = (algebraMap R S).comp (id R)
⊢ P (algebraMap R S)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P
⊢ RingHom.HoldsForLocalizationAway P

Tactic:
introv R _

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ P (algebraMap R S)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : algebraMap R S = (algebraMap R S).comp (id R)
⊢ P ((algebraMap R S).comp (id R))

Tactic:
apply hP.StableUnderCompositionWithLocalizationAwayTarget S r

Result:
case a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : algebraMap R S = (algebraMap R S).comp (id R)
⊢ P (id R)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : algebraMap R S = (algebraMap R S).comp (id R)
⊢ P (algebraMap R S)

Tactic:
rw [this]

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal P
hPi : ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
this : algebraMap R S = (algebraMap R S).comp (id R)
⊢ P ((algebraMap R S).comp (id R))