-- Mathlib/RingTheory/Localization/Away/Basic.lean
/-- If `S₁` is the localization of `R` away from `f` and `S₂` is the localization away from `g`,
then any localization `T` of `S₂` away from `f` is also a localization of `S₁` away from `g`. -/
lemma commutes {R : Type*} [CommSemiring R] (S₁ S₂ T : Type*) [CommSemiring S₁]
    [CommSemiring S₂] [CommSemiring T] [Algebra R S₁] [Algebra R S₂] [Algebra R T] [Algebra S₁ T]
    [Algebra S₂ T] [IsScalarTower R S₁ T] [IsScalarTower R S₂ T] (x y : R)
    [IsLocalization.Away x S₁] [IsLocalization.Away y S₂]
    [IsLocalization.Away (algebraMap R S₂ x) T] :
    IsLocalization.Away (algebraMap R S₁ y) T

Proof state:
case h.e.h.e'_3.h
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x y : R
inst✝² : Away x S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x) T
this : IsLocalization (Algebra.algebraMapSubmonoid S₂ (Submonoid.powers x)) T
⊢ Submonoid.powers ((algebraMap R S₁) y) = Algebra.algebraMapSubmonoid S₁ (Submonoid.powers y)

Tactic:
ext x

Result:
case h.e.h.e'_3.h.h
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x✝ y : R
inst✝² : Away x✝ S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x✝) T
this : IsLocalization (Algebra.algebraMapSubmonoid S₂ (Submonoid.powers x✝)) T
x : S₁
⊢ x ∈ Submonoid.powers ((algebraMap R S₁) y) ↔ x ∈ Algebra.algebraMapSubmonoid S₁ (Submonoid.powers y)

Proof state:
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x y : R
inst✝² : Away x S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x) T
⊢ IsLocalization (Algebra.algebraMapSubmonoid S₂ (Submonoid.powers x)) T

Tactic:
simp only [Algebra.algebraMapSubmonoid, Submonoid.map_powers]

Result:
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x y : R
inst✝² : Away x S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x) T
⊢ IsLocalization (Submonoid.powers ((algebraMap R S₂) x)) T

Proof state:
case h.e.h.e'_3.h.h
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x✝ y : R
inst✝² : Away x✝ S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x✝) T
this : IsLocalization (Algebra.algebraMapSubmonoid S₂ (Submonoid.powers x✝)) T
x : S₁
⊢ x ∈ Submonoid.powers ((algebraMap R S₁) y) ↔ x ∈ Algebra.algebraMapSubmonoid S₁ (Submonoid.powers y)

Tactic:
simp [Algebra.algebraMapSubmonoid]

Result:
no goals

Proof state:
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x y : R
inst✝² : Away x S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x) T
⊢ IsLocalization (Submonoid.powers ((algebraMap R S₂) x)) T

Tactic:
infer_instance

Result:
no goals

Proof state:
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x y : R
inst✝² : Away x S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x) T
this : IsLocalization (Algebra.algebraMapSubmonoid S₂ (Submonoid.powers x)) T
⊢ Away ((algebraMap R S₁) y) T

Tactic:
convert IsLocalization.commutes S₁ S₂ T (Submonoid.powers x) (Submonoid.powers y)

Result:
case h.e.h.e'_3.h
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x y : R
inst✝² : Away x S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x) T
this : IsLocalization (Algebra.algebraMapSubmonoid S₂ (Submonoid.powers x)) T
⊢ Submonoid.powers ((algebraMap R S₁) y) = Algebra.algebraMapSubmonoid S₁ (Submonoid.powers y)

Proof state:
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x y : R
inst✝² : Away x S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x) T
⊢ Away ((algebraMap R S₁) y) T

Tactic:
haveI : IsLocalization (Algebra.algebraMapSubmonoid S₂ (Submonoid.powers x)) T := by
  simp only [Algebra.algebraMapSubmonoid, Submonoid.map_powers]
  infer_instance

Result:
R : Type u_5
inst✝¹³ : CommSemiring R
S₁ : Type u_6
S₂ : Type u_7
T : Type u_8
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
x y : R
inst✝² : Away x S₁
inst✝¹ : Away y S₂
inst✝ : Away ((algebraMap R S₂) x) T
this : IsLocalization (Algebra.algebraMapSubmonoid S₂ (Submonoid.powers x)) T
⊢ Away ((algebraMap R S₁) y) T