-- Mathlib/RingTheory/RingHom/Locally.lean
/-- If `P` is stable under base change, then so is `Locally P`. -/
lemma locally_isStableUnderBaseChange (hPi : RespectsIso P) (hPb : IsStableUnderBaseChange P) :
    IsStableUnderBaseChange (Locally P)

Proof state:
case intro.intro.refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPb : IsStableUnderBaseChange 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
inst✝ : Algebra R T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp (algebraMap R T))
this✝⁴ : (a : ↑s) → Algebra (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a) :=
  fun a => (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R T (Localization.Away ↑a))).toAlgebra
this✝³ : (a : ↑s) → Algebra T (S ⊗[R] Localization.Away ↑a) :=
  fun a => ((algebraMap (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)).comp (algebraMap T (S ⊗[R] T))).toAlgebra
this✝² : ∀ (a : ↑s), IsScalarTower T (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)
this✝¹ : ∀ (a : ↑s), IsScalarTower T (Localization.Away ↑a) (S ⊗[R] Localization.Away ↑a)
this✝ : ∀ (a : ↑s), IsScalarTower S (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)
this : ∀ (a : ↑s), Algebra.IsPushout T (Localization.Away ↑a) (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)
a : ↑s
⊢ IsLocalization (Algebra.algebraMapSubmonoid (S ⊗[R] T) (Submonoid.powers ↑a)) (S ⊗[R] Localization.Away ↑a)

Tactic:
rw [← isLocalizedModule_iff_isLocalization, isLocalizedModule_iff_isBaseChange
  (S := Submonoid.powers a.val) (A := Localization.Away a.val)]

Result:
case intro.intro.refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPb : IsStableUnderBaseChange 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
inst✝ : Algebra R T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp (algebraMap R T))
this✝⁴ : (a : ↑s) → Algebra (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a) :=
  fun a => (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R T (Localization.Away ↑a))).toAlgebra
this✝³ : (a : ↑s) → Algebra T (S ⊗[R] Localization.Away ↑a) :=
  fun a => ((algebraMap (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)).comp (algebraMap T (S ⊗[R] T))).toAlgebra
this✝² : ∀ (a : ↑s), IsScalarTower T (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)
this✝¹ : ∀ (a : ↑s), IsScalarTower T (Localization.Away ↑a) (S ⊗[R] Localization.Away ↑a)
this✝ : ∀ (a : ↑s), IsScalarTower S (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)
this : ∀ (a : ↑s), Algebra.IsPushout T (Localization.Away ↑a) (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)
a : ↑s
⊢ IsBaseChange (Localization.Away ↑a) (IsScalarTower.toAlgHom T (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)).toLinearMap

Proof state:
case intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPb : IsStableUnderBaseChange 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
inst✝ : Algebra R T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp (algebraMap R T))
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) Algebra.TensorProduct.includeLeftRingHom

Tactic:
rw [locally_iff_exists hPi]

Result:
case intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPb : IsStableUnderBaseChange 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
inst✝ : Algebra R T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp (algebraMap R T))
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
          ∀ (i : ι), P ((algebraMap (S ⊗[R] T) (Sₜ i)).comp Algebra.TensorProduct.includeLeftRingHom)

Proof state:
case intro.intro.refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPb : IsStableUnderBaseChange 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
inst✝ : Algebra R T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp (algebraMap R T))
this✝⁵ : (a : ↑s) → Algebra (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a) :=
  fun a => (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R T (Localization.Away ↑a))).toAlgebra
this✝⁴ : (a : ↑s) → Algebra T (S ⊗[R] Localization.Away ↑a) :=
  fun a => ((algebraMap (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)).comp (algebraMap T (S ⊗[R] T))).toAlgebra
this✝³ : ∀ (a : ↑s), IsScalarTower T (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)
this✝² : ∀ (a : ↑s), IsScalarTower T (Localization.Away ↑a) (S ⊗[R] Localization.Away ↑a)
this✝¹ : ∀ (a : ↑s), IsScalarTower S (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)
this✝ : ∀ (a : ↑s), Algebra.IsPushout T (Localization.Away ↑a) (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)
a : ↑s
this :
  (algebraMap (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)).comp Algebra.TensorProduct.includeLeftRingHom =
    Algebra.TensorProduct.includeLeftRingHom
⊢ P ((algebraMap (S ⊗[R] T) ((fun a => S ⊗[R] Localization.Away ↑a) a)).comp Algebra.TensorProduct.includeLeftRingHom)

Tactic:
rw [this]

Result:
case intro.intro.refine_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPb : IsStableUnderBaseChange 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
inst✝ : Algebra R T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp (algebraMap R T))
this✝⁵ : (a : ↑s) → Algebra (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a) :=
  fun a => (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R T (Localization.Away ↑a))).toAlgebra
this✝⁴ : (a : ↑s) → Algebra T (S ⊗[R] Localization.Away ↑a) :=
  fun a => ((algebraMap (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)).comp (algebraMap T (S ⊗[R] T))).toAlgebra
this✝³ : ∀ (a : ↑s), IsScalarTower T (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)
this✝² : ∀ (a : ↑s), IsScalarTower T (Localization.Away ↑a) (S ⊗[R] Localization.Away ↑a)
this✝¹ : ∀ (a : ↑s), IsScalarTower S (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)
this✝ : ∀ (a : ↑s), Algebra.IsPushout T (Localization.Away ↑a) (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)
a : ↑s
this :
  (algebraMap (S ⊗[R] T) (S ⊗[R] Localization.Away ↑a)).comp Algebra.TensorProduct.includeLeftRingHom =
    Algebra.TensorProduct.includeLeftRingHom
⊢ P Algebra.TensorProduct.includeLeftRingHom