awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (M := K[X]) (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p hppos) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) q hqpos)
⊢ IsPrimitiveRoot z (↑k : ℕ)

Tactic:
have : IsPrimitiveRoot z k := hx.pow_mul_pow_lcm hy hppos.ne' hqpos.ne'
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (M := K[X]) (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p hppos) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) q hqpos)
this : IsPrimitiveRoot z (↑k : ℕ)
⊢ IsCyclotomicExtension.{u, v} {(↑k : ℕ)} K ↥K[z]

Tactic:
haveI := IsPrimitiveRoot.adjoin_isCyclotomicExtension K this
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (M := K[X]) (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p hppos) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) q hqpos)
this_1 : IsPrimitiveRoot z (↑k : ℕ)
this : IsCyclotomicExtension.{u, v} {(↑k : ℕ)} K ↥K[z]
⊢ Module.finrank.{u, v} K ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) K[z] : Submodule K L) ≤
    Module.finrank K L

Tactic:
Submodule.finrank_le (Subalgebra.toSubmodule (adjoin K { z }))

Premises used: Algebra.adjoin, Subalgebra.toSubmodule, Submodule.finrank_le, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (M := K[X]) (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p hppos) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) q hqpos)
this_1 : IsPrimitiveRoot z (↑k : ℕ)
this : IsCyclotomicExtension.{u, v} {(↑k : ℕ)} K ↥K[z]
h :
  φ (p.lcm q) =
    Module.finrank.{u, v} K ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) K[z] : Submodule K L)
⊢ φ (p.lcm q) ≤ Module.finrank K L

Tactic:
convert! Submodule.finrank_le (Subalgebra.toSubmodule (adjoin K { z }))

Premises used: Algebra.adjoin, Subalgebra.toSubmodule, Submodule.finrank_le, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (M := K[X]) (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p hppos) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) q hqpos)
this_1 : IsPrimitiveRoot z (↑k : ℕ)
this : IsCyclotomicExtension.{u, v} {(↑k : ℕ)} K ↥K[z]
⊢ Irreducible (M := K[X]) (cyclotomic (↑k : ℕ) K)

Tactic:
rw [show Nat.lcm p q = (k : ℕ) from rfl] at hirr

Premises used: rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (M := K[X]) (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p hppos) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) q hqpos)
this_1 : IsPrimitiveRoot z (↑k : ℕ)
this : IsCyclotomicExtension.{u, v} {(↑k : ℕ)} K ↥K[z]
hirr₁ : Irreducible (M := K[X]) (cyclotomic (↑k : ℕ) K)
⊢ IsPrimitiveRoot z (↑k : ℕ)

Tactic:
rw [show Nat.lcm p q = (k : ℕ) from rfl] at hirr

Premises used: rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hirr : Irreducible (M := K[X]) (cyclotomic (p.lcm q) K)
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p hppos) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) q hqpos)
this_1 : IsPrimitiveRoot z (↑k : ℕ)
this : IsCyclotomicExtension.{u, v} {(↑k : ℕ)} K ↥K[z]
hirr₁ : Irreducible (M := K[X]) (cyclotomic (↑k : ℕ) K)
this₁ : IsPrimitiveRoot z (↑k : ℕ)
⊢ IsCyclotomicExtension.{u, v} {(↑k : ℕ)} K ↥K[z]

Tactic:
rw [show Nat.lcm p q = (k : ℕ) from rfl] at hirr

Premises used: rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : CommRing L
inst_2 : IsDomain L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
p q : ℕ
x y : L
hx : IsPrimitiveRoot x p
hy : IsPrimitiveRoot y q
hppos : p > 0
hqpos : q > 0
z : L := x ^ (p / p.factorizationLCMLeft q) * y ^ (q / p.factorizationLCMRight q)
k : ℕ+ := PNat.lcm (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) p hppos) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) q hqpos)
hirr : Irreducible (M := K[X]) (cyclotomic (↑k : ℕ) K)
this_1 : IsPrimitiveRoot z (↑k : ℕ)
this : IsCyclotomicExtension.{u, v} {(↑k : ℕ)} K ↥K[z]
⊢ φ (p.lcm q) =
    Module.finrank.{u, v} K ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) K[z] : Submodule K L)

