-- Mathlib/NumberTheory/FunctionField.lean
theorem InftyValuation.map_add_le_max' (x y : RatFunc Fq) :
    inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y)

Proof state:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ inftyValuationDef Fq x ≤ 0 ⊔ inftyValuationDef Fq x

Tactic:
rw [max_eq_right (WithZero.zero_le (inftyValuationDef Fq x))]

Result:
no goals

Proof state:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

Tactic:
by_cases hy : y = 0

Result:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

Proof state:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ ↑(Multiplicative.ofAdd (x + y).intDegree) ≤ ↑(Multiplicative.ofAdd x.intDegree) ⊔ ↑(Multiplicative.ofAdd y.intDegree)

Tactic:
rw [le_max_iff, WithZero.coe_le_coe, Multiplicative.ofAdd_le, WithZero.coe_le_coe,
  Multiplicative.ofAdd_le, ← le_max_iff]

Result:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ (x + y).intDegree ≤ x.intDegree ⊔ y.intDegree

Proof state:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

Tactic:
by_cases hx : x = 0

Result:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

Proof state:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

Tactic:
rw [inftyValuationDef, if_pos hxy]

Result:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ 0 ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

Proof state:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ 0 ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

Tactic:
exact zero_le'

Result:
no goals

Proof state:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ inftyValuationDef Fq x ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq 0

Tactic:
conv_rhs => rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]

Result:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ inftyValuationDef Fq x ≤ 0 ⊔ inftyValuationDef Fq x

Proof state:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

Tactic:
rw [hx, zero_add]

Result:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ inftyValuationDef Fq y ≤ inftyValuationDef Fq 0 ⊔ inftyValuationDef Fq y

Proof state:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ inftyValuationDef Fq y ≤ inftyValuationDef Fq 0 ⊔ inftyValuationDef Fq y

Tactic:
conv_rhs => rw [inftyValuationDef, if_pos (Eq.refl _)]

Result:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ inftyValuationDef Fq y ≤ 0 ⊔ inftyValuationDef Fq y

Proof state:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

Tactic:
rw [inftyValuationDef, inftyValuationDef, inftyValuationDef, if_neg hx, if_neg hy,
  if_neg hxy]

Result:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ ↑(Multiplicative.ofAdd (x + y).intDegree) ≤ ↑(Multiplicative.ofAdd x.intDegree) ⊔ ↑(Multiplicative.ofAdd y.intDegree)

Proof state:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ (x + y).intDegree ≤ x.intDegree ⊔ y.intDegree

Tactic:
exact RatFunc.intDegree_add_le hy hxy

Result:
no goals

Proof state:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : x = 0
⊢ inftyValuationDef Fq y ≤ 0 ⊔ inftyValuationDef Fq y

Tactic:
rw [max_eq_right (WithZero.zero_le (inftyValuationDef Fq y))]

Result:
no goals

Proof state:
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

Tactic:
by_cases hxy : x + y = 0

Result:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

Proof state:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ inftyValuationDef Fq (x + y) ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq y

Tactic:
rw [hy, add_zero]

Result:
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x y : RatFunc Fq
hx : ¬x = 0
hy : y = 0
⊢ inftyValuationDef Fq x ≤ inftyValuationDef Fq x ⊔ inftyValuationDef Fq 0