-- Mathlib/RingTheory/Valuation/AlgebraInstances.lean
theorem integralClosure_algebraMap_injective :
    Injective (algebraMap v.valuationSubring (integralClosure v.valuationSubring L))

Proof state:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
hinj : Injective ⇑(algebraMap (↥v.valuationSubring) L)
x : ↥v.valuationSubring
hx : ↑((algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L)) x) = 0
⊢ x = 0

Tactic:
rw [injective_iff_map_eq_zero (algebraMap v.valuationSubring L)] at hinj

Result:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
hinj : ∀ (a : ↥v.valuationSubring), (algebraMap (↥v.valuationSubring) L) a = 0 → a = 0
x : ↥v.valuationSubring
hx : ↑((algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L)) x) = 0
⊢ x = 0

Proof state:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
hinj : Injective ⇑(algebraMap (↥v.valuationSubring) L)
⊢ Injective ⇑(algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L))

Tactic:
rw [injective_iff_map_eq_zero (algebraMap v.valuationSubring _)]

Result:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
hinj : Injective ⇑(algebraMap (↥v.valuationSubring) L)
⊢ ∀ (a : ↥v.valuationSubring), (algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L)) a = 0 → a = 0

Proof state:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
hinj : Injective ⇑(algebraMap (↥v.valuationSubring) L)
x : ↥v.valuationSubring
hx : (algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L)) x = 0
⊢ x = 0

Tactic:
rw [← Subtype.coe_inj, Subalgebra.coe_zero] at hx

Result:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
hinj : Injective ⇑(algebraMap (↥v.valuationSubring) L)
x : ↥v.valuationSubring
hx : ↑((algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L)) x) = 0
⊢ x = 0

Proof state:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
hinj : ∀ (a : ↥v.valuationSubring), (algebraMap (↥v.valuationSubring) L) a = 0 → a = 0
x : ↥v.valuationSubring
hx : ↑((algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L)) x) = 0
⊢ x = 0

Tactic:
exact hinj x hx

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Injective ⇑(algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L))

Tactic:
have hinj : Injective ⇑(algebraMap v.valuationSubring L) :=
  ValuationSubring.algebraMap_injective v L

Result:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
hinj : Injective ⇑(algebraMap (↥v.valuationSubring) L)
⊢ Injective ⇑(algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L))

Proof state:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
hinj : Injective ⇑(algebraMap (↥v.valuationSubring) L)
⊢ ∀ (a : ↥v.valuationSubring), (algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L)) a = 0 → a = 0

Tactic:
intro x hx

Result:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
hinj : Injective ⇑(algebraMap (↥v.valuationSubring) L)
x : ↥v.valuationSubring
hx : (algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L)) x = 0
⊢ x = 0