K : Type ?u.419164
F : Type ?u.419167
R : Type u_2
inst✝⁴ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.419179
Γ''₀ : Type ?u.419182
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
⊢ ↑v (x + y) ≤ ↑v x ∨ ↑v (x + y) ≤ ↑v y
K : Type ?u.419164
F : Type ?u.419167
R : Type u_2
inst✝⁴ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.419179
Γ''₀ : Type ?u.419182
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
⊢ ∀ (x y : R), ↑v (x + y) ≤ ↑v x ∨ ↑v (x + y) ≤ ↑v y
intro x y
K : Type ?u.419164
F : Type ?u.419167
R : Type u_2
inst✝⁴ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.419179
Γ''₀ : Type ?u.419182
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
⊢ max (↑v x) (↑v y) ≥ ↑v (x + y)
K : Type ?u.419164
F : Type ?u.419167
R : Type u_2
inst✝⁴ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.419179
Γ''₀ : Type ?u.419182
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
⊢ ↑v (x + y) ≤ ↑v x ∨ ↑v (x + y) ≤ ↑v y
rw [← le_max_iff, ← ge_iff_le]
no goals
K : Type ?u.419164
F : Type ?u.419167
R : Type u_2
inst✝⁴ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.419179
Γ''₀ : Type ?u.419182
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
⊢ max (↑v x) (↑v y) ≥ ↑v (x + y)
apply map_add