rw [multiplicity.mul hq, multiplicity.mul hq, add_comm,
  ← PartENat.natCast_get (multiplicity.finite_iff_dom.mp
    (WfDvdMonoid.multiplicity_finite hq.not_unit ha.2)),
  ← PartENat.natCast_get (multiplicity.finite_iff_dom.mp
    (WfDvdMonoid.multiplicity_finite hq.not_unit hb.2)),
  ← PartENat.natCast_get (multiplicity.finite_iff_dom.mp
    (WfDvdMonoid.multiplicity_finite hq.not_unit ha.1)),
  ← Nat.cast_add, ← Nat.cast_add, PartENat.coe_le_coe,
  multiplicity.get_multiplicity_self, add_le_add_iff_left,
  ← PartENat.coe_le_coe, PartENat.natCast_get, ← multiplicity.pow_dvd_iff_le_multiplicity,
  pow_one] at this
case neg.hi.intro
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✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a q : M
a✝ : a ≠ 0
hq : Prime q
ha : ¬q = 0 ∧ ¬a = 0
c : M
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p (a * c)) → a ∣ a * c
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p (a * c)
hb : ¬a = 0 ∧ ¬c = 0
this : multiplicity q (q * a) ≤ multiplicity q (a * c)
⊢ a * q ∣ a * c
case neg.hi.intro
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✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
a q : M
a✝ : a ≠ 0
hq : Prime q
ha : ¬q = 0 ∧ ¬a = 0
c : M
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p (a * c)) → a ∣ a * c
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p (a * c)
hb : ¬a = 0 ∧ ¬c = 0
this : q ∣ c
⊢ a * q ∣ a * c