Tactic:
simpa using (IsCyclotomicExtension.finrank (Algebra.adjoin K {z}) hirr).symm

Premises used: Algebra.adjoin, Membership.mem, IsCyclotomicExtension.finrank, Subtype, Singleton.singleton, Eq.symm
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl : l ≠ 0
⊢ NeZero l

Tactic:
have hl : NeZero l := ⟨hl⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
⊢ IsPrimitiveRoot (zeta n ℚ K) n

Tactic:
have hroot := IsCyclotomicExtension.zeta_spec n ℚ K
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
⊢ φ (l.lcm n) ≤ Module.finrank ℚ K

Tactic:
have key := IsPrimitiveRoot.lcm_totient_le_finrank hζ hroot
    (cyclotomic.irreducible_rat <| Nat.lcm_pos (Nat.pos_of_ne_zero hl.1) (NeZero.pos n))
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
key : φ (l.lcm n) ≤ Module.finrank ℚ K
⊢ φ (l.lcm n) ≤ φ n

Tactic:
rw [IsCyclotomicExtension.finrank K (cyclotomic.irreducible_rat (NeZero.pos n))] at key

Premises used: IsCyclotomicExtension.finrank, Polynomial.cyclotomic.irreducible_rat, NeZero.pos
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
key : φ (l.lcm n) ≤ φ n
rcases : ∀ (r : ℕ) (hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r), l ∣ 2 * n
⊢ l ∣ 2 * n

Tactic:
rcases _root_.dvd_lcm_right l n with ⟨r, hr⟩

Premises used: dvd_lcm_right
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
key : φ (l.lcm n) ≤ φ n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
⊢ φ n * φ r ≤ φ (n * r)

Tactic:
have ineq := Nat.totient_super_multiplicative n r
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
key : φ (l.lcm n) ≤ φ n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (n * r)
⊢ φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)

Tactic:
rw [← hr] at ineq
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
key : φ (l.lcm n) ≤ φ n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
⊢ φ r ≤ 1

Tactic:
replace key := (mul_le_iff_le_one_right (Nat.totient_pos.2 (NeZero.pos n))).mp (le_trans ineq key)
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
key : φ r ≤ 1
⊢ 0 < r

Tactic:
Nat.pos_of_ne_zero (fun h ↦ ?_)

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
key : φ r ≤ 1
refine : ∀ (h : r = 0), False
⊢ 0 < r

Tactic:
refine Nat.pos_of_ne_zero (fun h ↦ ?_)

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
key : φ r ≤ 1
h : r = 0
⊢ False

Tactic:
simp only [h, mul_zero, _root_.lcm_eq_zero_iff, NeZero.ne _, or_false] at hr

Premises used: lcm_eq_zero_iff, MulZeroClass.mul_zero, or_false, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
key : φ r ≤ 1
⊢ 0 < r

Tactic:
have rpos : 0 < r := by
    refine Nat.pos_of_ne_zero (fun h ↦ ?_)
    simp only [h, mul_zero, _root_.lcm_eq_zero_iff, NeZero.ne _, or_false] at hr
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
key : φ r ≤ 1
rpos : 0 < r
⊢ r = 1 ∨ r = 2

Tactic:
replace key := (Nat.dvd_prime Nat.prime_two).1 (Nat.dvd_two_of_totient_le_one rpos key)
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 1 ∨ r = 2
inl : ∀ (key : r = 1), l ∣ 2 * n
inr : ∀ (key : r = 2), l ∣ 2 * n
⊢ l ∣ 2 * n

Tactic:
rcases key with (key | key)
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 1
⊢ @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n

Tactic:
rw [key, mul_one] at hr

Premises used: mul_one
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 1
hr₁ : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n
⊢ φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)

Tactic:
rw [key, mul_one] at hr

Premises used: mul_one
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 1
hr₁ : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n
ineq₁ : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
⊢ 0 < r

