-- Mathlib/RingTheory/LocalProperties/Basic.lean
/-- If `P` is stable under base change and holds for `f`, then `P` holds for `f` localized
at any submonoid `M` of `R`. -/
lemma RingHom.IsStableUnderBaseChange.isLocalization_map (M : Submonoid R) [IsLocalization M Rᵣ]
    (f : R →+* S) [IsLocalization (M.map f) Sᵣ] (hf : P f) :
    P (IsLocalization.map Sᵣ f M.le_comap_map : Rᵣ →+* Sᵣ)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
⊢ P (IsLocalization.map Sᵣ f ⋯)

Tactic:
algebraize [f, IsLocalization.map (S := Rᵣ) Sᵣ f M.le_comap_map,
  (IsLocalization.map (S := Rᵣ) Sᵣ f M.le_comap_map).comp (algebraMap R Rᵣ)]

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rᵣ Sᵣ := (IsLocalization.map Sᵣ f ⋯).toAlgebra
algInst✝ : Algebra R Sᵣ := ((IsLocalization.map Sᵣ f ⋯).comp (algebraMap R Rᵣ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rᵣ Sᵣ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sᵣ))
⊢ P (IsLocalization.map Sᵣ f ⋯)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rᵣ Sᵣ := (IsLocalization.map Sᵣ f ⋯).toAlgebra
algInst✝ : Algebra R Sᵣ := ((IsLocalization.map Sᵣ f ⋯).comp (algebraMap R Rᵣ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rᵣ Sᵣ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sᵣ))
⊢ P (IsLocalization.map Sᵣ f ⋯)

Tactic:
haveI : IsScalarTower R S Sᵣ := IsScalarTower.of_algebraMap_eq'
  (IsLocalization.map_comp M.le_comap_map)

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rᵣ Sᵣ := (IsLocalization.map Sᵣ f ⋯).toAlgebra
algInst✝ : Algebra R Sᵣ := ((IsLocalization.map Sᵣ f ⋯).comp (algebraMap R Rᵣ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rᵣ Sᵣ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sᵣ))
this : IsScalarTower R S Sᵣ
⊢ P (IsLocalization.map Sᵣ f ⋯)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rᵣ Sᵣ := (IsLocalization.map Sᵣ f ⋯).toAlgebra
algInst✝ : Algebra R Sᵣ := ((IsLocalization.map Sᵣ f ⋯).comp (algebraMap R Rᵣ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rᵣ Sᵣ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sᵣ))
this✝ : IsScalarTower R S Sᵣ
this : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ
⊢ P (IsLocalization.map Sᵣ f ⋯)

Tactic:
apply hP.of_isLocalization M hf

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rᵣ Sᵣ := (IsLocalization.map Sᵣ f ⋯).toAlgebra
algInst✝ : Algebra R Sᵣ := ((IsLocalization.map Sᵣ f ⋯).comp (algebraMap R Rᵣ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rᵣ Sᵣ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sᵣ))
this : IsScalarTower R S Sᵣ
⊢ P (IsLocalization.map Sᵣ f ⋯)

Tactic:
haveI : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ :=
  inferInstanceAs <| IsLocalization (M.map f) Sᵣ

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra Rᵣ Sᵣ := (IsLocalization.map Sᵣ f ⋯).toAlgebra
algInst✝ : Algebra R Sᵣ := ((IsLocalization.map Sᵣ f ⋯).comp (algebraMap R Rᵣ)).toAlgebra
scalarTowerInst✝ : IsScalarTower R Rᵣ Sᵣ := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R Sᵣ))
this✝ : IsScalarTower R S Sᵣ
this : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ
⊢ P (IsLocalization.map Sᵣ f ⋯)