-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_add_of_distinct_val (h : v x ≠ v y) : v (x + y) = max (v x) (v y)

Proof state:
case inr
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
h' : v (x + y) < v x ⊔ v y
this : ∀ {x y : R}, v x ≠ v y → v (x + y) < v x ⊔ v y → v y < v x → False
vyx : ¬v y < v x
⊢ v (y + x) < v y ⊔ v x

Tactic:
rwa [add_comm, max_comm]

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ 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)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
h' : v (x + y) < v x ⊔ v y
⊢ False

Tactic:
wlog vyx : v y < v x generalizing x y

Result:
case inr
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
h' : v (x + y) < v x ⊔ v y
this : ∀ {x y : R}, v x ≠ v y → v (x + y) < v x ⊔ v y → v y < v x → False
vyx : ¬v y < v x
⊢ False

R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ v y
h' : v (x + y) < v x ⊔ v y
vyx : v y < v x
⊢ False

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
⊢ ¬v (x + y) < v x ⊔ v y

Tactic:
intro h'

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
h' : v (x + y) < v x ⊔ v y
⊢ False

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ v y
h' : v (x + y) < v x ⊔ v y
vyx : v y < v x
⊢ False

Tactic:
rw [max_eq_left_of_lt vyx] at h'

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ v y
h' : v (x + y) < v x
vyx : v y < v x
⊢ False

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ v y
h' : v (x + y) < v x
vyx : v y < v x
⊢ False

Tactic:
apply lt_irrefl (v x)

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ v y
h' : v (x + y) < v x
vyx : v y < v x
⊢ v x < v x

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x✝ y✝ x y : R
h : v x ≠ v y
h' : v (x + y) < v x
vyx : v y < v x
⊢ v x < v x

Tactic:
calc
  v x = v (x + y - y) := by simp
  _ ≤ max (v <| x + y) (v y) := map_sub _ _ _
  _ < v x := max_lt h' vyx

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
⊢ v (x + y) = v x ⊔ v y

Tactic:
suffices ¬v (x + y) < max (v x) (v y) from
  or_iff_not_imp_right.1 (le_iff_eq_or_lt.1 (v.map_add x y)) this

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
⊢ ¬v (x + y) < v x ⊔ v y

Proof state:
case inr
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
h' : v (x + y) < v x ⊔ v y
this : ∀ {x y : R}, v x ≠ v y → v (x + y) < v x ⊔ v y → v y < v x → False
vyx : ¬v y < v x
⊢ False

Tactic:
refine this h.symm ?_ (h.lt_or_lt.resolve_right vyx)

Result:
case inr
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
h : v x ≠ v y
h' : v (x + y) < v x ⊔ v y
this : ∀ {x y : R}, v x ≠ v y → v (x + y) < v x ⊔ v y → v y < v x → False
vyx : ¬v y < v x
⊢ v (y + x) < v y ⊔ v x