awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
⊢ ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0

Tactic:
simpa using (cyclotomic_pos' n hq').ne'

Premises used: Polynomial.cyclotomic_pos', 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
⊢ ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0

Tactic:
have : ¬eval (↑q) (cyclotomic n ℂ) = 0 := by simpa using (cyclotomic_pos' n hq').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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
⊢ (q - 1).toNNReal ≠ 0

Tactic:
simp [hq']
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
⊢ ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖₊ ≠ 0

Tactic:
simp_all
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this_1 : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
this : Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < Units.mk0 ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖₊ ⋯
⊢ (q - 1) ^ φ n < ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖

Tactic:
simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe,
      hq'.le, coe_nnnorm, NNReal.coe_pow, Real.coe_toNNReal', sub_nonneg, sup_of_le_left] at this

Premises used: Real.coe_toNNReal', LT.lt.le, coe_nnnorm, NNReal.coe_pow, NNReal.coe_lt_coe, Units.val_pow_eq_pow_val, Units.val_lt_val, Units.val_mk0, sub_nonneg, sup_of_le_left
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this_1 : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
this : (q - 1) ^ φ n < ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖
⊢ (q - 1) ^ φ n < ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖

Tactic:
this
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this_1 : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
this : (q - 1) ^ φ n < ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖
h : eval q (cyclotomic n ℝ) = ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)

Tactic:
convert! this
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this_1 : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
this : (q - 1) ^ φ n < ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖
h : ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖ = eval q (cyclotomic n ℝ)
⊢ eval q (cyclotomic n ℝ) = ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this_1 : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
this : (q - 1) ^ φ n < ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖
⊢ ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖ = eval q (cyclotomic n ℝ)

Tactic:
simp [cyclotomic_nonneg n hq'.le]

Premises used: LT.lt.le, Polynomial.cyclotomic_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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
suffices : Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < Units.mk0 ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖₊ ⋯
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)

