internlm/Lean-Github huggingface dataset:
Theorem: ENat.mul_mono_left
Proof 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
Proof 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
Theorem: ENat.mul_mono_left
Proof 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
Proof 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
Theorem: ENat.mul_mono_left
Proof 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
Proof 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
Theorem: ENat.mul_mono_left
Proof 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]
Proof 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
Theorem: ENat.mul_mono_left
Proof 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]
Proof 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
Theorem: ENat.mul_mono_left
Proof 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
Proof 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
Theorem: ENat.mul_mono_left
Proof 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
Proof 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
Theorem: ENat.mul_mono_left
Proof 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
Proof state after:
no goals
Theorem: ENat.mul_mono_left
Proof 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']
Proof 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 = ⊤
Theorem: ENat.mul_mono_left
Proof 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
Proof state after:
no goals
Theorem: ENat.mul_mono_left
Proof 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]
Proof 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 * ⊤
Theorem: ENat.mul_mono_left
Proof 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]
Proof 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 ≤ ⊤
Theorem: ENat.mul_mono_left
Proof 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
Proof state after:
no goals
Theorem: ENat.mul_mono_left
Proof 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'
Proof 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
Theorem: ENat.mul_mono_left
Proof 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
Proof state after:
no goals
Theorem: ENat.nsmul_mono
Proof 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
n m : ℕ∞
k : ℕ
hk : k ≠ 0
⊢ k • n ≤ k • m ↔ n ≤ m
Tactic:
simp_rw [nsmul_eq_mul]
Proof state after:
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 : k ≠ 0
⊢ ↑k * n ≤ ↑k * m ↔ n ≤ m
Theorem: ENat.nsmul_mono
Proof 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
n m : ℕ∞
k : ℕ
hk : k ≠ 0
⊢ ↑k * n ≤ ↑k * m ↔ n ≤ m
Tactic:
apply ENat.mul_mono_left
Proof state after:
case hk
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 : k ≠ 0
⊢ ↑k ≠ 0

case hk'
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 : k ≠ 0
⊢ ↑k ≠ ⊤
Theorem: ENat.nsmul_mono
Proof state before:
case hk
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 : k ≠ 0
⊢ ↑k ≠ 0
Tactic:
exact Nat.cast_ne_zero.mpr hk
Proof state after:
no goals
Theorem: ENat.nsmul_mono
Proof state before:
case hk'
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 : k ≠ 0
⊢ ↑k ≠ ⊤
Tactic:
exact coe_ne_top k
Proof state after:
no goals
Theorem: pow_dvd_pow_iff_dvd
Proof 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
M : Type u_2
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
⊢ a ^ x ∣ b ^ x ↔ a ∣ b
Tactic:
by_cases ha : a = 0
Proof state after:
case pos
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : a = 0
⊢ a ^ x ∣ b ^ x ↔ a ∣ b

