rw [WithTop.none_eq_top, top_le_iff, WithTop.mul_top hk, top_le_iff, WithTop.mul_eq_top_iff,
  iff_true_intro hk, iff_false_intro hk']
case none
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
k m : ℕ∞
hk : k ≠ 0
hk' : k ≠ ⊤
⊢ k * none ≤ k * m ↔ none ≤ m
case none
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
k m : ℕ∞
hk : k ≠ 0
hk' : k ≠ ⊤
⊢ True ∧ m = ⊤ ∨ False ∧ m ≠ 0 ↔ m = ⊤