rw [← not_imp_not, Ne, ← not_or, not_not]
case mp
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
⊢ multiplicity.Finite x y → ¬IsUnit x ∧ y ≠ 0
case mp
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : WfDvdMonoid M
x y : M
⊢ IsUnit x ∨ y = 0 → ¬multiplicity.Finite x y