obtain (m|m) := m
case some
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 ≠ ⊤
n : ℕ
⊢ k * some n ≤ k * m ↔ some n ≤ m
case some.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 : ℕ∞
hk : k ≠ 0
hk' : k ≠ ⊤
n : ℕ
⊢ k * some n ≤ k * none ↔ some n ≤ none

case some.some
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
k : ℕ∞
hk : k ≠ 0
hk' : k ≠ ⊤
n m : ℕ
⊢ k * some n ≤ k * some m ↔ some n ≤ some m