-- Mathlib/RingTheory/Localization/Basic.lean
theorem IsField.localization_map_bijective {R Rₘ : Type*} [CommRing R] [CommRing Rₘ]
    {M : Submonoid R} (hM : (0 : R) ∉ M) (hR : IsField R) [Algebra R Rₘ] [IsLocalization M Rₘ] :
    Function.Bijective (algebraMap R Rₘ)

Proof state:
R : Type u_4
Rₘ : Type u_5
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 := hR.toField
⊢ Bijective ⇑(algebraMap R Rₘ)

Tactic:
replace hM := le_nonZeroDivisors_of_noZeroDivisors hM

Result:
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
⊢ Bijective ⇑(algebraMap R Rₘ)

Proof state:
case intro.intro.mk
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
⊢ ∃ a, (algebraMap R Rₘ) a = mk' Rₘ r ⟨m, hm⟩

Tactic:
obtain ⟨n, hn⟩ := hR.mul_inv_cancel (nonZeroDivisors.ne_zero <| hM hm)

Result:
case intro.intro.mk.intro
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ ∃ a, (algebraMap R Rₘ) a = mk' Rₘ r ⟨m, hm⟩

Proof state:
case intro.intro.mk.intro
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ ∃ a, (algebraMap R Rₘ) a = mk' Rₘ r ⟨m, hm⟩

Tactic:
exact ⟨r * n, by rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]⟩

Result:
no goals

Proof state:
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ (algebraMap R Rₘ) (r * n) = mk' Rₘ r ⟨m, hm⟩

Tactic:
rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]

Result:
no goals

Proof state:
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
⊢ Bijective ⇑(algebraMap R Rₘ)

Tactic:
refine ⟨IsLocalization.injective _ hM, fun x => ?_⟩

Result:
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
x : Rₘ
⊢ ∃ a, (algebraMap R Rₘ) a = x

Proof state:
R : Type u_4
Rₘ : Type u_5
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ₘ)

Tactic:
letI := hR.toField

Result:
R : Type u_4
Rₘ : Type u_5
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 := hR.toField
⊢ Bijective ⇑(algebraMap R Rₘ)

Proof state:
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
x : Rₘ
⊢ ∃ a, (algebraMap R Rₘ) a = x

Tactic:
obtain ⟨r, ⟨m, hm⟩, rfl⟩ := mk'_surjective M x

Result:
case intro.intro.mk
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
⊢ ∃ a, (algebraMap R Rₘ) a = mk' Rₘ r ⟨m, hm⟩