R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit x
u : Oˣ
hu : ↑u = x
⊢ ↑v (↑(algebraMap O R) x) * ↑v (↑(algebraMap O R) ↑u⁻¹) ≤ ↑v (↑(algebraMap O R) x) * 1
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit x
u : Oˣ
hu : ↑u = x
⊢ 1 ≤ ↑v (↑(algebraMap O R) x)
rw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
  (algebraMap O R).map_mul, v.map_mul]
no goals
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x : O
hx : IsUnit x
u : Oˣ
hu : ↑u = x
⊢ ↑v (↑(algebraMap O R) x) * ↑v (↑(algebraMap O R) ↑u⁻¹) ≤ ↑v (↑(algebraMap O R) x) * 1
exact mul_le_mul_left' (hv.2 (u⁻¹ : Units O)) _