awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  Eq (α := ℤ) (eval 1 (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ)) (eval 1 (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i))
rw :
  ∀
    (this :
      (↑n : ℤ) =
        HMul.hMul (α := ℤ)
          (∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)),
            eval 1 (cyclotomic x ℤ))
          (∏ x ∈ range (padicValNat p n), eval 1 (cyclotomic (p ^ (x + 1)) ℤ))),
    False
rw₁ :
  ∀
    (this :
      (↑n : ℤ) =
        HMul.hMul (α := ℤ)
          (∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)),
            eval 1 (cyclotomic x ℤ))
          (∏ x ∈ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ))),
    Set.InjOn (β := ℕ) (fun (t : ℕ) ↦ p ^ (t + 1)) (↑(range (padicValNat p n)) : Set ℕ)
⊢ False

Tactic:
rw [eval_geom_sum, one_geom_sum, eval_prod, eq_comm, ←
    Finset.prod_sdiff <| @range_pow_padicValNat_subset_divisors' p _ _, Finset.prod_image] at this

Premises used: Polynomial.eval_prod, one_geom_sum, eq_comm, Finset.prod_sdiff, range_pow_padicValNat_subset_divisors', Finset.prod_image, Polynomial.eval_geom_sum
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HMul.hMul (α := ℤ)
      (∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ))
      (∏ x ∈ range (padicValNat p n), eval 1 (cyclotomic (p ^ (x + 1)) ℤ))
⊢ (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      ∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)

Tactic:
simp_rw [eval_one_cyclotomic_prime_pow, Finset.prod_const, Finset.card_range, mul_comm] at this

Premises used: Finset.card_range, Finset.prod_const, Polynomial.eval_one_cyclotomic_prime_pow, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      ∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
rw :
  ∀
    (this :
      (↑n : ℤ) =
        HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
          HMul.hMul (α := ℤ)
            (∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
              eval 1 (cyclotomic x ℤ))
            (∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))),
    False
rw₁ : {n} ⊆ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))
⊢ False

Tactic:
rw [← Finset.prod_sdiff <| show {n} ⊆ _ from _] at this

Premises used: Finset.prod_sdiff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      ∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
simp : (¬n = 1 ∧ ¬n = 0) ∧ ∀ x < padicValNat p n, ¬p ^ (x + 1) = n
⊢ {n} ⊆ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))

Tactic:
simp only [singleton_subset_iff, mem_sdiff, mem_erase, Ne, mem_divisors, dvd_refl,
        true_and, mem_image, mem_range, not_exists, not_and]

Premises used: Finset.mem_image, Nat.mem_divisors, not_exists, Finset.singleton_subset_iff, Ne, Finset.mem_range, Finset.mem_sdiff, Finset.mem_erase, not_and, dvd_refl, true_and
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      ∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ (¬n = 1 ∧ ¬n = 0) ∧ ∀ x < padicValNat p n, ¬p ^ (x + 1) = n

Tactic:
⟨⟨hn.ne', hn'.ne'⟩, fun t _ => h hp _⟩

Premises used: LT.lt.ne', HAdd.hAdd, And.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      ∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ (¬n = 1 ∧ ¬n = 0) ∧ ∀ x < padicValNat p n, ¬p ^ (x + 1) = n

Tactic:
exact ⟨⟨hn.ne', hn'.ne'⟩, fun t _ => h hp _⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      HMul.hMul (α := ℤ)
        (∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
        (∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))
⊢ (↑p : ℤ) ∣ eval 1 (cyclotomic n ℤ)

Tactic:
rw [← Int.natAbs_natCast p, Int.natAbs_dvd_natAbs] at hpe

Premises used: Int.natAbs_dvd_natAbs, Int.natAbs_natCast
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      HMul.hMul (α := ℤ)
        (∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
        (∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))
hpe₁ : (↑p : ℤ) ∣ eval 1 (cyclotomic n ℤ)
⊢ Fact (Nat.Prime p)

Tactic:
rw [← Int.natAbs_natCast p, Int.natAbs_dvd_natAbs] at hpe

