awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ζ ≠ 0

Tactic:
have hζ₀ : ζ ≠ 0 := by
      clear_value ζ
      rintro rfl
      exact hn.ne' (hζ.unique IsPrimitiveRoot.zero)
-- 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
hζ₀ : ζ ≠ 0
refine_2 : ∀ (this : ζ.re < 0 ∧ ζ.im = 0), False
refine_1 : ζ.re ≠ 0
⊢ False

Tactic:
have : ζ.re < 0 ∧ ζ.im = 0 := ⟨h.1.lt_of_ne ?_, h.2⟩
-- 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
hζ₀ : ζ ≠ 0
this : ζ.re < 0 ∧ ζ.im = 0
⊢ ζ = -1

Tactic:
rw [← Complex.arg_eq_pi_iff, hζ.arg_eq_pi_iff hn.ne'] at this

Premises used: LT.lt.ne', Complex.arg_eq_pi_iff, IsPrimitiveRoot.arg_eq_pi_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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
this : ζ = -1
⊢ IsPrimitiveRoot (M := ℂ) (-1) n

Tactic:
rw [this] at 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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
this : ζ = -1
hζ₁ : IsPrimitiveRoot (M := ℂ) (-1) n
⊢ ζ.re ≤ 0 ∧ ζ.im = 0

Tactic:
rw [this] at 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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
this : ζ = -1
hζ₁ : IsPrimitiveRoot (M := ℂ) (-1) n
h₁ : ζ.re ≤ 0 ∧ ζ.im = 0
⊢ ζ ≠ 0

Tactic:
rw [this] at 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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
this : ζ = -1
hζ₁ : IsPrimitiveRoot (M := ℂ) (-1) n
h₁ : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₂ : ζ ≠ 0
⊢ ζ = -1

Tactic:
rw [this] at 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 (M := ℂ) (-1) n
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
this : ζ = -1
linarith : -1 + HSub.hSub (α := ℤ) 3 (↑n : ℤ) + HSub.hSub (α := ℤ) (↑n : ℤ) 2 = 0
⊢ False

Tactic:
linarith [hζ.unique <| IsPrimitiveRoot.neg_one 0 two_ne_zero.symm]

Premises used: Ne.symm, two_ne_zero, IsPrimitiveRoot.neg_one, IsPrimitiveRoot.unique, OfNat.ofNat
-- 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
hζ₀ : ζ ≠ 0
refine_1 : ∀ (hζ₀ : ζ.re = 0), ζ = 0
⊢ ζ.re ≠ 0

Tactic:
contrapose 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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ.re = 0
refine_1 : ζ.re = Complex.re 0
refine_1₁ : ζ.im = Complex.im 0
⊢ ζ = 0

Tactic:
apply Complex.ext

Premises used: Complex.ext
-- 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
hζ₀ : ζ.re = 0
⊢ ζ.re = Complex.re 0

Tactic:
simp [hζ₀, h.2]

Premises used: And.right
-- 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
hζ₀ : ζ.re = 0
⊢ ζ.im = Complex.im 0

Tactic:
simp [hζ₀, h.2]

Premises used: And.right
-- 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:
have hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1 := by
    refine ⟨ζ, (mem_primitiveRoots hn).mpr hζ, ?_⟩
    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']
    rw [Complex.sameRay_iff]
    push Not
    refine ⟨mod_cast hq.ne', neg_ne_zero.mpr <| hζ.ne_zero hn.ne', ?_⟩
    rw [Complex.arg_ofReal_of_nonneg hq.le, Ne, eq_comm]
    intro h
    rw [Complex.arg_eq_zero_iff, Complex.neg_re, neg_nonneg, Complex.neg_im, neg_eq_zero] at h
    have hζ₀ : ζ ≠ 0 := by
      clear_value ζ
      rintro rfl
      exact hn.ne' (hζ.unique IsPrimitiveRoot.zero)
    have : ζ.re < 0 ∧ ζ.im = 0 := ⟨h.1.lt_of_ne ?_, h.2⟩
    · rw [← Complex.arg_eq_pi_iff, hζ.arg_eq_pi_iff hn.ne'] at this
      rw [this] at hζ
      linarith [hζ.unique <| IsPrimitiveRoot.neg_one 0 two_ne_zero.symm]
    · contrapose hζ₀
      apply Complex.ext <;> simp [hζ₀, h.2]
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ < q + 1
⊢ ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0

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

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

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

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

Tactic:
simp
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ < q + 1
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
linarith : q + 1 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - q) + (q + 1 - 0) = 0
linarith₁ : q + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < q + 1

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

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

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

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

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

Tactic:
rw [eq_comm, max_eq_left_iff]

Premises used: max_eq_left_iff, 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ < q + 1
this_1 : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
this : ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖ < max (q + 1) 0 ^ φ n
linarith : q + 1 < 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - q) + (q + 1 - 0) = 0
linarith₁ : q + 1 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ q + 1

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

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

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

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

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

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

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

