-- Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
theorem eval_one_cyclotomic_not_prime_pow {R : Type*} [Ring R] {n : ℕ}
    (h : ∀ {p : ℕ}, p.Prime → ∀ k : ℕ, p ^ k ≠ n) : eval 1 (cyclotomic n R) = 1

Proof state:
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)
this :
  ↑n =
    (∏ 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 ∈ range (padicValNat p n), ∀ y ∈ range (padicValNat p n), p ^ (x + 1) = p ^ (y + 1) → x = y

Tactic:
rintro x - y - hxy

Result:
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)
this :
  ↑n =
    (∏ 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 : p ^ (x + 1) = p ^ (y + 1)
⊢ x = y

Proof state:
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)
this : ∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ = ∑ i ∈ range n, X ^ i
⊢ False

Tactic:
apply_fun eval 1 at this

Result:
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)
this : eval 1 (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) = eval 1 (∑ i ∈ range n, X ^ i)
⊢ False

Proof state:
case inr
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

Tactic:
rsuffices h | h : eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1

Result:
case inr.inl
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {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

case inr.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {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

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

Proof state:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
⊢ eval 1 (cyclotomic n R) = 1

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn')

Result:
case inl
R : Type u_1
inst✝ : Ring R
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ 0
⊢ eval 1 (cyclotomic 0 R) = 1

case inr
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

Proof state:
case intro
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✝¹ : Fact (Nat.Prime p)
t : ℤ
this✝ :
  ↑n =
    ↑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 : p ^ (padicValNat p n + 1) ∣ n
⊢ False

Tactic:
exact pow_succ_padicValNat_not_dvd hn'.ne' this

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : Ring R
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ 0
⊢ eval 1 (cyclotomic 0 R) = 1

Tactic:
simp

Result:
no goals

Proof state:
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)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ((∏ 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

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)
this :
  ↑n =
    ↑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))

Tactic:
swap

Result:
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)
this :
  ↑n =
    ↑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))

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)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ((∏ 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

Proof state:
case inr.inl
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = 1
this : eval (↑1) (map (Int.castRingHom R) (cyclotomic n ℤ)) = (Int.castRingHom R) (eval (↑1) (cyclotomic n ℤ))
⊢ eval 1 (cyclotomic n R) = 1

Tactic:
simpa only [map_cyclotomic, Int.cast_one, h, eq_intCast] using this

Result:
no goals

Proof state:
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)
this :
  ↑n =
    (∏ 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 : p ^ (x + 1) = p ^ (y + 1)
⊢ x = y

Tactic:
apply Nat.succ_injective

Result:
case a
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)
this :
  ↑n =
    (∏ 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 : p ^ (x + 1) = p ^ (y + 1)
⊢ x.succ = y.succ

Proof state:
case inr.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {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

Tactic:
exfalso

Result:
case inr.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
h✝ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
h : eval 1 (cyclotomic n ℤ) = -1
⊢ False

Proof state:
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

Tactic:
rw [← Int.natAbs_eq_natAbs_iff, Int.natAbs_one, Nat.eq_one_iff_not_exists_prime_dvd]

Result:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
⊢ ∀ (p : ℕ), Nat.Prime p → ¬p ∣ (eval 1 (cyclotomic n ℤ)).natAbs