Premises used: Int.natAbs_dvd_natAbs, Int.natAbs_natCast
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      HMul.hMul (α := ℤ)
        (∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
        (∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))
hpe₁ : (↑p : ℤ) ∣ eval 1 (cyclotomic n ℤ)
this₁ : Fact (Nat.Prime p)
⊢ (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      HMul.hMul (α := ℤ)
        (∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
        (∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))

Tactic:
rw [← Int.natAbs_natCast p, Int.natAbs_dvd_natAbs] at hpe

Premises used: Int.natAbs_dvd_natAbs, Int.natAbs_natCast
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : (↑p : ℤ) ∣ eval 1 (cyclotomic n ℤ)
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      HMul.hMul (α := ℤ)
        (∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
        (∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))
obtain : ∀ (t : ℤ) (ht : eval 1 (cyclotomic n ℤ) = (↑p : ℤ) * t), False
⊢ False

Tactic:
obtain ⟨t, ht⟩ := hpe
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      HMul.hMul (α := ℤ)
        (∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
        (∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))
t : ℤ
ht : eval 1 (cyclotomic n ℤ) = (↑p : ℤ) * t
rw :
  ∀ (t : ℤ)
    (this :
      (↑n : ℤ) =
        HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) * (↑p : ℤ) *
          (t *
            ∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
              eval 1 (cyclotomic x ℤ)))
    (ht : eval 1 (cyclotomic n ℤ) = (↑p : ℤ) * t), False
⊢ False

Tactic:
rw [Finset.prod_singleton, ht, mul_left_comm, mul_comm, ← mul_assoc, mul_assoc] at this

Premises used: Finset.prod_singleton, mul_assoc, mul_left_comm, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this_1 : Fact (Nat.Prime p)
t : ℤ
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) * (↑p : ℤ) *
      (t *
        ∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
ht : eval 1 (cyclotomic n ℤ) = (↑p : ℤ) * t
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) * (↑p : ℤ) ∣ (↑n : ℤ)

Tactic:
have : (p : ℤ) ^ padicValNat p n * p ∣ n := ⟨_, this⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this_1 : Fact (Nat.Prime p)
t : ℤ
this_2 :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) * (↑p : ℤ) *
      (t *
        ∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
ht : eval 1 (cyclotomic n ℤ) = (↑p : ℤ) * t
this : HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) * (↑p : ℤ) ∣ (↑n : ℤ)
⊢ p ^ (padicValNat p n + 1) ∣ n

Tactic:
simp only [← _root_.pow_succ, ← Int.natAbs_dvd_natAbs, Int.natAbs_natCast,
      Int.natAbs_pow] at this

Premises used: pow_succ, Int.natAbs_pow, Int.natAbs_dvd_natAbs, Int.natAbs_natCast
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this_1 : Fact (Nat.Prime p)
t : ℤ
this_2 :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) * (↑p : ℤ) *
      (t *
        ∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
ht : eval 1 (cyclotomic n ℤ) = (↑p : ℤ) * t
this : p ^ (padicValNat p n + 1) ∣ n
⊢ False

Tactic:
pow_succ_padicValNat_not_dvd hn'.ne' this

Premises used: pow_succ_padicValNat_not_dvd, LT.lt.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this_1 : Fact (Nat.Prime p)
t : ℤ
this_2 :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) * (↑p : ℤ) *
      (t *
        ∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
ht : eval 1 (cyclotomic n ℤ) = (↑p : ℤ) * t
this : p ^ (padicValNat p n + 1) ∣ n
⊢ False

Tactic:
exact pow_succ_padicValNat_not_dvd hn'.ne' this

Premises used: pow_succ_padicValNat_not_dvd, LT.lt.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HMul.hMul (α := ℤ)
      (∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ))
      (∏ x ∈ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ))
x y : ℕ
hxy : Eq (α := ℕ) ((fun (t : ℕ) ↦ p ^ (t + 1)) x) ((fun (t : ℕ) ↦ p ^ (t + 1)) y)
a : x.succ = y.succ
⊢ x = y

Tactic:
apply Nat.succ_injective

