K : Type ?u.3854144
F : Type ?u.3854147
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.3854159
Γ''₀ : Type ?u.3854162
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
aux : ∀ (a s : R), ↑v s = 0 → ↑v (a + s) ≤ ↑v a
⊢ ↑v (a + s) = ↑v a
K : Type ?u.3854144
F : Type ?u.3854147
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.3854159
Γ''₀ : Type ?u.3854162
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
⊢ ↑v (a + s) = ↑v a
have aux : ∀ a s, v s = 0 → v (a + s) ≤ v a := by
  intro a' s' h'
  refine' le_trans (v.map_add a' s') (max_le le_rfl _)
  simp [h']
K : Type ?u.3854144
F : Type ?u.3854147
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.3854159
Γ''₀ : Type ?u.3854162
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
aux : ∀ (a s : R), ↑v s = 0 → ↑v (a + s) ≤ ↑v a
⊢ ↑v a ≤ ↑v (a + s)
K : Type ?u.3854144
F : Type ?u.3854147
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.3854159
Γ''₀ : Type ?u.3854162
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
aux : ∀ (a s : R), ↑v s = 0 → ↑v (a + s) ≤ ↑v a
⊢ ↑v (a + s) = ↑v a
apply le_antisymm (aux a s h)
no goals
K : Type ?u.3854144
F : Type ?u.3854147
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.3854159
Γ''₀ : Type ?u.3854162
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
aux : ∀ (a s : R), ↑v s = 0 → ↑v (a + s) ≤ ↑v a
⊢ ↑v a ≤ ↑v (a + s)
calc
  v a = v (a + s + -s) := by simp
  _ ≤ v (a + s) := aux (a + s) (-s) (by rwa [← Ideal.neg_mem_iff] at h)
K : Type ?u.3854144
F : Type ?u.3854147
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.3854159
Γ''₀ : Type ?u.3854162
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
a' s' : R
h' : ↑v s' = 0
⊢ ↑v (a' + s') ≤ ↑v a'
K : Type ?u.3854144
F : Type ?u.3854147
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.3854159
Γ''₀ : Type ?u.3854162
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
⊢ ∀ (a s : R), ↑v s = 0 → ↑v (a + s) ≤ ↑v a
intro a' s' h'
K : Type ?u.3854144
F : Type ?u.3854147
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.3854159
Γ''₀ : Type ?u.3854162
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
a' s' : R
h' : ↑v s' = 0
⊢ ↑v s' ≤ ↑v a'
K : Type ?u.3854144
F : Type ?u.3854147
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.3854159
Γ''₀ : Type ?u.3854162
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
a' s' : R
h' : ↑v s' = 0
⊢ ↑v (a' + s') ≤ ↑v a'
refine' le_trans (v.map_add a' s') (max_le le_rfl _)
no goals
K : Type ?u.3854144
F : Type ?u.3854147
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.3854159
Γ''₀ : Type ?u.3854162
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
a' s' : R
h' : ↑v s' = 0
⊢ ↑v s' ≤ ↑v a'
simp [h']
no goals
K : Type ?u.3854144
F : Type ?u.3854147
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.3854159
Γ''₀ : Type ?u.3854162
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
aux : ∀ (a s : R), ↑v s = 0 → ↑v (a + s) ≤ ↑v a
⊢ ↑v a = ↑v (a + s + -s)
simp
no goals
K : Type ?u.3854144
F : Type ?u.3854147
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.3854159
Γ''₀ : Type ?u.3854162
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
a s : R
h : s ∈ supp v
aux : ∀ (a s : R), ↑v s = 0 → ↑v (a + s) ≤ ↑v a
⊢ ↑v (-s) = 0
rwa [← Ideal.neg_mem_iff] at h