-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem AddValuation.map_add (x y : ℚ_[p]) :
    min (addValuationDef x) (addValuationDef y) ≤ addValuationDef (x + y : ℚ_[p])

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ (if y = 0 then ⊤ else ↑y.valuation) ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
⊢ ((if x = 0 then ⊤ else ↑x.valuation) ⊓ if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
by_cases hx : x = 0

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ ((if x = 0 then ⊤ else ↑x.valuation) ⊓ if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
⊢ ((if x = 0 then ⊤ else ↑x.valuation) ⊓ if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Proof state:
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 ↑x.valuation) ⊓ if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
rw [hy, if_pos rfl, min_eq_left, add_zero]

Result:
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 ↑x.valuation) ≤ ⊤

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

Tactic:
exact le_top

Result:
no goals

Proof state:
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 ↑x.valuation) ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
⊢ ((if x = 0 then ⊤ else ↑x.valuation) ⊓ if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
by_cases hy : y = 0

Result:
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 ↑x.valuation) ⊓ if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ ((if x = 0 then ⊤ else ↑x.valuation) ⊓ if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ x.addValuationDef ⊓ y.addValuationDef ≤ (x + y).addValuationDef

Tactic:
simp only [addValuationDef]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ ((if x = 0 then ⊤ else ↑x.valuation) ⊓ if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

Tactic:
exact le_valuation_add hxy

Result:
no goals

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ ((if x = 0 then ⊤ else ↑x.valuation) ⊓ if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
rw [hx, if_pos rfl, min_eq_right, zero_add]

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

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ ((if x = 0 then ⊤ else ↑x.valuation) ⊓ if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
by_cases hxy : x + y = 0

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

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
⊢ ((if x = 0 then ⊤ else ↑x.valuation) ⊓ if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ ((if x = 0 then ⊤ else ↑x.valuation) ⊓ if y = 0 then ⊤ else ↑y.valuation) ≤
    if x + y = 0 then ⊤ else ↑(x + y).valuation

Tactic:
rw [if_neg hx, if_neg hy, if_neg hxy, ← WithTop.coe_min, WithTop.coe_le_coe]

Result:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ x.valuation ⊓ y.valuation ≤ (x + y).valuation

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

Tactic:
rw [hxy, if_pos rfl]

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