-- Mathlib/RingTheory/LocalProperties/Basic.lean
lemma RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway
    (hPc : RingHom.StableUnderComposition P) (hPl : HoldsForLocalizationAway P) :
    StableUnderCompositionWithLocalizationAway P

Proof state:
case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R✝ S T : Type u
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
s : S
inst✝ : IsLocalization.Away s T
f : R✝ →+* S
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S T).comp f)

Tactic:
exact hPc _ _ hf (hPl T s)

Result:
no goals

Proof state:
case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
⊢ StableUnderCompositionWithLocalizationAwayTarget
    fun {R S} [CommRing R] [CommRing S] {R S} [CommRing R] [CommRing S] => P

Tactic:
introv _ _ hf

Result:
case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R✝ S T : Type u
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
s : S
inst✝ : IsLocalization.Away s T
f : R✝ →+* S
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S T).comp f)

Proof state:
case left
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
⊢ StableUnderCompositionWithLocalizationAwaySource
    fun {R S} [CommRing R] [CommRing S] {R S} [CommRing R] [CommRing S] => P

Tactic:
introv _ _ hf

Result:
case left
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R✝ S T : Type u
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R✝ S
r : R✝
inst✝ : IsLocalization.Away r S
f : S →+* T
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (f.comp (algebraMap R✝ S))

Proof state:
case left
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
R✝ S T : Type u
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R✝ S
r : R✝
inst✝ : IsLocalization.Away r S
f : S →+* T
hf : (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ (fun {R S} [CommRing R] [CommRing S] => P) (f.comp (algebraMap R✝ S))

Tactic:
exact hPc _ _ (hPl S r) hf

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
⊢ StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] => P

Tactic:
constructor

Result:
case left
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
⊢ StableUnderCompositionWithLocalizationAwaySource
    fun {R S} [CommRing R] [CommRing S] {R S} [CommRing R] [CommRing S] => P

case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
⊢ StableUnderCompositionWithLocalizationAwayTarget
    fun {R S} [CommRing R] [CommRing S] {R S} [CommRing R] [CommRing S] => P