-- Mathlib/RingTheory/Localization/Defs.lean
lemma injective_of_map_algebraMap_zero {T} [CommRing T] (f : S →+* T)
    (h : ∀ x, f (algebraMap R S x) = 0 → algebraMap R S x = 0) :
    Function.Injective f

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_5
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
x y : R
hz : f ((algebraMap R S) (x - y)) = 0
⊢ (algebraMap R S) x = (algebraMap R S) y

Tactic:
apply h at hz

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_5
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
x y : R
hz : (algebraMap R S) (x - y) = 0
⊢ (algebraMap R S) x = (algebraMap R S) y

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_5
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
x y : R
hz : f ((algebraMap R S) x) = f ((algebraMap R S) y)
⊢ (algebraMap R S) x = (algebraMap R S) y

Tactic:
rw [← sub_eq_zero, ← map_sub, ← map_sub] at hz

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_5
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
x y : R
hz : f ((algebraMap R S) (x - y)) = 0
⊢ (algebraMap R S) x = (algebraMap R S) y

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_5
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
⊢ Injective ⇑f

Tactic:
rw [IsLocalization.injective_iff_map_algebraMap_eq M]

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_5
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
⊢ ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ f ((algebraMap R S) x) = f ((algebraMap R S) y)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_5
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
⊢ ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ f ((algebraMap R S) x) = f ((algebraMap R S) y)

Tactic:
refine fun x y ↦ ⟨fun hz ↦ hz ▸ rfl, fun hz ↦ ?_⟩

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_5
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
x y : R
hz : f ((algebraMap R S) x) = f ((algebraMap R S) y)
⊢ (algebraMap R S) x = (algebraMap R S) y

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_5
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
x y : R
hz : (algebraMap R S) (x - y) = 0
⊢ (algebraMap R S) x = (algebraMap R S) y

Tactic:
rwa [map_sub, sub_eq_zero] at hz

Result:
no goals