Premises used: Nat.succ_injective
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HMul.hMul (α := ℤ)
      (∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ))
      (∏ x ∈ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ))
x y : ℕ
hxy : Eq (α := ℕ) ((fun (t : ℕ) ↦ p ^ (t + 1)) x) ((fun (t : ℕ) ↦ p ^ (t + 1)) y)
⊢ x.succ = y.succ

Tactic:
Nat.pow_right_injective hp.two_le hxy

Premises used: Nat.pow_right_injective, Nat.Prime.two_le
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HMul.hMul (α := ℤ)
      (∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ))
      (∏ x ∈ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ))
x y : ℕ
hxy : Eq (α := ℕ) ((fun (t : ℕ) ↦ p ^ (t + 1)) x) ((fun (t : ℕ) ↦ p ^ (t + 1)) y)
⊢ x.succ = y.succ

Tactic:
exact Nat.pow_right_injective hp.two_le hxy

Premises used: Nat.pow_right_injective, Nat.Prime.two_le
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
⊢ 0 < n

Tactic:
have hn : 0 < n := pos_of_gt hn'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
⊢ 0 < q

Tactic:
have hq := zero_lt_one.trans hq'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : ζ' ∈ primitiveRoots n ℂ
⊢ IsPrimitiveRoot ζ' n

Tactic:
rw [mem_primitiveRoots hn] at hζ'

Premises used: mem_primitiveRoots
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ ‖(↑q : ℂ)‖ - ‖ζ'‖ ≤ ‖(↑q : ℂ) - ζ'‖

Tactic:
norm_sub_norm_le (↑q) ζ'

Premises used: norm_sub_norm_le
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
h : q = ‖(↑q : ℂ)‖
h₁ : 1 = ‖ζ'‖
⊢ q - 1 ≤ ‖(↑q : ℂ) - ζ'‖

Tactic:
convert! norm_sub_norm_le (↑q) ζ'

Premises used: norm_sub_norm_le
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
h : q = ‖q‖
h₁ h₂ : q = q
⊢ q = ‖(↑q : ℂ)‖

Tactic:
rw [Complex.norm_real, Real.norm_of_nonneg hq.le]

Premises used: LT.lt.le, Complex.norm_real, Real.norm_of_nonneg
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
h h₁ : Eq (α := ℝ) 1 1
⊢ 1 = ‖ζ'‖

Tactic:
rw [hζ'.norm'_eq_one hn.ne']

Premises used: LT.lt.ne', IsPrimitiveRoot.norm'_eq_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
⊢ ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖

Tactic:
have hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖ := by
    intro ζ' hζ'
    rw [mem_primitiveRoots hn] at hζ'
    convert! norm_sub_norm_le (↑q) ζ'
    · rw [Complex.norm_real, Real.norm_of_nonneg hq.le]
    · rw [hζ'.norm'_eq_one hn.ne']
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
⊢ IsPrimitiveRoot ζ n

Tactic:
have hζ : IsPrimitiveRoot ζ n := Complex.isPrimitiveRoot_exp n hn.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
⊢ ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖

Tactic:
⟨ζ, (mem_primitiveRoots hn).mpr hζ, ?_⟩

Premises used: Iff.mpr, And.intro, mem_primitiveRoots, Exists.intro
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
refine : q - 1 < ‖(↑q : ℂ) - ζ‖
⊢ ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖

Tactic:
refine ⟨ζ, (mem_primitiveRoots hn).mpr hζ, ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q : ℂ) ζ
⊢ ‖(↑q : ℂ)‖ - ‖ζ‖ < ‖(↑q : ℂ) - ζ‖

Tactic:
lt_norm_sub_of_not_sameRay this

Premises used: lt_norm_sub_of_not_sameRay
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q : ℂ) ζ
h : q = ‖(↑q : ℂ)‖
h₁ : 1 = ‖ζ‖
⊢ q - 1 < ‖(↑q : ℂ) - ζ‖

Tactic:
convert! lt_norm_sub_of_not_sameRay this

