awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
h : 1 < x
⊢ 0 < x + 1
have linarith : x + 1 ≤ 0 → HMul.hMul (α := R) 2 (-1) + (1 - x) + (x + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
h : 1 < x
linarith : x + 1 ≤ 0 → HMul.hMul (α := R) 2 (-1) + (1 - x) + (x + 1 - 0) = 0
⊢ 0 < x + 1
have linarith₁ : x + 1 ≤ 0 → GT.gt.{u_1} (α := R) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
h : 1 ≤ x
⊢ 0 ≤ x + 1
have linarith : x + 1 < 0 → HMul.hMul (α := R) 2 (-1) + (1 - x) + (x + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
h : 1 ≤ x
linarith : x + 1 < 0 → HMul.hMul (α := R) 2 (-1) + (1 - x) + (x + 1 - 0) = 0
⊢ 0 ≤ x + 1
have linarith₁ : x + 1 < 0 → GT.gt.{u_1} (α := R) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
⊢ (1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R))
have succ : 1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
succ : 1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)
⊢ (1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R))
have succ₁ : 1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
h : 1 ≤ x
⊢ 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R)
have succ : 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)
Tactic: apply le_of_lt
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
⊢ (1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R))
have succ : 1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)
Tactic: constructor <;> intro <;> [skip; apply le_of_lt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
n : ℕ
succ : 1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)
⊢ (1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R))
have succ₁ : 1 ≤ x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)
Tactic: constructor <;> intro <;> [skip; apply le_of_lt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
⊢ eval 1 (cyclotomic n R) = 1
have inl : ∀ (h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ 0), eval 1 (cyclotomic 0 R) = 1
Tactic: rcases n.eq_zero_or_pos with (rfl | hn')
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
inl : ∀ (h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ 0), eval 1 (cyclotomic 0 R) = 1
⊢ eval 1 (cyclotomic n R) = 1
have inr : ∀ (hn' : n > 0), eval 1 (cyclotomic n R) = 1
Tactic: rcases n.eq_zero_or_pos with (rfl | hn')
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
⊢ eval 1 (cyclotomic n R) = 1
have hn : 1 < n
Tactic: have hn : 1 < n := one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn'.ne', (h Nat.prime_two 0).symm⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
⊢ eval 1 (cyclotomic n R) = 1
have inr : ∀ (h : eval 1 (cyclotomic n ℤ) = 1), eval 1 (cyclotomic n R) = 1
Tactic: rsuffices h | h : eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
inr : ∀ (h : eval 1 (cyclotomic n ℤ) = 1), eval 1 (cyclotomic n R) = 1
⊢ eval 1 (cyclotomic n R) = 1
have inr₁ : ∀ (h : eval 1 (cyclotomic n ℤ) = -1), eval 1 (cyclotomic n R) = 1
Tactic: rsuffices h | h : eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
inr : ∀ (h : eval 1 (cyclotomic n ℤ) = 1), eval 1 (cyclotomic n R) = 1
inr₁ : ∀ (h : eval 1 (cyclotomic n ℤ) = -1), eval 1 (cyclotomic n R) = 1
⊢ eval 1 (cyclotomic n R) = 1
have rsuffices : eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1
Tactic: rsuffices h | h : eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h_1 : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = 1
⊢ eval 1 (cyclotomic n R) = 1
have this : Eq (α := R) (eval (↑1 : R) (map (Int.castRingHom R) (cyclotomic n ℤ)) : R)
  (((Int.castRingHom R : ℤ →+* R) : (a : ℤ) → R) (eval (↑1 : ℤ) (cyclotomic n ℤ)) : R)
Tactic: have := eval_intCast_map (Int.castRingHom R) (cyclotomic n ℤ) 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h_1 : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = -1
⊢ eval 1 (cyclotomic n R) = 1
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h_1 : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = -1
⊢ False
have linarith : -1 + (eval 1 (cyclotomic n ℤ) - -1) + (0 - eval 1 (cyclotomic n ℤ)) = 0
Tactic: linarith [cyclotomic_nonneg n (le_refl (1 : ℤ))]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
⊢ eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1
have rw : ∀ (p : ℕ), Nat.Prime p → ¬p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
Tactic: rw [← Int.natAbs_eq_natAbs_iff, Int.natAbs_one, Nat.eq_one_iff_not_exists_prime_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
⊢ False
have this : Fact (Nat.Prime p)
Tactic: haveI := Fact.mk hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this : Fact (Nat.Prime p)
⊢ False
have this₁ : Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
Tactic: have := prod_cyclotomic_eq_geom_sum hn' ℤ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this : Eq (α := ℤ[X]) (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i)
⊢ False
have this₁ : Eq (α := ℤ) (eval 1 (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ)) (eval 1 (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i))
Tactic: apply_fun eval 1 at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  Eq (α := ℤ) (eval 1 (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ)) (eval 1 (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i))
⊢ False
have rw : ∀
  (this :
    (↑n : ℤ) =
      HMul.hMul (α := ℤ)
        (∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)),
          eval 1 (cyclotomic x ℤ))
        (∏ x ∈ range (padicValNat p n), eval 1 (cyclotomic (p ^ (x + 1)) ℤ))),
  False
Tactic: rw [eval_geom_sum, one_geom_sum, eval_prod, eq_comm, ←
    Finset.prod_sdiff <| @range_pow_padicValNat_subset_divisors' p _ _, Finset.prod_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  Eq (α := ℤ) (eval 1 (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ)) (eval 1 (∑ i ∈ range n, HPow.hPow (α := ℤ[X]) X i))
rw :
  ∀
    (this :
      (↑n : ℤ) =
        HMul.hMul (α := ℤ)
          (∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)),
            eval 1 (cyclotomic x ℤ))
          (∏ x ∈ range (padicValNat p n), eval 1 (cyclotomic (p ^ (x + 1)) ℤ))),
    False
⊢ False
have rw₁ : ∀
  (this :
    (↑n : ℤ) =
      HMul.hMul (α := ℤ)
        (∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)),
          eval 1 (cyclotomic x ℤ))
        (∏ x ∈ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ))),
  Set.InjOn (β := ℕ) (fun (t : ℕ) ↦ p ^ (t + 1)) (↑(range (padicValNat p n)) : Set ℕ)
