case intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3304
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
a : R
ha : a ∈ ↑M
⊢ ↑(algebraMap R S) a ∈ IsUnit.submonoid S
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3304
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
⊢ Submonoid.map (algebraMap R S) M ≤ IsUnit.submonoid S
rintro _ ⟨a, ha, rfl⟩
no goals
case intro.intro
R : Type u_2
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.3304
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
a : R
ha : a ∈ ↑M
⊢ ↑(algebraMap R S) a ∈ IsUnit.submonoid S
exact IsLocalization.map_units S ⟨_, ha⟩