p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ min (addValuationDef x) (addValuationDef y) ≤ addValuationDef (x + y)
simp only [addValuationDef]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
by_cases hxy : x + y = 0
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤ ⊤
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
rw [hxy, if_pos (Eq.refl _)]
no goals
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤ ⊤
exact le_top
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
by_cases hx : x = 0
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ (if y = 0 then ⊤ else ↑(valuation y)) ≤ ⊤
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
rw [hx, if_pos (Eq.refl _), min_eq_right, zero_add]
no goals
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ (if y = 0 then ⊤ else ↑(valuation y)) ≤ ⊤
exact le_top
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
by_cases hy : y = 0
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ (if x = 0 then ⊤ else ↑(valuation x)) ≤ ⊤
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
rw [hy, if_pos (Eq.refl _), min_eq_left, add_zero]
no goals
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ (if x = 0 then ⊤ else ↑(valuation x)) ≤ ⊤
exact le_top
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
rw [if_neg hx, if_neg hy, if_neg hxy, ← WithTop.coe_min, WithTop.coe_le_coe]
no goals
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
exact valuation_map_add hxy