K : Type ?u.4087485
F : Type ?u.4087488
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.4087500
inst✝² : Ring R
inst✝¹ : LinearOrderedAddCommMonoidWithTop Γ₀
inst✝ : LinearOrderedAddCommMonoidWithTop Γ'₀
v : AddValuation R Γ₀
x✝ y✝ z x y : R
⊢ ↑v x ≤ ↑v (x + y) ∨ ↑v y ≤ ↑v (x + y)
K : Type ?u.4087485
F : Type ?u.4087488
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.4087500
inst✝² : Ring R
inst✝¹ : LinearOrderedAddCommMonoidWithTop Γ₀
inst✝ : LinearOrderedAddCommMonoidWithTop Γ'₀
v : AddValuation R Γ₀
x y z : R
⊢ ∀ (x y : R), ↑v x ≤ ↑v (x + y) ∨ ↑v y ≤ ↑v (x + y)
intro x y
K : Type ?u.4087485
F : Type ?u.4087488
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.4087500
inst✝² : Ring R
inst✝¹ : LinearOrderedAddCommMonoidWithTop Γ₀
inst✝ : LinearOrderedAddCommMonoidWithTop Γ'₀
v : AddValuation R Γ₀
x✝ y✝ z x y : R
⊢ ↑v (x + y) ≥ min (↑v x) (↑v y)
K : Type ?u.4087485
F : Type ?u.4087488
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.4087500
inst✝² : Ring R
inst✝¹ : LinearOrderedAddCommMonoidWithTop Γ₀
inst✝ : LinearOrderedAddCommMonoidWithTop Γ'₀
v : AddValuation R Γ₀
x✝ y✝ z x y : R
⊢ ↑v x ≤ ↑v (x + y) ∨ ↑v y ≤ ↑v (x + y)
rw [← @min_le_iff _ _ (v x) (v y) (v (x+y)), ← ge_iff_le]
no goals
K : Type ?u.4087485
F : Type ?u.4087488
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.4087500
inst✝² : Ring R
inst✝¹ : LinearOrderedAddCommMonoidWithTop Γ₀
inst✝ : LinearOrderedAddCommMonoidWithTop Γ'₀
v : AddValuation R Γ₀
x✝ y✝ z x y : R
⊢ ↑v (x + y) ≥ min (↑v x) (↑v y)
apply map_add