Tactic: rw [eval_geom_sum, one_geom_sum, eval_prod, eq_comm, ←
    Finset.prod_sdiff <| @range_pow_padicValNat_subset_divisors' p _ _, Finset.prod_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HMul.hMul (α := ℤ)
      (∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ))
      (∏ x ∈ range (padicValNat p n), eval 1 (cyclotomic (p ^ (x + 1)) ℤ))
⊢ False
have this₁ : (↑n : ℤ) =
  HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
    ∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
Tactic: simp_rw [eval_one_cyclotomic_prime_pow, Finset.prod_const, Finset.card_range, mul_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      ∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ False
have rw : ∀
  (this :
    (↑n : ℤ) =
      HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
        HMul.hMul (α := ℤ)
          (∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
            eval 1 (cyclotomic x ℤ))
          (∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))),
  False
Tactic: rw [← Finset.prod_sdiff <| show {n} ⊆ _ from _] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      ∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
rw :
  ∀
    (this :
      (↑n : ℤ) =
        HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
          HMul.hMul (α := ℤ)
            (∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
              eval 1 (cyclotomic x ℤ))
            (∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))),
    False
⊢ False
have rw₁ : {n} ⊆ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))
Tactic: rw [← Finset.prod_sdiff <| show {n} ⊆ _ from _] at this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      ∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ {n} ⊆ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))
have simp : (¬n = 1 ∧ ¬n = 0) ∧ ∀ x < padicValNat p n, ¬p ^ (x + 1) = n
Tactic: simp only [singleton_subset_iff, mem_sdiff, mem_erase, Ne, mem_divisors, dvd_refl,
        true_and, mem_image, mem_range, not_exists, not_and]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      HMul.hMul (α := ℤ)
        (∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
        (∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))
⊢ False
have hpe₁ : (↑p : ℤ) ∣ eval 1 (cyclotomic n ℤ)
Tactic: rw [← Int.natAbs_natCast p, Int.natAbs_dvd_natAbs] at hpe
Cleared hypotheses: hpe, this_1, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : (↑p : ℤ) ∣ eval 1 (cyclotomic n ℤ)
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      HMul.hMul (α := ℤ)
        (∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
        (∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))
⊢ False
have obtain : ∀ (t : ℤ) (ht : eval 1 (cyclotomic n ℤ) = (↑p : ℤ) * t), False
Tactic: obtain ⟨t, ht⟩ := hpe
Cleared hypotheses: hpe
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) *
      HMul.hMul (α := ℤ)
        (∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
        (∏ x ∈ {n}, eval 1 (cyclotomic x ℤ))
t : ℤ
ht : eval 1 (cyclotomic n ℤ) = (↑p : ℤ) * t
⊢ False
have rw : ∀ (t : ℤ)
  (this :
    (↑n : ℤ) =
      HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) * (↑p : ℤ) *
        (t *
          ∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
            eval 1 (cyclotomic x ℤ)))
  (ht : eval 1 (cyclotomic n ℤ) = (↑p : ℤ) * t), False
