p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ Int.natAbs ↑p ≠ 1 ∧ z ≠ 0
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ (multiplicity (↑p) z).Dom
apply multiplicity.finite_int_iff.2
no goals
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ Int.natAbs ↑p ≠ 1 ∧ z ≠ 0
simp [hp, hz]
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ Part.get (multiplicity p (Int.natAbs z)) (_ : multiplicity.Finite p (Int.natAbs z)) =
    Part.get (multiplicity (↑p) z) (_ : multiplicity.Finite (↑p) z)
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ padicValInt p z = Part.get (multiplicity (↑p) z) (_ : multiplicity.Finite (↑p) z)
rw [padicValInt, padicValNat, dif_pos (And.intro hp (Int.natAbs_pos.mpr hz))]
no goals
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ Part.get (multiplicity p (Int.natAbs z)) (_ : multiplicity.Finite p (Int.natAbs z)) =
    Part.get (multiplicity (↑p) z) (_ : multiplicity.Finite (↑p) z)
simp only [multiplicity.Int.natAbs p z]