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

Tactic:
haveI : IsLocalization.Away (algebraMap S (Localization.Away a) t)
    (Localization.Away (algebraMap S T a)) :=
  IsLocalization.Away.commutes _ T ((Localization.Away (algebraMap S T a))) a t

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

Proof state:
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))

Tactic:
rintro - ⟨a, ha, rfl⟩

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
⊢ P ((algebraMap T (Localization.Away ((algebraMap S T) a))).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
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 :
  ∃ s,
    ∃ (_ : Ideal.span ↑s = ⊤),
      ∀ 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:
obtain ⟨s, hsone, hs⟩ := hf

Result:
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)