Tactic:
exact fun _ => Units.mk0 (Real.toNNReal (q + 1)) (by positivity)

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

Tactic:
simp [Complex.card_primitiveRoots]

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

Tactic:
simp only [Finset.mem_attach, forall_true_left, Subtype.forall, ←
      Units.val_le_val, ← NNReal.coe_le_coe, Units.val_mk0,
      coe_nnnorm]

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

Tactic:
have : ‖_‖ ≤ _ := hfor x hx
-- 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ < q + 1
this_1 : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
x : ℂ
hx : x ∈ primitiveRoots n ℂ
this : ‖(↑q : ℂ) - x‖ ≤ q + 1
⊢ ‖(↑q : ℂ) - x‖ ≤ (↑(q + 1).toNNReal : ℝ)

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

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' : 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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ < q + 1
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
convert_6 :
  ∀ (ζ : ℂ) (hζ : ζ ∈ primitiveRoots n ℂ) (hhζ : ‖(↑q : ℂ) - ζ‖ < q + 1),
    ∃ (a : ℂ) (_ : a ∈ primitiveRoots n ℂ), True ∧ ‖(↑q : ℂ) - a‖ < (↑(q + 1).toNNReal : ℝ)
⊢ ∃ (a : ℂ) (_ : a ∈ primitiveRoots n ℂ), True ∧ ‖(↑q : ℂ) - a‖ < (↑(q + 1).toNNReal : ℝ)

Tactic:
obtain ⟨ζ, hζ, hhζ : ‖_‖ < _⟩ := hex
-- 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
ζ_1 : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ_1 : IsPrimitiveRoot ζ_1 n
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
ζ : ℂ
hζ : ζ ∈ primitiveRoots n ℂ
hhζ : ‖(↑q : ℂ) - ζ‖ < q + 1
⊢ True ∧ ‖(↑q : ℂ) - ζ‖ < (↑(q + 1).toNNReal : ℝ)

Tactic:
simp [hhζ]
-- 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
ζ_1 : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ_1 : IsPrimitiveRoot ζ_1 n
this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
ζ : ℂ
hζ : ζ ∈ primitiveRoots n ℂ
hhζ : ‖(↑q : ℂ) - ζ‖ < q + 1
⊢ ∃ (a : ℂ) (_ : a ∈ primitiveRoots n ℂ), True ∧ ‖(↑q : ℂ) - a‖ < (↑(q + 1).toNNReal : ℝ)

Tactic:
exact ⟨ζ, hζ, by simp [hhζ]⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
q : ℝ
hq' : 1 < q
⊢ eval q (cyclotomic 0 ℝ) ≤ (q + 1) ^ φ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
q : ℝ
hq' : 1 < q
⊢ eval q (cyclotomic 1 ℝ) ≤ (q + 1) ^ φ 1

Tactic:
simp [add_assoc, zero_le_one]

Premises used: add_assoc, zero_le_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
q : ℝ
hq' : 1 < q
⊢ eval q (cyclotomic 2 ℝ) ≤ (q + 1) ^ φ 2

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
inl : ∀ (hq : Ne (α := ℕ) 0 1), HSub.hSub (α := ℕ) 0 1 ^ φ n < (eval (↑0 : ℤ) (cyclotomic n ℤ)).natAbs
inr : ∀ (hq' : 1 < q), (q - 1) ^ φ n < (eval (↑q : ℤ) (cyclotomic n ℤ)).natAbs
⊢ (q - 1) ^ φ n < (eval (↑q : ℤ) (cyclotomic n ℤ)).natAbs

Tactic:
rcases hq.lt_or_gt.imp_left Nat.lt_one_iff.mp with (rfl | hq')

Premises used: Or.imp_left, Nat.lt_one_iff, Iff.mp, rfl, Ne.lt_or_gt
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn' : 1 < n
hq : Ne (α := ℕ) 0 1
inl : Ne (α := ℤ) 1 0
⊢ HSub.hSub (α := ℕ) 0 1 ^ φ n < (eval (↑0 : ℤ) (cyclotomic n ℤ)).natAbs

Tactic:
rw [zero_tsub, zero_pow (Nat.totient_pos.2 (pos_of_gt hn')).ne', pos_iff_ne_zero,
      Int.natAbs_ne_zero, Nat.cast_zero, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hn']

Premises used: Iff.mpr, Polynomial.coeff_zero_eq_eval_zero, pos_of_gt, Polynomial.cyclotomic_coeff_zero, LT.lt.ne', Nat.cast_zero, Nat.totient_pos, pos_iff_ne_zero, Int.natAbs_ne_zero, zero_pow, zero_tsub
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn' : 1 < n
hq : Ne (α := ℕ) 0 1
⊢ Ne (α := ℤ) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
Goal:
n : ℕ
hn' : 1 < n
hq : Ne (α := ℕ) 0 1
⊢ Ne (α := ℤ) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero