awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
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
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
have hex : ∃ ζ' ∈ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
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 ℝ) < (q + 1) ^ φ n
have this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
Tactic: have : ¬eval (↑q) (cyclotomic n ℂ) = 0 := by simpa using (cyclotomic_pos' n hq').ne.symm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ (q + 1).toNNReal ≠ 0
have simp : 0 < q + 1
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ 0 < q + 1
have linarith : q + 1 ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - q) + (q + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ 0 < q + 1
have linarith₁ : q + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
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 ℝ) < (q + 1) ^ φ n
have this₁ : ‖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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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 ℝ) < (q + 1) ^ φ n
have h : eval q (cyclotomic n ℝ) = ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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 ℝ) < (q + 1) ^ φ n
have h₁ : q + 1 = max (q + 1) 0
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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 ℂ)‖
have h : ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖ = eval q (cyclotomic n ℝ)
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ q + 1 = max (q + 1) 0
have h : 0 ≤ q + 1
Tactic: rw [eq_comm, max_eq_left_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ 0 ≤ q + 1
have linarith : q + 1 < 0 → HMul.hMul (α := ℝ) 2 (-1) + (1 - q) + (q + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ 0 ≤ q + 1
have linarith₁ : q + 1 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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 ℝ) < (q + 1) ^ φ n
have suffices : Units.mk0 ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖₊ sorry < Units.mk0 (q + 1).toNNReal sorry ^ φ 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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 ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖₊ ⋯ < Units.mk0 (q + 1).toNNReal ⋯ ^ φ n
have simp : ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ sorry < Units.mk0 (q + 1).toNNReal sorry ^ φ n
Tactic: simp only [cyclotomic_eq_prod_X_sub_primitiveRoots hζ, eval_prod, eval_C, eval_X, eval_sub,
    nnnorm_prod, Units.mk0_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯ < Units.mk0 (q + 1).toNNReal ⋯ ^ φ n
have h : Units.mk0 (q + 1).toNNReal sorry ^ φ n = ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q + 1).toNNReal sorry
Tactic: convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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 ⋯
⊢ ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯ < Units.mk0 (q + 1).toNNReal ⋯ ^ φ n
have convert_3 : ↥(primitiveRoots n ℂ) → NNRealˣ
Tactic: convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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ˣ
⊢ ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯ < Units.mk0 (q + 1).toNNReal ⋯ ^ φ n
have convert_5 : ∀ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ sorry ≤ Units.mk0 (q + 1).toNNReal sorry
Tactic: convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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 ⋯
⊢ ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯ < Units.mk0 (q + 1).toNNReal ⋯ ^ φ n
have convert_6 : ∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ sorry < Units.mk0 (q + 1).toNNReal sorry
Tactic: convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ ∀ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯ ≤ Units.mk0 (q + 1).toNNReal ⋯
have convert_5 : ∀ (a : ℂ) (b : a ∈ primitiveRoots n ℂ), ‖(↑q : ℂ) - a‖ ≤ (↑(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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
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).toNNReal : ℝ)
have this₁ : ‖(↑q : ℂ) - x‖ ≤ q + 1
Tactic: have : ‖_‖ ≤ _ := hfor x hx
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ ∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯ < Units.mk0 (q + 1).toNNReal ⋯
have convert_6 : ∃ (a : ℂ) (_ : a ∈ primitiveRoots n ℂ), True ∧ ‖(↑q : ℂ) - a‖ < (↑(q + 1).toNNReal : ℝ)
Tactic: simp only [Finset.mem_attach, Subtype.exists, ←
      NNReal.coe_lt_coe, ← Units.val_lt_val, Units.val_mk0 _, coe_nnnorm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ ∃ (a : ℂ) (_ : a ∈ primitiveRoots n ℂ), True ∧ ‖(↑q : ℂ) - a‖ < (↑(q + 1).toNNReal : ℝ)
have convert_6 : ∀ (ζ : ℂ) (hζ : ζ ∈ primitiveRoots n ℂ) (hhζ : ‖(↑q : ℂ) - ζ‖ < q + 1),
  ∃ (a : ℂ) (_ : a ∈ primitiveRoots n ℂ), True ∧ ‖(↑q : ℂ) - a‖ < (↑(q + 1).toNNReal : ℝ)
Tactic: obtain ⟨ζ, hζ, hhζ : ‖_‖ < _⟩ := hex
Cleared hypotheses: hex
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
⊢ (q - 1) ^ φ n < (eval (↑q : ℤ) (cyclotomic n ℤ)).natAbs
have inl : ∀ (hq : Ne (α := ℕ) 0 1), HSub.hSub (α := ℕ) 0 1 ^ φ n < (eval (↑0 : ℤ) (cyclotomic n ℤ)).natAbs
Tactic: rcases hq.lt_or_gt.imp_left Nat.lt_one_iff.mp with (rfl | hq')
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
inl : ∀ (hq : Ne (α := ℕ) 0 1), HSub.hSub (α := ℕ) 0 1 ^ φ n < (eval (↑0 : ℤ) (cyclotomic n ℤ)).natAbs
⊢ (q - 1) ^ φ n < (eval (↑q : ℤ) (cyclotomic n ℤ)).natAbs
have inr : ∀ (hq' : 1 < q), (q - 1) ^ φ n < (eval (↑q : ℤ) (cyclotomic n ℤ)).natAbs
Tactic: rcases hq.lt_or_gt.imp_left Nat.lt_one_iff.mp with (rfl | hq')
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n : ℕ
hn' : 1 < n
hq : Ne (α := ℕ) 0 1
⊢ HSub.hSub (α := ℕ) 0 1 ^ φ n < (eval (↑0 : ℤ) (cyclotomic n ℤ)).natAbs
have inl : Ne (α := ℤ) 1 0
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']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (q - 1) ^ φ n < (eval (↑q : ℤ) (cyclotomic n ℤ)).natAbs
have inr : HSub.hSub (α := ℝ) (↑q : ℝ) 1 ^ φ n < (↑|eval (↑q : ℤ) (cyclotomic n ℤ)| : ℝ)
Tactic: rw [← @Nat.cast_lt ℝ, Nat.cast_pow, Nat.cast_sub hq'.le, Nat.cast_one, Nat.cast_natAbs]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 ^ φ n < (↑|eval (↑q : ℤ) (cyclotomic n ℤ)| : ℝ)
have inr : eval (↑q : ℝ) (cyclotomic n ℝ) ≤ (↑|eval (↑q : ℤ) (cyclotomic n ℤ)| : ℝ)
Tactic: refine (sub_one_pow_totient_lt_cyclotomic_eval hn' (Nat.one_lt_cast.2 hq')).trans_le ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ eval (↑q : ℝ) (cyclotomic n ℝ) ≤ (↑|eval (↑q : ℤ) (cyclotomic n ℤ)| : ℝ)
have h : Eq (α := ℝ) ((↑|eval (↑q : ℤ) (cyclotomic n ℤ)| : ℝ) : ℝ)
  (|(algebraMap ℤ ℝ : (a : ℤ) → ℝ) (eval (↑q : ℤ) (cyclotomic n ℤ))| : ℝ)
Tactic: convert! (cyclotomic.eval_apply (q : ℤ) n (algebraMap ℤ ℝ)).trans_le (le_abs_self _)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
have inl : ∀ (hdiv : ¬p ∣ 0),
  (expand R p : (a : R[X]) → R[X]) (cyclotomic 0 R) = HMul.hMul (α := R[X]) (cyclotomic (0 * p) R) (cyclotomic 0 R)
Tactic: rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
Cleared hypotheses: n, hdiv
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
inl :
  ∀ (hdiv : ¬p ∣ 0),
    (expand R p : (a : R[X]) → R[X]) (cyclotomic 0 R) = HMul.hMul (α := R[X]) (cyclotomic (0 * p) R) (cyclotomic 0 R)
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
have inr : ∀ (hnpos : n > 0),
  (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
Tactic: rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (hypothesis)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
have this : NeZero n
Tactic: haveI := NeZero.of_pos hnpos
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this_1 : NeZero n
this : (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
have rw : (expand R p : (a : R[X]) → R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) =
  HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
Tactic: rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int,
      map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this_1 : NeZero n
this : (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
rw :
  (expand R p : (a : R[X]) → R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) =
    HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
have rw₁ : map (R := ℤ) (Int.castRingHom R) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) =
  HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
Tactic: rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int,
      map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this_1 : NeZero n
this : (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
rw :
  (expand R p : (a : R[X]) → R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) =
    HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
rw₁ :
  map (R := ℤ) (Int.castRingHom R) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) =
    HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
have rw₂ : map (Int.castRingHom R) (cyclotomic (n * p) ℤ * cyclotomic n ℤ) =
  HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
Tactic: rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int,
      map_cyclotomic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
Goal:
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst : CommRing R
hnpos : n > 0
this_1 : NeZero n
this : (expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ
rw :
  (expand R p : (a : R[X]) → R[X]) (map (Int.castRingHom R) (cyclotomic n ℤ)) =
    HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
rw₁ :
  map (R := ℤ) (Int.castRingHom R) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)) =
    HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
rw₂ :
  map (Int.castRingHom R) (cyclotomic (n * p) ℤ * cyclotomic n ℤ) =
    HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
⊢ (expand R p : (a : R[X]) → R[X]) (cyclotomic n R) = HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (cyclotomic n R)
have rw₃ : HMul.hMul (α := R[X]) (map (Int.castRingHom R) (cyclotomic (n * p) ℤ)) (map (Int.castRingHom R) (cyclotomic n ℤ)) =
  HMul.hMul (α := R[X]) (cyclotomic (n * p) R) (map (Int.castRingHom R) (cyclotomic n ℤ))
Tactic: rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int,
      map_cyclotomic]