K : Type ?u.2424657
F : Type ?u.2424660
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2424672
Γ''₀ : Type ?u.2424675
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (-x) < ↑v 1
⊢ ↑v (1 - x) = 1
K : Type ?u.2424657
F : Type ?u.2424660
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2424672
Γ''₀ : Type ?u.2424675
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x < 1
⊢ ↑v (1 - x) = 1
rw [← v.map_one, ← v.map_neg] at h
K : Type ?u.2424657
F : Type ?u.2424660
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2424672
Γ''₀ : Type ?u.2424675
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (-x) < ↑v 1
⊢ ↑v (1 + -x) = 1
K : Type ?u.2424657
F : Type ?u.2424660
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2424672
Γ''₀ : Type ?u.2424675
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (-x) < ↑v 1
⊢ ↑v (1 - x) = 1
rw [sub_eq_add_neg 1 x]
no goals
K : Type ?u.2424657
F : Type ?u.2424660
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.2424672
Γ''₀ : Type ?u.2424675
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v (-x) < ↑v 1
⊢ ↑v (1 + -x) = 1
simpa only [v.map_one, v.map_neg] using v.map_add_eq_of_lt_left h