K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
this : ¬↑v (x + y) < max (↑v x) (↑v y)
⊢ ↑v (x + y) = max (↑v x) (↑v y)

case this
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
⊢ ¬↑v (x + y) < max (↑v x) (↑v y)
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
⊢ ↑v (x + y) = max (↑v x) (↑v y)
suffices : ¬v (x + y) < max (v x) (v y)
case this
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
⊢ ¬↑v (x + y) < max (↑v x) (↑v y)
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
this : ¬↑v (x + y) < max (↑v x) (↑v y)
⊢ ↑v (x + y) = max (↑v x) (↑v y)

case this
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
⊢ ¬↑v (x + y) < max (↑v x) (↑v y)
exact or_iff_not_imp_right.1 (le_iff_eq_or_lt.1 (v.map_add x y)) this
case this
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < max (↑v x) (↑v y)
⊢ False
case this
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
⊢ ¬↑v (x + y) < max (↑v x) (↑v y)
intro h'
case this.inr
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < max (↑v x) (↑v y)
this : ∀ {x y : R}, ↑v x ≠ ↑v y → ↑v (x + y) < max (↑v x) (↑v y) → ↑v y < ↑v x → False
vyx : ¬↑v y < ↑v x
⊢ False

K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < max (↑v x) (↑v y)
vyx : ↑v y < ↑v x
⊢ False
case this
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < max (↑v x) (↑v y)
⊢ False
wlog vyx : v y < v x generalizing x y
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < ↑v x
vyx : ↑v y < ↑v x
⊢ False
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < max (↑v x) (↑v y)
vyx : ↑v y < ↑v x
⊢ False
rw [max_eq_left_of_lt vyx] at h'
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < ↑v x
vyx : ↑v y < ↑v x
⊢ ↑v x < ↑v x
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < ↑v x
vyx : ↑v y < ↑v x
⊢ False
apply lt_irrefl (v x)
no goals
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < ↑v x
vyx : ↑v y < ↑v x
⊢ ↑v x < ↑v x
calc
  v x = v (x + y - y) := by simp
  _ ≤ max (v <| x + y) (v y) := (map_sub _ _ _)
  _ < v x := max_lt h' vyx
case this.inr
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < max (↑v x) (↑v y)
this : ∀ {x y : R}, ↑v x ≠ ↑v y → ↑v (x + y) < max (↑v x) (↑v y) → ↑v y < ↑v x → False
vyx : ¬↑v y < ↑v x
⊢ ↑v (y + x) < max (↑v y) (↑v x)
case this.inr
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < max (↑v x) (↑v y)
this : ∀ {x y : R}, ↑v x ≠ ↑v y → ↑v (x + y) < max (↑v x) (↑v y) → ↑v y < ↑v x → False
vyx : ¬↑v y < ↑v x
⊢ False
refine' this h.symm _ (h.lt_or_lt.resolve_right vyx)
no goals
case this.inr
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x y z : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < max (↑v x) (↑v y)
this : ∀ {x y : R}, ↑v x ≠ ↑v y → ↑v (x + y) < max (↑v x) (↑v y) → ↑v y < ↑v x → False
vyx : ¬↑v y < ↑v x
⊢ ↑v (y + x) < max (↑v y) (↑v x)
rwa [add_comm, max_comm]
no goals
K : Type ?u.1807321
F : Type ?u.1807324
R : Type u_2
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type ?u.1807336
Γ''₀ : Type ?u.1807339
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : Ring R
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ z x y : R
h : ↑v x ≠ ↑v y
h' : ↑v (x + y) < ↑v x
vyx : ↑v y < ↑v x
⊢ ↑v x = ↑v (x + y - y)
simp