K : Type ?u.2296489
F : Type ?u.2296492
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2296504
Γ''₀ : Type ?u.2296507
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (y - x) < ↑v x
this : ↑v (y - x + x) = max (↑v (y - x)) (↑v x)
⊢ ↑v y = ↑v x
K : Type ?u.2296489
F : Type ?u.2296492
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2296504
Γ''₀ : Type ?u.2296507
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (y - x) < ↑v x
⊢ ↑v y = ↑v x
have := Valuation.map_add_of_distinct_val v (ne_of_gt h).symm
K : Type ?u.2296489
F : Type ?u.2296492
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2296504
Γ''₀ : Type ?u.2296507
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (y - x) < ↑v x
this : ↑v (y - x + x) = ↑v x
⊢ ↑v y = ↑v x
K : Type ?u.2296489
F : Type ?u.2296492
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2296504
Γ''₀ : Type ?u.2296507
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (y - x) < ↑v x
this : ↑v (y - x + x) = max (↑v (y - x)) (↑v x)
⊢ ↑v y = ↑v x
rw [max_eq_right (le_of_lt h)] at this
no goals
K : Type ?u.2296489
F : Type ?u.2296492
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2296504
Γ''₀ : Type ?u.2296507
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (y - x) < ↑v x
this : ↑v (y - x + x) = ↑v x
⊢ ↑v y = ↑v x
simpa using this