case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
⊢ a ^ x ∣ b ^ x ↔ a ∣ b
Theorem: pow_dvd_pow_iff_dvd
Proof state before:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
⊢ a ^ x ∣ b ^ x ↔ a ∣ b
Tactic:
have ha' : a ^ x ≠ 0 := (pow_ne_zero_iff h').mpr ha
Proof state after:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
⊢ a ^ x ∣ b ^ x ↔ a ∣ b
Theorem: pow_dvd_pow_iff_dvd
Proof state before:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
⊢ a ^ x ∣ b ^ x ↔ a ∣ b
Tactic:
rw [dvd_iff_multiplicity_le ha, dvd_iff_multiplicity_le ha']
Proof state after:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
⊢ (∀ (p : M), Prime p → multiplicity p (a ^ x) ≤ multiplicity p (b ^ x)) ↔
    ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b
Theorem: pow_dvd_pow_iff_dvd
Proof state before:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
⊢ (∀ (p : M), Prime p → multiplicity p (a ^ x) ≤ multiplicity p (b ^ x)) ↔
    ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b
Tactic:
refine forall₂_congr (fun p hp ↦ ?_)
Proof state after:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ multiplicity p (a ^ x) ≤ multiplicity p (b ^ x) ↔ multiplicity p a ≤ multiplicity p b
Theorem: pow_dvd_pow_iff_dvd
Proof state before:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ multiplicity p (a ^ x) ≤ multiplicity p (b ^ x) ↔ multiplicity p a ≤ multiplicity p b
Tactic:
simp_rw [multiplicity.pow hp, ← PartENat.withTopEquiv_le]
Proof state after:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ PartENat.withTopEquiv (x • multiplicity p a) ≤ PartENat.withTopEquiv (x • multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p b)
Theorem: pow_dvd_pow_iff_dvd
Proof state before:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ PartENat.withTopEquiv (x • multiplicity p a) ≤ PartENat.withTopEquiv (x • multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p b)
Tactic:
show PartENat.withTopAddEquiv _ ≤ PartENat.withTopAddEquiv _ ↔ _
Proof state after:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ PartENat.withTopAddEquiv (x • multiplicity p a) ≤ PartENat.withTopAddEquiv (x • multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p b)
Theorem: pow_dvd_pow_iff_dvd
Proof state before:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ PartENat.withTopAddEquiv (x • multiplicity p a) ≤ PartENat.withTopAddEquiv (x • multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p b)
Tactic:
simp_rw [map_nsmul]
Proof state after:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ x • PartENat.withTopAddEquiv (multiplicity p a) ≤ x • PartENat.withTopAddEquiv (multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p b)
Theorem: pow_dvd_pow_iff_dvd
Proof state before:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ x • PartENat.withTopAddEquiv (multiplicity p a) ≤ x • PartENat.withTopAddEquiv (multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p b)
Tactic:
rw [ENat.nsmul_mono h']
Proof state after:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ PartENat.withTopAddEquiv (multiplicity p a) ≤ PartENat.withTopAddEquiv (multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p b)
Theorem: pow_dvd_pow_iff_dvd
Proof state before:
case neg
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : ¬a = 0
ha' : a ^ x ≠ 0
p : M
hp : Prime p
⊢ PartENat.withTopAddEquiv (multiplicity p a) ≤ PartENat.withTopAddEquiv (multiplicity p b) ↔
    PartENat.withTopEquiv (multiplicity p a) ≤ PartENat.withTopEquiv (multiplicity p b)
Tactic:
rfl
Proof state after:
no goals
Theorem: pow_dvd_pow_iff_dvd
Proof state before:
case pos
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✝ : UniqueFactorizationMonoid M
a b : M
x : ℕ
h' : x ≠ 0
ha : a = 0
⊢ a ^ x ∣ b ^ x ↔ a ∣ b
Tactic:
rw [ha, zero_pow h', zero_dvd_iff, zero_dvd_iff, pow_eq_zero_iff h']
Proof state after:
no goals
Theorem: isPrincipal_of_isPrincipal_pow_of_Coprime'
Proof 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✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
⊢ (↑I).IsPrincipal
Tactic:
by_cases Izero : I = 0
Proof state after:
case pos
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : I = 0
⊢ (↑I).IsPrincipal

case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : ¬I = 0
⊢ (↑I).IsPrincipal
Theorem: isPrincipal_of_isPrincipal_pow_of_Coprime'
Proof state before:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : ¬I = 0
⊢ (↑I).IsPrincipal
Tactic:
rw [← Ne, ← isUnit_iff_ne_zero] at Izero
Proof state after:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑I).IsPrincipal
Theorem: isPrincipal_of_isPrincipal_pow_of_Coprime'
Proof state before:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑I).IsPrincipal
Tactic:
show Submodule.IsPrincipal (Izero.unit' : FractionalIdeal A⁰ K)
Proof state after:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑↑Izero.unit').IsPrincipal
Theorem: isPrincipal_of_isPrincipal_pow_of_Coprime'
Proof state before:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑↑Izero.unit').IsPrincipal
Tactic:
rw [← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← H, Nat.dvd_gcd_iff]
Proof state after:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ orderOf (ClassGroup.mk Izero.unit') ∣ p ∧ orderOf (ClassGroup.mk Izero.unit') ∣ Fintype.card (ClassGroup A)