awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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 ∣ 2 * n
have key : φ (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))
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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 ∣ 2 * n
have key₁ : φ (l.lcm n) ≤ φ n
Tactic: rw [IsCyclotomicExtension.finrank K (cyclotomic.irreducible_rat (NeZero.pos n))] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ l ∣ 2 * n
have rcases : ∀ (r : ℕ) (hr : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n * r), l ∣ 2 * n
Tactic: rcases _root_.dvd_lcm_right l n with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
⊢ l ∣ 2 * n
have ineq : φ n * φ r ≤ φ (n * r)
Tactic: have ineq := Nat.totient_super_multiplicative n r
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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)
⊢ l ∣ 2 * n
have ineq₁ : φ n * φ r ≤ φ (@GCDMonoid.lcm _ instCommMonoidWithZero _ l n)
Tactic: rw [← hr] at ineq
Cleared hypotheses: ineq
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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)
⊢ l ∣ 2 * n
have key₁ : φ r ≤ 1
Tactic: replace key := (mul_le_iff_le_one_right (Nat.totient_pos.2 (NeZero.pos n))).mp (le_trans ineq key)
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
have refine : ∀ (h : r = 0), False
Tactic: refine Nat.pos_of_ne_zero (fun h ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
⊢ l ∣ 2 * n
have rpos : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
⊢ l ∣ 2 * n
have key₁ : r = 1 ∨ r = 2
Tactic: replace key := (Nat.dvd_prime Nat.prime_two).1 (Nat.dvd_two_of_totient_le_one rpos key)
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ l ∣ 2 * n
have inl : ∀ (key : r = 1), l ∣ 2 * n
Tactic: rcases key with (key | key)
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ l ∣ 2 * n
have inr : ∀ (key : r = 2), l ∣ 2 * n
Tactic: rcases key with (key | key)
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
⊢ l ∣ 2 * n
have hr₁ : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = n
Tactic: rw [key, mul_one] at hr
Cleared hypotheses: hr, ineq, rpos, key
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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 * n
have inl : l ∣ 2 * @GCDMonoid.lcm _ instCommMonoidWithZero _ l n
Tactic: rw [← hr]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
⊢ l ∣ 2 * n
have hr₁ : @GCDMonoid.lcm _ instCommMonoidWithZero _ l n = 2 * n
Tactic: rw [key, mul_comm] at hr
Cleared hypotheses: hr, ineq, rpos, key
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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)
have h : 2 * n = orderOf (-ζ)
Tactic: convert! IsPrimitiveRoot.orderOf (-ζ)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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 (-ζ)
have h : 2 * n = orderOf.{u} (G := K) (-1) * orderOf ζ
Tactic: rw [neg_eq_neg_one_mul, (Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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 ζ
⊢ 2 * n = orderOf (-ζ)
have h₁ : (orderOf.{u} (G := K) (-1)).Coprime (orderOf ζ)
Tactic: rw [neg_eq_neg_one_mul, (Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
⊢ ∃ (r : ℕ), x = (-ζ) ^ r
have hnegζ : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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)
⊢ ∃ (r : ℕ), x = (-ζ) ^ r
have obtain : ∀ (k : ℕ) (hkpos : 0 < k) (hkn : x ^ k = 1), ∃ (r : ℕ), x = (-ζ) ^ r
Tactic: obtain ⟨k, hkpos, hkn⟩ := isOfFinOrder_iff_pow_eq_one.1 hx
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ ∃ (r : ℕ), x = (-ζ) ^ r
have obtain : ∀ (l : ℕ) (hl : l ∈ k.divisors) (hlroot : IsRoot (cyclotomic l K) x), ∃ (r : ℕ), x = (-ζ) ^ r
Tactic: obtain ⟨l, hl, hlroot⟩ := (isRoot_of_unity_iff hkpos _).1 hkn
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
l : ℕ
hl : l ∈ k.divisors
hlroot : IsRoot (cyclotomic l K) x
⊢ ∃ (r : ℕ), x = (-ζ) ^ r
have hlzero : NeZero l
Tactic: have hlzero : NeZero l := ⟨fun h ↦ by simp [h] at hl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
l : ℕ
hl : l ∈ k.divisors
hlroot : IsRoot (cyclotomic l K) x
hlzero : NeZero l
⊢ ∃ (r : ℕ), x = (-ζ) ^ r
have this : NeZero.{u} (R := K) (↑l : K)
Tactic: have : NeZero (l : K) := ⟨NeZero.natCast_ne l K⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
l : ℕ
hl : l ∈ k.divisors
hlroot : IsRoot (cyclotomic l K) x
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
⊢ ∃ (r : ℕ), x = (-ζ) ^ r
have hlroot₁ : IsPrimitiveRoot x l
Tactic: rw [isRoot_cyclotomic_iff] at hlroot
Cleared hypotheses: hlroot, hlzero, this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
⊢ ∃ (r : ℕ), x = (-ζ) ^ r
have obtain : ∀ (a : ℕ) (ha : 2 * n = l * a), ∃ (r : ℕ), x = (-ζ) ^ r
Tactic: obtain ⟨a, ha⟩ := hlroot.dvd_of_isCyclotomicExtension n hlzero.1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
a : ℕ
ha : 2 * n = l * a
⊢ x ^ (2 * n) = 1
have rw : x ^ (l * a) = 1
Tactic: rw [ha, pow_mul, hlroot.pow_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
a : ℕ
ha : 2 * n = l * a
rw : x ^ (l * a) = 1
⊢ x ^ (2 * n) = 1
have rw₁ : (x ^ l) ^ a = 1
Tactic: rw [ha, pow_mul, hlroot.pow_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
a : ℕ
ha : 2 * n = l * a
rw : x ^ (l * a) = 1
rw₁ : (x ^ l) ^ a = 1
⊢ x ^ (2 * n) = 1
have rw₂ : HPow.hPow (α := K) 1 a = 1
Tactic: rw [ha, pow_mul, hlroot.pow_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
a : ℕ
ha : 2 * n = l * a
rw : x ^ (l * a) = 1
rw₁ : (x ^ l) ^ a = 1
rw₂ : HPow.hPow (α := K) 1 a = 1
⊢ x ^ (2 * n) = 1
have rw₃ : Eq.{u + 1} (α := K) 1 1
Tactic: rw [ha, pow_mul, hlroot.pow_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
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
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
a : ℕ
ha : 2 * n = l * a
⊢ ∃ (r : ℕ), x = (-ζ) ^ r
have hlroot₁ : x ^ (2 * n) = 1
Tactic: replace hlroot : x ^ (2 * n) = 1 := by rw [ha, pow_mul, hlroot.pow_eq_one, one_pow]
Cleared hypotheses: hlroot
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
l : ℕ
hl : l ∈ k.divisors
hlzero : NeZero l
this : NeZero.{u} (R := K) (↑l : K)
a : ℕ
ha : 2 * n = l * a
hlroot : x ^ (2 * n) = 1
⊢ ∃ (r : ℕ), x = (-ζ) ^ r
have obtain : ∀ (s : ℕ) (hs : (-ζ) ^ s = x), ∃ (r : ℕ), x = (-ζ) ^ r
Tactic: obtain ⟨s, -, hs⟩ := hnegζ.eq_pow_of_pow_eq_one hlroot
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
⊢ ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r
have obtain : ∀ (r : ℕ) (hr : x = (-ζ) ^ r), ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r
Tactic: obtain ⟨r, hr⟩ := hζ.exists_neg_pow_of_isOfFinOrder hno hx
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
r : ℕ
hr : x = (-ζ) ^ r
⊢ ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r
have refine : x = ζ ^ (r % n) ∨ x = -ζ ^ (r % n)
Tactic: refine ⟨r % n, Nat.mod_lt _ (NeZero.pos _), ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
r : ℕ
hr : x = (-ζ) ^ r
⊢ x = ζ ^ (r % n) ∨ x = -ζ ^ (r % n)
have rw : (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r
Tactic: rw [show ζ ^ (r % n) = ζ ^ r from (IsPrimitiveRoot.eq_orderOf hζ).symm ▸ pow_mod_orderOf .., hr]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
r : ℕ
hr : x = (-ζ) ^ r
⊢ (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r
have inl : ∀ (h : Even r), (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r
Tactic: rcases Nat.even_or_odd r with (h | h)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
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
r : ℕ
hr : x = (-ζ) ^ r
inl : ∀ (h : Even r), (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r
⊢ (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r
have inr : ∀ (h : Odd r), (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r
Tactic: rcases Nat.even_or_odd r with (h | h)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
K : Type u
L : Type v
inst : CommRing L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
hζ : IsPrimitiveRoot ζ 2
inst_3 : IsDomain L
⊢ (Algebra.norm K : (a : L) → K) ζ = HPow.hPow (α := K) (-1) (Module.finrank K L)
have rw : (Algebra.norm K : (a : L) → K) (-1) = HPow.hPow (α := K) (-1) (Module.finrank K L)
Tactic: rw [hζ.eq_neg_one_of_two_right, show -1 = algebraMap K L (-1) by simp, Algebra.norm_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
K : Type u
L : Type v
inst : CommRing L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
hζ : IsPrimitiveRoot ζ 2
inst_3 : IsDomain L
rw : (Algebra.norm K : (a : L) → K) (-1) = HPow.hPow (α := K) (-1) (Module.finrank K L)
⊢ (Algebra.norm K : (a : L) → K) ζ = HPow.hPow (α := K) (-1) (Module.finrank K L)
have rw₁ : (Algebra.norm K : (a : L) → K) ((algebraMap K L : (a : K) → L) (-1) : L) = HPow.hPow (α := K) (-1) (Module.finrank K L)
Tactic: rw [hζ.eq_neg_one_of_two_right, show -1 = algebraMap K L (-1) by simp, Algebra.norm_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
K : Type u
L : Type v
inst : CommRing L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
hζ : IsPrimitiveRoot ζ 2
inst_3 : IsDomain L
rw : (Algebra.norm K : (a : L) → K) (-1) = HPow.hPow (α := K) (-1) (Module.finrank K L)
rw₁ :
  (Algebra.norm K : (a : L) → K) ((algebraMap K L : (a : K) → L) (-1) : L) =
    HPow.hPow (α := K) (-1) (Module.finrank K L)
⊢ (Algebra.norm K : (a : L) → K) ζ = HPow.hPow (α := K) (-1) (Module.finrank K L)
have rw₂ : HPow.hPow (α := K) (-1) (Module.finrank K L) = HPow.hPow (α := K) (-1) (Module.finrank K L)
Tactic: rw [hζ.eq_neg_one_of_two_right, show -1 = algebraMap K L (-1) by simp, Algebra.norm_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
have this : NeZero.{u} (R := K) (↑n : K)
Tactic: haveI := IsCyclotomicExtension.neZero' n K L
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
have pos : ∀ (h1 : n = 1), Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
Tactic: by_cases h1 : n = 1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
pos : ∀ (h1 : n = 1), Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
have neg : ∀ (h1 : ¬n = 1), Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
Tactic: by_cases h1 : n = 1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
have hζ₁ : ζ = 1
Tactic: rw [h1, one_right_iff] at hζ
Cleared hypotheses: hζ, inst_4, inst_5, hn, hirr, this, h1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : ζ = 1
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
have pos : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) 1 : K) (1 : K)
Tactic: rw [hζ, show 1 = algebraMap K L 1 by simp, Algebra.norm_algebraMap, one_pow]