Tactic:
rw [key, mul_one] at hr

Premises used: mul_one
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 1
hr₁ : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n
ineq₁ : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos₁ : 0 < r
⊢ r = 1

Tactic:
rw [key, mul_one] at hr

Premises used: mul_one
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 1
inl : l ∣ 2 * @GCDMonoid.lcm _ instCommMonoidWithZero _ l n
⊢ l ∣ 2 * n

Tactic:
rw [← hr]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 1
⊢ l ∣ 2 * @GCDMonoid.lcm _ instCommMonoidWithZero _ l n

Tactic:
dvd_mul_of_dvd_right (_root_.dvd_lcm_left l n) 2

Premises used: dvd_mul_of_dvd_right, dvd_lcm_left, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 1
⊢ l ∣ 2 * @GCDMonoid.lcm _ instCommMonoidWithZero _ l n

Tactic:
exact dvd_mul_of_dvd_right (_root_.dvd_lcm_left l n) 2

Premises used: dvd_mul_of_dvd_right, dvd_lcm_left, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 2
⊢ @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = 2 * n

Tactic:
rw [key, mul_comm] at hr

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 2
hr₁ : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = 2 * n
⊢ φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)

Tactic:
rw [key, mul_comm] at hr

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 2
hr₁ : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = 2 * n
ineq₁ : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
⊢ 0 < r

Tactic:
rw [key, mul_comm] at hr

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 2
hr₁ : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = 2 * n
ineq₁ : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos₁ : 0 < r
⊢ r = 2

Tactic:
rw [key, mul_comm] at hr

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl_1 : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = 2 * n
ineq : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
rpos : 0 < r
key : r = 2
⊢ l ∣ 2 * n

Tactic:
simpa [← hr] using _root_.dvd_lcm_left _ _

Premises used: dvd_lcm_left
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ IsPrimitiveRoot (-ζ) (orderOf (-ζ))

Tactic:
IsPrimitiveRoot.orderOf (-ζ)

Premises used: IsPrimitiveRoot.orderOf, Neg.neg
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
h : 2 * n = orderOf (-ζ)
⊢ IsPrimitiveRoot (-ζ) (2 * n)

Tactic:
convert! IsPrimitiveRoot.orderOf (-ζ)

Premises used: IsPrimitiveRoot.orderOf, Neg.neg
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
h : 2 * n = orderOf.{u} (G := K) (-1) * orderOf ζ
h₁ : (orderOf.{u} (G := K) (-1)).Coprime (orderOf ζ)
⊢ 2 * n = orderOf (-ζ)

Tactic:
rw [neg_eq_neg_one_mul, (Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime]

Premises used: Commute.orderOf_mul_eq_mul_orderOf_of_coprime, neg_eq_neg_one_mul
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ 2 * n = orderOf.{u} (G := K) (-1) * orderOf ζ

Tactic:
simp [hζ.eq_orderOf]

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ (orderOf.{u} (G := K) (-1)).Coprime (orderOf ζ)

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

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ IsPrimitiveRoot (-ζ) (2 * n)

Tactic:
have hnegζ : IsPrimitiveRoot (-ζ) (2 * n) := by
    convert! IsPrimitiveRoot.orderOf (-ζ)
    rw [neg_eq_neg_one_mul, (Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
    · simp [hζ.eq_orderOf]
    · simp [← hζ.eq_orderOf, hno]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
obtain : ∀ (k : ℕ) (hkpos : 0 < k) (hkn : x ^ k = 1), ∃ (r : ℕ), x = (-ζ) ^ r
⊢ ∃ (r : ℕ), x = (-ζ) ^ r

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

Premises used: Iff.mp, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : NumberField K
inst_3 : 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
obtain : ∀ (l : ℕ) (hl : l ∈ k.divisors) (hlroot : IsRoot (cyclotomic l K) x), ∃ (r : ℕ), x = (-ζ) ^ r
⊢ ∃ (r : ℕ), x = (-ζ) ^ r

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

Premises used: Iff.mp, isRoot_of_unity_iff