Tactic: rw [Finset.prod_singleton, ht, mul_left_comm, mul_comm, ← mul_assoc, mul_assoc] at this
Cleared hypotheses: this, t, ht
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this_1 : Fact (Nat.Prime p)
t : ℤ
this :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) * (↑p : ℤ) *
      (t *
        ∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
ht : eval 1 (cyclotomic n ℤ) = (↑p : ℤ) * t
⊢ False
have this₁ : HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) * (↑p : ℤ) ∣ (↑n : ℤ)
Tactic: have : (p : ℤ) ^ padicValNat p n * p ∣ n := ⟨_, this⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
this_1 : Fact (Nat.Prime p)
t : ℤ
this_2 :
  (↑n : ℤ) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) * (↑p : ℤ) *
      (t *
        ∏ x ∈ (n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n))) \ {n},
          eval 1 (cyclotomic x ℤ))
ht : eval 1 (cyclotomic n ℤ) = (↑p : ℤ) * t
this : HPow.hPow (α := ℤ) (↑p : ℤ) (padicValNat p n) * (↑p : ℤ) ∣ (↑n : ℤ)
⊢ False
have this₁ : p ^ (padicValNat p n + 1) ∣ n
Tactic: simp only [← _root_.pow_succ, ← Int.natAbs_dvd_natAbs, Int.natAbs_natCast,
      Int.natAbs_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this_1 : Fact (Nat.Prime p)
this :
  (↑n : ℤ) =
    HMul.hMul (α := ℤ)
      (∏ x ∈ n.divisors.erase 1 \ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ))
      (∏ x ∈ image (fun (t : ℕ) ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ))
x y : ℕ
hxy : Eq (α := ℕ) ((fun (t : ℕ) ↦ p ^ (t + 1)) x) ((fun (t : ℕ) ↦ p ^ (t + 1)) y)
⊢ x = y
have a : x.succ = y.succ
Tactic: apply Nat.succ_injective
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (hypothesis)
Goal:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
⊢ (q - 1) ^ φ n < eval q (cyclotomic 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' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
⊢ (q - 1) ^ φ n < eval q (cyclotomic 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' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : ζ' ∈ primitiveRoots n ℂ
⊢ q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
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' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
have h : q = ‖(↑q : ℂ)‖
Tactic: convert! norm_sub_norm_le (↑q) ζ'
-- 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
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
h : q = ‖(↑q : ℂ)‖
⊢ q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
have h₁ : 1 = ‖ζ'‖
Tactic: convert! norm_sub_norm_le (↑q) ζ'
-- 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
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q = ‖(↑q : ℂ)‖
have h : q = ‖q‖
Tactic: rw [Complex.norm_real, Real.norm_of_nonneg 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
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
h : q = ‖q‖
⊢ q = ‖(↑q : ℂ)‖
have h₁ : q = q
Tactic: rw [Complex.norm_real, Real.norm_of_nonneg 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
ζ' : ℂ
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' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
have hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
Tactic: have hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖ := by
    intro ζ' hζ'
    rw [mem_primitiveRoots hn] at hζ'
    convert! norm_sub_norm_le (↑q) ζ'
    · rw [Complex.norm_real, Real.norm_of_nonneg hq.le]
    · rw [hζ'.norm'_eq_one hn.ne']
-- 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 : ℂ))
⊢ (q - 1) ^ φ n < eval q (cyclotomic 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' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖(↑q : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
⊢ ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖(↑q : ℂ) - ζ'‖
have refine : q - 1 < ‖(↑q : ℂ) - ζ‖
Tactic: refine ⟨ζ, (mem_primitiveRoots hn).mpr 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 : ℂ) - ζ'‖
ζ : ℂ := Complex.exp (2 * (↑Real.pi : ℂ) * Complex.I / (↑n : ℂ))
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q : ℂ) ζ
⊢ q - 1 < ‖(↑q : ℂ) - ζ‖
have h : q = ‖(↑q : ℂ)‖
Tactic: convert! lt_norm_sub_of_not_sameRay 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
this : ¬SameRay ℝ (↑q : ℂ) ζ
h : q = ‖(↑q : ℂ)‖
⊢ q - 1 < ‖(↑q : ℂ) - ζ‖
have h₁ : 1 = ‖ζ‖
Tactic: convert! lt_norm_sub_of_not_sameRay 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
⊢ q - 1 < ‖(↑q : ℂ) - ζ‖
have suffices : ¬SameRay ℝ (↑q : ℂ) ζ
Tactic: suffices ¬SameRay ℝ (q : ℂ) ζ by
      convert! lt_norm_sub_of_not_sameRay this <;>
        simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]
-- 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
⊢ ¬SameRay ℝ (↑q : ℂ) ζ
have rw : ¬((↑q : ℂ) = 0 ∨ ζ = 0 ∨ (↑q : ℂ).arg = ζ.arg)
Tactic: rw [Complex.sameRay_iff]