awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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)
have push : (↑q : ℂ) ≠ 0 ∧ ζ ≠ 0 ∧ (↑q : ℂ).arg ≠ ζ.arg
Tactic: push Not
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
have refine : (↑q : ℂ).arg ≠ ζ.arg
Tactic: refine ⟨mod_cast hq.ne', hζ.ne_zero hn.ne', ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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 : ℂ).arg ≠ ζ.arg
have rw : ¬ζ = 1
Tactic: rw [Complex.arg_ofReal_of_nonneg hq.le, Ne, eq_comm, hζ.arg_eq_zero_iff hn.ne']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ ¬ζ = 1
have clear_value : ∀ (ζ : ℂ) (hζ : IsPrimitiveRoot ζ n), ¬ζ = 1
Tactic: clear_value ζ
Cleared hypotheses: ζ, hζ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ False
have linarith : -1 + HSub.hSub (α := ℤ) 2 (↑n : ℤ) + HSub.hSub (α := ℤ) (↑n : ℤ) 1 = 0
Tactic: linarith [hζ.unique IsPrimitiveRoot.one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
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 - 1) ^ φ n < eval q (cyclotomic n ℝ)
have hex : ∃ ζ' ∈ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
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 : ℂ) - ζ'‖
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
have this : ¬eval (↑q : ℂ) (cyclotomic n ℂ) = 0
Tactic: have : ¬eval (↑q) (cyclotomic n ℂ) = 0 := by simpa using (cyclotomic_pos' n hq').ne'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
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 ℝ)
have this₁ : (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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 ℝ)
have h : eval q (cyclotomic n ℝ) = ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖
Tactic: convert! this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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 ℂ)‖
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' : 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) ^ φ n < eval q (cyclotomic n ℝ)
have suffices : Units.mk0 (q - 1).toNNReal sorry ^ φ n < Units.mk0 ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖₊ sorry
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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 < Units.mk0 ‖eval (↑q : ℂ) (cyclotomic n ℂ)‖₊ ⋯
have simp : Units.mk0 (q - 1).toNNReal sorry ^ φ n < ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ sorry
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' : 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 : ℂ) - (↑i : ℂ)‖₊ ⋯
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' : 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 ⋯
⊢ Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯
have convert_2 : ↥(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' : 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ˣ
⊢ Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯
have convert_5 : ∀ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal sorry ≤ Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ sorry
Tactic: convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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 : ℂ)‖₊ ⋯
⊢ Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯
have convert_6 : ∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal sorry < Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ sorry
Tactic: convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ ∀ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal ⋯ ≤ Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯
have convert_5 : ∀ (a : ℂ) (b : a ∈ primitiveRoots n ℂ), q ≤ ‖(↑q : ℂ) - a‖ + 1 ∧ True
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
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
⊢ ∃ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 (q - 1).toNNReal ⋯ < Units.mk0 ‖(↑q : ℂ) - (↑i : ℂ)‖₊ ⋯
have convert_6 : ∃ (a : ℂ) (_ : a ∈ primitiveRoots n ℂ), True ∧ (↑(q - 1).toNNReal : ℝ) < ‖(↑q : ℂ) - a‖
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 (hypothesis)
Goal:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
have hn : 0 < n
Tactic: have hn : 0 < n := pos_of_gt hn'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
have hq : 0 < q
Tactic: have hq := zero_lt_one.trans hq'
-- 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
ζ' : ℂ
hζ' : ζ' ∈ primitiveRoots n ℂ
⊢ ‖(↑q : ℂ) - ζ'‖ ≤ q + 1
have hζ'₁ : IsPrimitiveRoot ζ' n
Tactic: rw [mem_primitiveRoots hn] at hζ'
Cleared hypotheses: hζ'
-- 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
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ ‖(↑q : ℂ) - ζ'‖ ≤ q + 1
have h : q = ‖(↑q : ℂ)‖
Tactic: convert! norm_sub_le (↑q) ζ'
-- 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
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
h : q = ‖(↑q : ℂ)‖
⊢ ‖(↑q : ℂ) - ζ'‖ ≤ q + 1
have h₁ : 1 = ‖ζ'‖
Tactic: convert! norm_sub_le (↑q) ζ'
-- 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
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q = ‖(↑q : ℂ)‖
have h : q = ‖q‖
Tactic: rw [Complex.norm_real, Real.norm_of_nonneg (zero_le_one.trans_lt hq').le]
-- 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
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
h : q = ‖q‖
⊢ q = ‖(↑q : ℂ)‖
have h₁ : q = q
Tactic: rw [Complex.norm_real, Real.norm_of_nonneg (zero_le_one.trans_lt hq').le]
-- 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
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ 1 = ‖ζ'‖
have h : Eq (α := ℝ) 1 1
Tactic: rw [hζ'.norm'_eq_one hn.ne']
-- 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
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
have hfor : ∀ ζ' ∈ 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']
-- 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 : ℂ))
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
have hζ : IsPrimitiveRoot ζ n
Tactic: have hζ : IsPrimitiveRoot ζ n := Complex.isPrimitiveRoot_exp n hn.ne'
-- 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
⊢ ∃ ζ' ∈ primitiveRoots n ℂ, ‖(↑q : ℂ) - ζ'‖ < q + 1
have refine : ‖(↑q : ℂ) - ζ‖ < q + 1
Tactic: refine ⟨ζ, (mem_primitiveRoots hn).mpr hζ, ?_⟩
-- 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
this : ¬SameRay ℝ (↑q : ℂ) (-ζ)
⊢ ‖(↑q : ℂ) - ζ‖ < q + 1
have h : q = ‖(↑q : ℂ)‖
Tactic: convert! norm_add_lt_of_not_sameRay 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
this : ¬SameRay ℝ (↑q : ℂ) (-ζ)
h : q = ‖(↑q : ℂ)‖
⊢ ‖(↑q : ℂ) - ζ‖ < q + 1
have h₁ : 1 = ‖-ζ‖
Tactic: convert! norm_add_lt_of_not_sameRay 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
this : ¬SameRay ℝ (↑q : ℂ) (-ζ)
⊢ q = ‖(↑q : ℂ)‖
have h : q = ‖q‖
Tactic: rw [Complex.norm_real]
-- 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
this : ¬SameRay ℝ (↑q : ℂ) (-ζ)
⊢ q = ‖q‖
have h : ‖q‖ = q
Tactic: 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
⊢ ‖(↑q : ℂ) - ζ‖ < q + 1
have suffices : ¬SameRay ℝ (↑q : ℂ) (-ζ)
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']
-- 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
⊢ ¬SameRay ℝ (↑q : ℂ) (-ζ)
have rw : ¬((↑q : ℂ) = 0 ∨ -ζ = 0 ∨ (↑q : ℂ).arg = (-ζ).arg)
Tactic: rw [Complex.sameRay_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
⊢ ¬((↑q : ℂ) = 0 ∨ -ζ = 0 ∨ (↑q : ℂ).arg = (-ζ).arg)
have push : (↑q : ℂ) ≠ 0 ∧ -ζ ≠ 0 ∧ (↑q : ℂ).arg ≠ (-ζ).arg
Tactic: push Not
-- 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
⊢ (↑q : ℂ) ≠ 0 ∧ -ζ ≠ 0 ∧ (↑q : ℂ).arg ≠ (-ζ).arg
have refine : (↑q : ℂ).arg ≠ (-ζ).arg
Tactic: refine ⟨mod_cast hq.ne', neg_ne_zero.mpr <| hζ.ne_zero hn.ne', ?_⟩
-- 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
⊢ (↑q : ℂ).arg ≠ (-ζ).arg
have rw : ¬(-ζ).arg = 0
Tactic: rw [Complex.arg_ofReal_of_nonneg hq.le, Ne, eq_comm]
-- 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
h : (-ζ).arg = 0
⊢ False
have h₁ : ζ.re ≤ 0 ∧ ζ.im = 0
Tactic: rw [Complex.arg_eq_zero_iff, Complex.neg_re, neg_nonneg, Complex.neg_im, neg_eq_zero] at h
Cleared hypotheses: h
-- 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
h : ζ.re ≤ 0 ∧ ζ.im = 0
⊢ ζ ≠ 0
have clear_value : ∀ (ζ : ℂ) (hζ : IsPrimitiveRoot ζ n) (h : ζ.re ≤ 0 ∧ ζ.im = 0), ζ ≠ 0
Tactic: clear_value ζ
Cleared hypotheses: ζ, hζ, h
-- 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
h : ζ.re ≤ 0 ∧ ζ.im = 0
⊢ False
have hζ₀ : ζ ≠ 0
Tactic: have hζ₀ : ζ ≠ 0 := by
      clear_value ζ
      rintro rfl
      exact hn.ne' (hζ.unique IsPrimitiveRoot.zero)
-- 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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
⊢ False
have refine_2 : ∀ (this : ζ.re < 0 ∧ ζ.im = 0), False
Tactic: have : ζ.re < 0 ∧ ζ.im = 0 := ⟨h.1.lt_of_ne ?_, h.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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
refine_2 : ∀ (this : ζ.re < 0 ∧ ζ.im = 0), False
⊢ False
have refine_1 : ζ.re ≠ 0
Tactic: have : ζ.re < 0 ∧ ζ.im = 0 := ⟨h.1.lt_of_ne ?_, 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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
this : ζ.re < 0 ∧ ζ.im = 0
⊢ False
have this₁ : ζ = -1
Tactic: rw [← Complex.arg_eq_pi_iff, hζ.arg_eq_pi_iff hn.ne'] at this
Cleared hypotheses: this
-- 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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
this : ζ = -1
⊢ False
have hζ₁ : IsPrimitiveRoot (M := ℂ) (-1) n
Tactic: rw [this] at hζ
Cleared hypotheses: hζ, h, hζ₀, 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 (M := ℂ) (-1) n
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
this : ζ = -1
⊢ False
have linarith : -1 + HSub.hSub (α := ℤ) 3 (↑n : ℤ) + HSub.hSub (α := ℤ) (↑n : ℤ) 2 = 0
Tactic: linarith [hζ.unique <| IsPrimitiveRoot.neg_one 0 two_ne_zero.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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ ≠ 0
⊢ ζ.re ≠ 0
have refine_1 : ∀ (hζ₀ : ζ.re = 0), ζ = 0
Tactic: contrapose hζ₀
Cleared hypotheses: hζ₀
-- 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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ.re = 0
⊢ ζ = 0
have refine_1 : ζ.re = Complex.re 0
Tactic: apply Complex.ext
-- 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
h : ζ.re ≤ 0 ∧ ζ.im = 0
hζ₀ : ζ.re = 0
refine_1 : ζ.re = Complex.re 0
⊢ ζ = 0
have refine_1₁ : ζ.im = Complex.im 0
Tactic: apply Complex.ext