Premises used: lt_norm_sub_of_not_sameRay
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q : ℂ) ζ
⊢ q = ‖(↑q : ℂ)‖

Tactic:
simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]

Premises used: LT.lt.le, Complex.norm_real, LT.lt.ne', IsPrimitiveRoot.norm'_eq_one, Real.norm_of_nonneg
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q : ℂ) ζ
⊢ 1 = ‖ζ‖

Tactic:
simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]

Premises used: LT.lt.le, Complex.norm_real, LT.lt.ne', IsPrimitiveRoot.norm'_eq_one, Real.norm_of_nonneg
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
suffices : ¬SameRay ℝ (↑q : ℂ) ζ
⊢ q - 1 < ‖(↑q : ℂ) - ζ‖

Tactic:
suffices ¬SameRay ℝ (q : ℂ) ζ by
      convert! lt_norm_sub_of_not_sameRay this <;>
        simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
rw : ¬((↑q : ℂ) = 0 ∨ ζ = 0 ∨ (↑q : ℂ).arg = ζ.arg)
⊢ ¬SameRay ℝ (↑q : ℂ) ζ

Tactic:
rw [Complex.sameRay_iff]

Premises used: Complex.sameRay_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
push : (↑q : ℂ) ≠ 0 ∧ ζ ≠ 0 ∧ (↑q : ℂ).arg ≠ ζ.arg
⊢ ¬((↑q : ℂ) = 0 ∨ ζ = 0 ∨ (↑q : ℂ).arg = ζ.arg)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
⊢ (↑q : ℂ) ≠ 0 ∧ ζ ≠ 0 ∧ (↑q : ℂ).arg ≠ ζ.arg

Tactic:
⟨mod_cast hq.ne', hζ.ne_zero hn.ne', ?_⟩

Premises used: congrArg, cast, Ne, Complex.ofReal, LT.lt.ne', And.intro, Nat.cast_zero, IsPrimitiveRoot.ne_zero, Eq.symm, Eq, Not, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
refine : (↑q : ℂ).arg ≠ ζ.arg
⊢ (↑q : ℂ) ≠ 0 ∧ ζ ≠ 0 ∧ (↑q : ℂ).arg ≠ ζ.arg

Tactic:
refine ⟨mod_cast hq.ne', hζ.ne_zero hn.ne', ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
rw : ¬ζ = 1
⊢ (↑q : ℂ).arg ≠ ζ.arg

Tactic:
rw [Complex.arg_ofReal_of_nonneg hq.le, Ne, eq_comm, hζ.arg_eq_zero_iff hn.ne']

Premises used: Complex.arg_ofReal_of_nonneg, LT.lt.le, Ne, IsPrimitiveRoot.arg_eq_zero_iff, eq_comm, LT.lt.ne'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
clear_value : ∀ (ζ : ℂ) (hζ : IsPrimitiveRoot ζ n), ¬ζ = 1
⊢ ¬ζ = 1

Tactic:
clear_value ζ
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
hζ : IsPrimitiveRoot (M := ℂ) 1 n
linarith : -1 + HSub.hSub (α := ℤ) 2 (↑n : ℤ) + HSub.hSub (α := ℤ) (↑n : ℤ) 1 = 0
⊢ False

Tactic:
linarith [hζ.unique IsPrimitiveRoot.one]

Premises used: IsPrimitiveRoot.one, IsPrimitiveRoot.unique
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
⊢ ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖

Tactic:
have hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖ := by
    refine ⟨ζ, (mem_primitiveRoots hn).mpr hζ, ?_⟩
    suffices ¬SameRay ℝ (q : ℂ) ζ by
      convert! lt_norm_sub_of_not_sameRay this <;>
        simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]
    rw [Complex.sameRay_iff]
    push Not
    refine ⟨mod_cast hq.ne', hζ.ne_zero hn.ne', ?_⟩
    rw [Complex.arg_ofReal_of_nonneg hq.le, Ne, eq_comm, hζ.arg_eq_zero_iff hn.ne']
    clear_value ζ
    rintro rfl
    linarith [hζ.unique IsPrimitiveRoot.one]