have := H q hq
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
⊢ 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 : multiplicity q (q * a) ≤ multiplicity q (a * c)
⊢ a * q ∣ a * c