no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : Finite p a ∧ Finite p b
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b
rw [← PartENat.natCast_get (finite_iff_dom.1 h.1), ←
    PartENat.natCast_get (finite_iff_dom.1 h.2), ←
    PartENat.natCast_get (finite_iff_dom.1 (finite_mul hp h.1 h.2)), ← Nat.cast_add,
    PartENat.natCast_inj, multiplicity.mul' hp]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : ¬(Finite p a ∧ Finite p b)
⊢ ⊤ = multiplicity p a + multiplicity p b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : ¬(Finite p a ∧ Finite p b)
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b
rw [eq_top_iff_not_finite.2 (mt (finite_mul_iff hp).1 h)]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : ¬(Finite p a ∧ Finite p b)
⊢ ⊤ = multiplicity p a + multiplicity p b
cases' not_and_or.1 h with h h <;> simp [eq_top_iff_not_finite.2 h]