Tactic:
suffices Units.mk0 (Real.toNNReal (q - 1)) (by simp [hq']) ^ totient n <
      Units.mk0 ‖(cyclotomic n ℂ).eval ↑q‖₊ (by simp_all) by
    simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe,
      hq'.le, coe_nnnorm, NNReal.coe_pow, Real.coe_toNNReal', sub_nonneg, sup_of_le_left] at this
    convert! this
    rw [eq_comm]
    simp [cyclotomic_nonneg n hq'.le]
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
simp : Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯
⊢ Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < Units.mk0 ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖₊ ⋯

Tactic:
simp only [cyclotomic_eq_prod_X_sub_primitiveRoots hζ, eval_prod, eval_C, eval_X, eval_sub,
    nnnorm_prod, Units.mk0_prod]

Premises used: Polynomial.eval_prod, Polynomial.eval_C, Polynomial.eval_X, Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots, nnnorm_prod, Units.mk0_prod, Polynomial.eval_sub
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
⊢ LT.lt (α := NNRealˣ) (∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal ⋯)
    (∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯)

Tactic:
Finset.prod_lt_prod' (M := NNRealˣ) _ _

Premises used: Finset.prod_lt_prod'
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
h : Units.mk0 (q - 1).toNNReal ⋯ ^ φ n = ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal ⋯
convert_2 : ↥(primitiveRoots n ℂ) → NNRealˣ
convert_5 : ∀ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal ⋯ ≤ Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯
convert_6 : ∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal ⋯ < Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯
⊢ Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯

Tactic:
convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _

Premises used: Finset.prod_lt_prod'
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
x : ↥(primitiveRoots n ℂ)
⊢ (q - 1).toNNReal ≠ 0

Tactic:
simp [hq']
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
⊢ ↥(primitiveRoots n ℂ) → NNRealˣ

Tactic:
exact fun _ => Units.mk0 (Real.toNNReal (q - 1)) (by simp [hq'])

Premises used: HSub.hSub, Units.mk0, OfNat.ofNat, Real.toNNReal
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
⊢ Units.mk0 (q - 1).toNNReal ⋯ ^ φ n = ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal ⋯

Tactic:
simp only [Complex.card_primitiveRoots, prod_const, card_attach]

Premises used: Finset.prod_const, Finset.card_attach, Complex.card_primitiveRoots
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
convert_5 : ∀ (a : ℂ) (b : a ∈ primitiveRoots n ℂ), q ≤ ‖(↑q : ℂ) - a‖ + 1 ∧ True
⊢ ∀ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal ⋯ ≤ Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯

Tactic:
simp only [Finset.mem_attach, forall_true_left, Subtype.forall, ←
      Units.val_le_val, ← NNReal.coe_le_coe, norm_nonneg, Units.val_mk0,
      Real.coe_toNNReal', coe_nnnorm, max_le_iff, tsub_le_iff_right]

Premises used: forall_true_left, Real.coe_toNNReal', Finset.mem_attach, Units.val_le_val, Subtype.forall, max_le_iff, tsub_le_iff_right, coe_nnnorm, Units.val_mk0, NNReal.coe_le_coe, norm_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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
x : ℂ
hx : x ∈ primitiveRoots n ℂ
⊢ q ≤ ‖(↑q : ℂ) - x‖ + 1 ∧ True

Tactic:
simpa only [and_true, tsub_le_iff_right] using hfor x hx

Premises used: and_true, tsub_le_iff_right
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
convert_6 : ∃ (a : ℂ) (_ : a ∈ primitiveRoots n ℂ), True ∧ (↑(q - 1).toNNReal : ℝ) < ‖(↑q : ℂ) - a‖
⊢ ∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal ⋯ < Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯

Tactic:
simp only [Finset.mem_attach, Subtype.exists, ←
      NNReal.coe_lt_coe, ← Units.val_lt_val, Units.val_mk0 _, coe_nnnorm]

Premises used: Finset.mem_attach, Subtype.exists, coe_nnnorm, NNReal.coe_lt_coe, Units.val_lt_val, Units.val_mk0
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
⊢ ∃ (a : ℂ) (_ : a ∈ primitiveRoots n ℂ), True ∧ (↑(q - 1).toNNReal : ℝ) < ‖(↑q : ℂ) - a‖

Tactic:
simpa [hq'.le, Real.coe_toNNReal', max_eq_left, sub_nonneg] using hex

Premises used: Real.coe_toNNReal', LT.lt.le, max_eq_left, sub_nonneg
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
q : ℝ
hq' : 1 < q
⊢ (q - 1) ^ φ 0 ≤ eval q (cyclotomic 0 ℝ)

Tactic:
simp only [totient_zero, _root_.pow_zero, cyclotomic_zero, eval_one, le_refl]

Premises used: le_refl, Nat.totient_zero, Polynomial.cyclotomic_zero, pow_zero, Polynomial.eval_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
q : ℝ
hq' : 1 < q
⊢ (q - 1) ^ φ 1 ≤ eval q (cyclotomic 1 ℝ)

Tactic:
simp only [totient_one, pow_one, cyclotomic_one, eval_sub, eval_X, eval_one, le_refl]

Premises used: le_refl, Polynomial.eval_X, Polynomial.cyclotomic_one, pow_one, Polynomial.eval_one, Polynomial.eval_sub, Nat.totient_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 3 ≤ 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' : 3 ≤ 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' : 3 ≤ 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' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ ‖(↑q : ℂ) - ζ'‖ ≤ ‖(↑q : ℂ)‖ + ‖ζ'‖

Tactic:
norm_sub_le (↑q) ζ'

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

Tactic:
convert! norm_sub_le (↑q) ζ'

Premises used: norm_sub_le
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 3 ≤ 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 (zero_le_one.trans_lt hq').le]

Premises used: LT.lt.le, Complex.norm_real, zero_le_one, LE.le.trans_lt, Real.norm_of_nonneg
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 3 ≤ 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' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
⊢ ∀ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ ≤ q + 1

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

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' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
refine : ‖(↑q : ℂ) - ζ‖ < q + 1
⊢ ∃ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ < q + 1

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

Tactic:
norm_add_lt_of_not_sameRay this

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

Tactic:
convert! norm_add_lt_of_not_sameRay this using 2

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

Tactic:
rw [Complex.norm_real]

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

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

Tactic:
abs_eq_self.mpr hq.le

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

Tactic:
exact abs_eq_self.mpr hq.le

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

Tactic:
simp [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' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
suffices : ¬SameRay ℝ (↑q : ℂ) (-ζ)
⊢ ‖(↑q : ℂ) - ζ‖ < q + 1

Tactic:
suffices ¬SameRay ℝ (q : ℂ) (-ζ) by
      convert! norm_add_lt_of_not_sameRay this using 2
      · rw [Complex.norm_real]
        symm
        exact abs_eq_self.mpr hq.le
      · simp [hζ.norm'_eq_one hn.ne']
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ ≤ q + 1
ζ : ℂ := 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' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ ≤ q + 1
ζ : ℂ := 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' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
⊢ (↑q : ℂ) ≠ 0 ∧ -ζ ≠ 0 ∧ (↑q : ℂ).arg ≠ (-ζ).arg

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

Premises used: Iff.mpr, congrArg, cast, Ne, Complex.ofReal, LT.lt.ne', And.intro, neg_ne_zero, 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' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ ≤ q + 1
ζ : ℂ := 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', neg_ne_zero.mpr <| hζ.ne_zero hn.ne', ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
rw : ¬(-ζ).arg = 0
⊢ (↑q : ℂ).arg ≠ (-ζ).arg

Tactic:
rw [Complex.arg_ofReal_of_nonneg hq.le, Ne, eq_comm]

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

Tactic:
rw [Complex.arg_eq_zero_iff, Complex.neg_re, neg_nonneg, Complex.neg_im, neg_eq_zero] at h

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

Tactic:
clear_value ζ
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ ≤ q + 1
hζ : IsPrimitiveRoot (M := ℂ) 0 n
h : Complex.re 0 ≤ 0 ∧ Complex.im 0 = 0
⊢ False

Tactic:
hn.ne' (hζ.unique IsPrimitiveRoot.zero)

Premises used: LT.lt.ne', IsPrimitiveRoot.zero, IsPrimitiveRoot.unique
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ ≤ q + 1
hζ : IsPrimitiveRoot (M := ℂ) 0 n
h : Complex.re 0 ≤ 0 ∧ Complex.im 0 = 0
⊢ False

Tactic:
exact hn.ne' (hζ.unique IsPrimitiveRoot.zero)

Premises used: LT.lt.ne', IsPrimitiveRoot.zero, IsPrimitiveRoot.unique