-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem exists_neg_pow_of_isOfFinOrder [IsCyclotomicExtension {n} ℚ K]
    (hno : Odd (n : ℕ)) {ζ x : K} (hζ : IsPrimitiveRoot ζ n) (hx : IsOfFinOrder x) :
    ∃ r : ℕ, x = (-ζ) ^ r :=  by
  have hnegζ : IsPrimitiveRoot (-ζ) (2 * n)

Proof state:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero ↑l
a : ℕ
ha : 2 * ↑n = l * a
⊢ x ^ (2 * ↑n) = 1

Tactic:
rw [ha, pow_mul, hlroot.pow_eq_one, one_pow]

Result:
no goals

Proof state:
case h.e'_4
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
⊢ (orderOf (-1)).Coprime (orderOf ζ)

Tactic:
simp [← hζ.eq_orderOf, hno]

Result:
no goals

Proof state:
case h.e'_4
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
⊢ 2 * ↑n = orderOf (-1) * orderOf ζ

Tactic:
simp [hζ.eq_orderOf]

Result:
no goals

Proof state:
case intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : (cyclotomic l K).IsRoot x
hlzero : NeZero l
this : NeZero ↑l
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
rw [isRoot_cyclotomic_iff] at hlroot

Result:
case intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero ↑l
⊢ ∃ r, x = (-ζ) ^ r

Proof state:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : (cyclotomic l K).IsRoot x
h : l = 0
⊢ False

Tactic:
simp [h] at hl

Result:
no goals

Proof state:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
obtain ⟨k, hkpos, hkn⟩ := isOfFinOrder_iff_pow_eq_one.1 hx

Result:
case intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
⊢ ∃ r, x = (-ζ) ^ r

Proof state:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
⊢ IsPrimitiveRoot (-ζ) (2 * ↑n)

Tactic:
convert IsPrimitiveRoot.orderOf (-ζ)

Result:
case h.e'_4
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
⊢ 2 * ↑n = orderOf (-ζ)

Proof state:
case intro.intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero ↑l
a : ℕ
ha : 2 * ↑n = l * a
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
replace hlroot : x ^ (2 * (n : ℕ)) = 1 := by rw [ha, pow_mul, hlroot.pow_eq_one, one_pow]

Result:
case intro.intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlzero : NeZero l
this : NeZero ↑l
a : ℕ
ha : 2 * ↑n = l * a
hlroot : x ^ (2 * ↑n) = 1
⊢ ∃ r, x = (-ζ) ^ r

Proof state:
case intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
obtain ⟨l, hl, hlroot⟩ := (isRoot_of_unity_iff hkpos _).1 hkn

Result:
case intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : (cyclotomic l K).IsRoot x
⊢ ∃ r, x = (-ζ) ^ r

Proof state:
case intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : (cyclotomic l K).IsRoot x
hlzero : NeZero l
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
have : NeZero (l : K) := ⟨NeZero.natCast_ne l K⟩

Result:
case intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : (cyclotomic l K).IsRoot x
hlzero : NeZero l
this : NeZero ↑l
⊢ ∃ r, x = (-ζ) ^ r

Proof state:
case intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero ↑l
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
obtain ⟨a, ha⟩ := hlroot.dvd_of_isCyclotomicExtension n hlzero.1

Result:
case intro.intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero ↑l
a : ℕ
ha : 2 * ↑n = l * a
⊢ ∃ r, x = (-ζ) ^ r

Proof state:
case intro.intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlzero : NeZero l
this : NeZero ↑l
a : ℕ
ha : 2 * ↑n = l * a
hlroot : x ^ (2 * ↑n) = 1
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
obtain ⟨s, -, hs⟩ := hnegζ.eq_pow_of_pow_eq_one hlroot

Result:
case intro.intro.intro.intro.intro.intro.intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlzero : NeZero l
this : NeZero ↑l
a : ℕ
ha : 2 * ↑n = l * a
hlroot : x ^ (2 * ↑n) = 1
s : ℕ
hs : (-ζ) ^ s = x
⊢ ∃ r, x = (-ζ) ^ r