-- Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
theorem cyclotomic_eval_lt_add_one_pow_totient {n : ℕ} {q : ℝ} (hn' : 3 ≤ n) (hq' : 1 < q) :
    (cyclotomic n ℝ).eval q < (q + 1) ^ totient n

Proof state:
case h.e'_4
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]

Result:
no goals

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

Tactic:
rw [Complex.arg_ofReal_of_nonneg hq.le, Ne, eq_comm]

Result:
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
⊢ ¬(-ζ).arg = 0

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

Tactic:
have hζ₀ : ζ ≠ 0 := by
  clear_value ζ
  rintro rfl
  exact hn.ne' (hζ.unique IsPrimitiveRoot.zero)

Result:
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

Proof state:
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✝ : { x // x ∈ primitiveRoots n ℂ }
⊢ (q + 1).toNNReal ≠ 0

Tactic:
simp

Result:
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✝ : { x // x ∈ primitiveRoots n ℂ }
⊢ 0 < q + 1

Proof state:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n

Tactic:
have hn : 0 < n := pos_of_gt hn'

Result:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n

Proof state:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
hζ : IsPrimitiveRoot 0 n
h : Complex.re 0 ≤ 0 ∧ Complex.im 0 = 0
⊢ False

Tactic:
exact hn.ne' (hζ.unique IsPrimitiveRoot.zero)

Result:
no goals

Proof state:
case h.e'_4.h.e'_5
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
this : ‖eval (↑q) (cyclotomic n ℂ)‖ < ((q + 1) ⊔ 0) ^ φ n
⊢ q + 1 = (q + 1) ⊔ 0

Tactic:
rw [eq_comm, max_eq_left_iff]

Result:
case h.e'_4.h.e'_5
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
this : ‖eval (↑q) (cyclotomic n ℂ)‖ < ((q + 1) ⊔ 0) ^ φ n
⊢ 0 ≤ q + 1

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

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

Result:
case h.e'_4
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, ?convert_3 i

case convert_3
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 // x ∈ primitiveRoots n ℂ } → NNRealˣ

case convert_5
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‖₊ ⋯ ≤ ?convert_3 i

case convert_6
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‖₊ ⋯ < ?convert_3 i

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

Tactic:
apply Complex.ext <;> simp [hζ₀, h.2]

Result:
no goals

Proof state:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ ‖↑q - ζ'‖ ≤ q + 1

Tactic:
convert norm_sub_le (↑q) ζ'

Result:
case h.e'_4.h.e'_5
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ q = ‖↑q‖

case h.e'_4.h.e'_6
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ 1 = ‖ζ'‖

Proof state:
case h.e'_3
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
this : ‖eval (↑q) (cyclotomic n ℂ)‖ < ((q + 1) ⊔ 0) ^ φ n
⊢ ‖eval (↑q) (cyclotomic n ℂ)‖ = eval q (cyclotomic n ℝ)

Tactic:
simp [cyclotomic_nonneg n hq'.le]

Result:
no goals

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

Tactic:
obtain ⟨ζ, hζ, hhζ : ‖_‖ < _⟩ := hex

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