R✝ : Type ?u.3191178
inst✝⁷ : CommRing R✝
M✝ : Submonoid R✝
S : Type ?u.3191370
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R✝ S
P : Type ?u.3191607
inst✝⁴ : CommRing P
R : Type u_1
Rₘ : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hM : ¬0 ∈ M
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := toField hR
⊢ Bijective ↑(algebraMap R Rₘ)
R✝ : Type ?u.3191178
inst✝⁷ : CommRing R✝
M✝ : Submonoid R✝
S : Type ?u.3191370
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R✝ S
P : Type ?u.3191607
inst✝⁴ : CommRing P
R : Type u_1
Rₘ : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hM : ¬0 ∈ M
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
⊢ Bijective ↑(algebraMap R Rₘ)
letI := hR.toField
R✝ : Type ?u.3191178
inst✝⁷ : CommRing R✝
M✝ : Submonoid R✝
S : Type ?u.3191370
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R✝ S
P : Type ?u.3191607
inst✝⁴ : CommRing P
R : Type u_1
Rₘ : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := toField hR
hM : M ≤ nonZeroDivisors R
⊢ Bijective ↑(algebraMap R Rₘ)
R✝ : Type ?u.3191178
inst✝⁷ : CommRing R✝
M✝ : Submonoid R✝
S : Type ?u.3191370
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R✝ S
P : Type ?u.3191607
inst✝⁴ : CommRing P
R : Type u_1
Rₘ : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hM : ¬0 ∈ M
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := toField hR
⊢ Bijective ↑(algebraMap R Rₘ)
replace hM := le_nonZeroDivisors_of_noZeroDivisors hM
R✝ : Type ?u.3191178
inst✝⁷ : CommRing R✝
M✝ : Submonoid R✝
S : Type ?u.3191370
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R✝ S
P : Type ?u.3191607
inst✝⁴ : CommRing P
R : Type u_1
Rₘ : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := toField hR
hM : M ≤ nonZeroDivisors R
x : Rₘ
⊢ ∃ a, ↑(algebraMap R Rₘ) a = x
R✝ : Type ?u.3191178
inst✝⁷ : CommRing R✝
M✝ : Submonoid R✝
S : Type ?u.3191370
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R✝ S
P : Type ?u.3191607
inst✝⁴ : CommRing P
R : Type u_1
Rₘ : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := toField hR
hM : M ≤ nonZeroDivisors R
⊢ Bijective ↑(algebraMap R Rₘ)
refine' ⟨IsLocalization.injective _ hM, fun x => _⟩
case intro.intro.mk
R✝ : Type ?u.3191178
inst✝⁷ : CommRing R✝
M✝ : Submonoid R✝
S : Type ?u.3191370
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R✝ S
P : Type ?u.3191607
inst✝⁴ : CommRing P
R : Type u_1
Rₘ : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := toField hR
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
⊢ ∃ a, ↑(algebraMap R Rₘ) a = mk' Rₘ r { val := m, property := hm }
R✝ : Type ?u.3191178
inst✝⁷ : CommRing R✝
M✝ : Submonoid R✝
S : Type ?u.3191370
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R✝ S
P : Type ?u.3191607
inst✝⁴ : CommRing P
R : Type u_1
Rₘ : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := toField hR
hM : M ≤ nonZeroDivisors R
x : Rₘ
⊢ ∃ a, ↑(algebraMap R Rₘ) a = x
obtain ⟨r, ⟨m, hm⟩, rfl⟩ := mk'_surjective M x
case intro.intro.mk.intro
R✝ : Type ?u.3191178
inst✝⁷ : CommRing R✝
M✝ : Submonoid R✝
S : Type ?u.3191370
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R✝ S
P : Type ?u.3191607
inst✝⁴ : CommRing P
R : Type u_1
Rₘ : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := toField hR
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ ∃ a, ↑(algebraMap R Rₘ) a = mk' Rₘ r { val := m, property := hm }
case intro.intro.mk
R✝ : Type ?u.3191178
inst✝⁷ : CommRing R✝
M✝ : Submonoid R✝
S : Type ?u.3191370
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R✝ S
P : Type ?u.3191607
inst✝⁴ : CommRing P
R : Type u_1
Rₘ : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := toField hR
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
⊢ ∃ a, ↑(algebraMap R Rₘ) a = mk' Rₘ r { val := m, property := hm }
obtain ⟨n, hn⟩ := hR.mul_inv_cancel (nonZeroDivisors.ne_zero <| hM hm)
no goals
case intro.intro.mk.intro
R✝ : Type ?u.3191178
inst✝⁷ : CommRing R✝
M✝ : Submonoid R✝
S : Type ?u.3191370
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R✝ S
P : Type ?u.3191607
inst✝⁴ : CommRing P
R : Type u_1
Rₘ : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := toField hR
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ ∃ a, ↑(algebraMap R Rₘ) a = mk' Rₘ r { val := m, property := hm }
exact ⟨r * n, by erw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]⟩
no goals
R✝ : Type ?u.3191178
inst✝⁷ : CommRing R✝
M✝ : Submonoid R✝
S : Type ?u.3191370
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R✝ S
P : Type ?u.3191607
inst✝⁴ : CommRing P
R : Type u_1
Rₘ : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := toField hR
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ ↑(algebraMap R Rₘ) (r * n) = mk' Rₘ r { val := m, property := hm }
erw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]