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

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)
by_cases hx : x = 0
no goals
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x = 0
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)
rw [hx, if_pos (Eq.refl _), MulZeroClass.zero_mul, if_pos (Eq.refl _), WithTop.top_add]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)
by_cases hy : y = 0
no goals
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)
rw [hy, if_pos (Eq.refl _), MulZeroClass.mul_zero, if_pos (Eq.refl _), WithTop.add_top]
no goals
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)
rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
  valuation_map_mul hx hy]