p : ℕ
z : ℤ
h : ¬↑p ∣ z
⊢ (if h : p ≠ 1 ∧ 0 < Int.natAbs z then
      Part.get (multiplicity p (Int.natAbs z)) (_ : multiplicity.Finite p (Int.natAbs z))
    else 0) =
    0
p : ℕ
z : ℤ
h : ¬↑p ∣ z
⊢ padicValInt p z = 0
rw [padicValInt, padicValNat]
no goals
p : ℕ
z : ℤ
h : ¬↑p ∣ z
⊢ (if h : p ≠ 1 ∧ 0 < Int.natAbs z then
      Part.get (multiplicity p (Int.natAbs z)) (_ : multiplicity.Finite p (Int.natAbs z))
    else 0) =
    0
split_ifs <;> simp [multiplicity.Int.natAbs, multiplicity_eq_zero.2 h]