-- Mathlib/RingTheory/RingHom/Locally.lean
/-- If `P` is stable under composition with localization away maps on the right,
then so is `Locally P`. -/
lemma locally_StableUnderCompositionWithLocalizationAwayTarget
    (hP0 : RespectsIso P)
    (hPa : StableUnderCompositionWithLocalizationAwayTarget P) :
    StableUnderCompositionWithLocalizationAwayTarget (Locally P)

Proof state:
case intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP0 : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPa : StableUnderCompositionWithLocalizationAwayTarget 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
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S T).comp f)

Tactic:
refine ⟨algebraMap S T '' s, ?_, ?_⟩

Result:
case intro.intro.refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP0 : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPa : StableUnderCompositionWithLocalizationAwayTarget 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
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
⊢ Ideal.span (⇑(algebraMap S T) '' ↑s) = ⊤

case intro.intro.refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP0 : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPa : StableUnderCompositionWithLocalizationAwayTarget 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
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
⊢ ∀ t ∈ ⇑(algebraMap S T) '' ↑s,
    (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp ((algebraMap S T).comp f))

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP0 : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] => P
⊢ StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] =>
    Locally fun {R S} [CommRing R] [CommRing S] => P

Tactic:
intro R S T _ _ _ _ t _ f hf

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP0 : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPa : StableUnderCompositionWithLocalizationAwayTarget 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
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
hf : Locally (fun {R S} [CommRing R] [CommRing S] => P) f
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S T).comp f)

Proof state:
case intro.intro.refine_2.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP0 : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPa : StableUnderCompositionWithLocalizationAwayTarget 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
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
a : S
ha : a ∈ ↑s
this✝ : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
  (IsLocalization.Away.map (Localization.Away a) (Localization.Away ((algebraMap S T) a)) (algebraMap S T) a).toAlgebra
this :
  (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)
⊢ P ((algebraMap T (Localization.Away ((algebraMap S T) a))).comp ((algebraMap S T).comp f))

Tactic:
rw [← comp_assoc, ← this, comp_assoc]

Result:
case intro.intro.refine_2.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP0 : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPa : StableUnderCompositionWithLocalizationAwayTarget 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
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
a : S
ha : a ∈ ↑s
this✝ : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
  (IsLocalization.Away.map (Localization.Away a) (Localization.Away ((algebraMap S T) a)) (algebraMap S T) a).toAlgebra
this :
  (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)
⊢ P
    ((algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      ((algebraMap S (Localization.Away a)).comp f))