Theorem: ENat.mul_mono_left (FltRegular/CaseII/AuxLemmas.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
k n m : ℕ∞
hk : k ≠ 0
hk' : k ≠ ⊤
⊢ k * n ≤ k * m ↔ n ≤ m
Tactic:
obtain (n|n) := n
State after:
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 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

State before:
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
Tactic:
obtain (m|m) := m
State after:
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

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

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

State before:
case some.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
n m k : ℕ
hk : some k ≠ 0
hk' : some k ≠ ⊤
⊢ some k * some n ≤ some k * some m ↔ some n ≤ some m
Tactic:
simp_rw [WithTop.some_eq_coe, ENat.some_eq_coe]
State after:
case some.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
n m k : ℕ
hk : some k ≠ 0
hk' : some k ≠ ⊤
⊢ ↑k * ↑n ≤ ↑k * ↑m ↔ ↑n ≤ ↑m

State before:
case some.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
n m k : ℕ
hk : some k ≠ 0
hk' : some k ≠ ⊤
⊢ ↑k * ↑n ≤ ↑k * ↑m ↔ ↑n ≤ ↑m
Tactic:
rw [← ENat.coe_mul, ← ENat.coe_mul, Nat.cast_le, Nat.cast_le]
State after:
case some.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
n m k : ℕ
hk : some k ≠ 0
hk' : some k ≠ ⊤
⊢ k * n ≤ k * m ↔ n ≤ m

State before:
case some.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
n m k : ℕ
hk : some k ≠ 0
hk' : some k ≠ ⊤
⊢ k * n ≤ k * m ↔ n ≤ m
Tactic:
refine (strictMono_mul_left_of_pos (Nat.pos_of_ne_zero ?_)).le_iff_le
State after:
case some.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
n m k : ℕ
hk : some k ≠ 0
hk' : some k ≠ ⊤
⊢ k ≠ 0

State before:
case some.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
n m k : ℕ
hk : some k ≠ 0
hk' : some k ≠ ⊤
⊢ k ≠ 0
Tactic:
rintro rfl
State after:
case some.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
n m : ℕ
hk : some 0 ≠ 0
hk' : some 0 ≠ ⊤
⊢ False

State before:
case some.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
n m : ℕ
hk : some 0 ≠ 0
hk' : some 0 ≠ ⊤
⊢ False
Tactic:
exact hk rfl
State after:
no goals

State before:
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
Tactic:
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']
State after:
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 = ⊤

State before:
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 = ⊤
Tactic:
simp
State after:
no goals

State before:
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
Tactic:
simp only [WithTop.none_eq_top, le_top, iff_true]
State after:
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 * ⊤

State before:
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 * ⊤
Tactic:
rw [WithTop.mul_top hk]
State after:
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 ≤ ⊤

State before:
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 ≤ ⊤
Tactic:
simp
State after:
no goals

State before:
case some.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
n m : ℕ
hk : none ≠ 0
hk' : none ≠ ⊤
⊢ none * some n ≤ none * some m ↔ some n ≤ some m
Tactic:
simp at hk'
State after:
case some.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
n m : ℕ
hk : none ≠ 0
hk' : ¬none = ⊤
⊢ none * some n ≤ none * some m ↔ some n ≤ some m

State before:
case some.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
n m : ℕ
hk : none ≠ 0
hk' : ¬none = ⊤
⊢ none * some n ≤ none * some m ↔ some n ≤ some m
Tactic:
contradiction
State after:
no goals