R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.244218
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
p : Ideal S
Hp : Ideal.IsPrime p
inst✝ : IsLocalization.AtPrime T p
⊢ ∀ (x : S), IsUnit x → x ∈ Ideal.primeCompl p
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.244218
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
p : Ideal S
Hp : Ideal.IsPrime p
inst✝ : IsLocalization.AtPrime T p
⊢ IsLocalization.AtPrime T (Ideal.comap (algebraMap R S) p)
apply localization_localization_isLocalization_of_has_all_units M p.primeCompl T
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.244218
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
p : Ideal S
Hp : Ideal.IsPrime p
inst✝ : IsLocalization.AtPrime T p
x : S
hx : IsUnit x
hx' : x ∈ ↑p
⊢ False
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.244218
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
p : Ideal S
Hp : Ideal.IsPrime p
inst✝ : IsLocalization.AtPrime T p
⊢ ∀ (x : S), IsUnit x → x ∈ Ideal.primeCompl p
intro x hx hx'
no goals
R : Type u_3
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.244218
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
p : Ideal S
Hp : Ideal.IsPrime p
inst✝ : IsLocalization.AtPrime T p
x : S
hx : IsUnit x
hx' : x ∈ ↑p
⊢ False
exact (Hp.1 : ¬_) (p.eq_top_of_isUnit_mem hx' hx)