-- 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.refine_2.intro.intro.a
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)
this✝ : IsScalarTower S (Localization.Away a) (Localization.Away ((algebraMap S T) a))
this : IsLocalization.Away ((algebraMap S (Localization.Away a)) t) (Localization.Away ((algebraMap S T) a))
⊢ P ((algebraMap S (Localization.Away a)).comp f)

Tactic:
apply hs a ha

Result:
no goals

Proof state:
case h
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)
x : S
⊢ (algebraMap S (Localization.Away ((algebraMap S T) a))) x =
    (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))) ((algebraMap S (Localization.Away a)) x)

Tactic:
simp [algebraMap_toAlgebra, IsLocalization.Away.map, ← IsScalarTower.algebraMap_apply]

Result:
no goals

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
⊢ P ((algebraMap T (Localization.Away ((algebraMap S T) a))).comp ((algebraMap S T).comp f))

Tactic:
have : (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) := by
  simp [algebraMap_toAlgebra, IsLocalization.Away.map]

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 T (Localization.Away ((algebraMap S T) a))).comp ((algebraMap S T).comp f))