p : ℕ
⊢ (if h : p ≠ 1 ∧ 0 < 1 then Part.get (multiplicity p 1) (_ : multiplicity.Finite p 1) else 0) = 0
p : ℕ
⊢ padicValNat p 1 = 0
unfold padicValNat
case inl
p : ℕ
h✝ : p ≠ 1 ∧ 0 < 1
⊢ Part.get (multiplicity p 1) (_ : multiplicity.Finite p 1) = 0

case inr
p : ℕ
h✝ : ¬(p ≠ 1 ∧ 0 < 1)
⊢ 0 = 0
p : ℕ
⊢ (if h : p ≠ 1 ∧ 0 < 1 then Part.get (multiplicity p 1) (_ : multiplicity.Finite p 1) else 0) = 0
split_ifs
no goals
case inl
p : ℕ
h✝ : p ≠ 1 ∧ 0 < 1
⊢ Part.get (multiplicity p 1) (_ : multiplicity.Finite p 1) = 0
simp
no goals
case inr
p : ℕ
h✝ : ¬(p ≠ 1 ∧ 0 < 1)
⊢ 0 = 0
rfl