case intro.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.58093
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : { x // x ∈ localizationLocalizationSubmodule M N }
y' : { x // x ∈ N }
z : { x // x ∈ M }
eq : ↑(algebraMap R S) ↑y = ↑y' * ↑(algebraMap R S) ↑z
⊢ IsUnit (↑(algebraMap R T) ↑y)
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.58093
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : { x // x ∈ localizationLocalizationSubmodule M N }
⊢ IsUnit (↑(algebraMap R T) ↑y)
obtain ⟨y', z, eq⟩ := mem_localizationLocalizationSubmodule.mp y.prop
case intro.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.58093
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : { x // x ∈ localizationLocalizationSubmodule M N }
y' : { x // x ∈ N }
z : { x // x ∈ M }
eq : ↑(algebraMap R S) ↑y = ↑y' * ↑(algebraMap R S) ↑z
⊢ IsUnit (↑(algebraMap S T) ↑y') ∧ IsUnit (↑(algebraMap S T) (↑(algebraMap R S) ↑z))
case intro.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.58093
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : { x // x ∈ localizationLocalizationSubmodule M N }
y' : { x // x ∈ N }
z : { x // x ∈ M }
eq : ↑(algebraMap R S) ↑y = ↑y' * ↑(algebraMap R S) ↑z
⊢ IsUnit (↑(algebraMap R T) ↑y)
rw [IsScalarTower.algebraMap_apply R S T, eq, RingHom.map_mul, IsUnit.mul_iff]
no goals
case intro.intro
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.58093
inst✝⁶ : CommRing P
N : Submonoid S
T : Type u_2
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : { x // x ∈ localizationLocalizationSubmodule M N }
y' : { x // x ∈ N }
z : { x // x ∈ M }
eq : ↑(algebraMap R S) ↑y = ↑y' * ↑(algebraMap R S) ↑z
⊢ IsUnit (↑(algebraMap S T) ↑y') ∧ IsUnit (↑(algebraMap S T) (↑(algebraMap R S) ↑z))
exact ⟨IsLocalization.map_units T y', (IsLocalization.map_units _ z).map (algebraMap S T)⟩