case inl
α : Type ?u.1342344
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = ↑(_root_.Int.natAbs b)
⊢ multiplicity a (_root_.Int.natAbs b) = multiplicity ↑a ↑(_root_.Int.natAbs b)

case inr
α : Type ?u.1342344
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = -↑(_root_.Int.natAbs b)
⊢ multiplicity a (_root_.Int.natAbs b) = multiplicity (↑a) (-↑(_root_.Int.natAbs b))
α : Type ?u.1342344
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
⊢ multiplicity a (_root_.Int.natAbs b) = multiplicity (↑a) b
cases' Int.natAbs_eq b with h h <;> conv_rhs => rw [h]
no goals
case inl
α : Type ?u.1342344
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = ↑(_root_.Int.natAbs b)
⊢ multiplicity a (_root_.Int.natAbs b) = multiplicity ↑a ↑(_root_.Int.natAbs b)
rw [Int.coe_nat_multiplicity]
no goals
case inr
α : Type ?u.1342344
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : ℕ
b : ℤ
h : b = -↑(_root_.Int.natAbs b)
⊢ multiplicity a (_root_.Int.natAbs b) = multiplicity (↑a) (-↑(_root_.Int.natAbs b))
rw [multiplicity.neg, Int.coe_nat_multiplicity]