awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
k : ℕ
hμ : IsPrimitiveRoot μ (HPow.hPow (α := ℕ) 2 (k + 1 + 1))
hC : IsCyclotomicExtension.{0, u_1} {HPow.hPow (α := ℕ) 2 (k + 1 + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (k + 1 + 1) = n
pos pos₁ pos₂ pos₃ :
  ∀ (hp : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) 2 (Module.finrank (↥ℚ⟮ζ⟯) K))
    (h :
      (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
        HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K))
    (hn : 2 < n) (q : ℕ) (hq : Nat.Prime q) (this : Fact (Nat.Prime q)) (hq' : q = 2) (k : ℕ)
    (hμ : IsPrimitiveRoot μ (HPow.hPow (α := ℕ) 2 (k + 1 + 1)))
    (hC : IsCyclotomicExtension.{0, u_1} {HPow.hPow (α := ℕ) 2 (k + 1 + 1)} ℚ ↥ℚ⟮ζ⟯) (hn' : q ^ (k + 1 + 1) = n),
    (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑2 : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑2 : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)

Tactic:
rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp

Premises used: IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hμ : IsPrimitiveRoot μ (q ^ (r + 1))
hC : IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (r + 1) = n
hq' : q = 2
pos :
  ∀ (hμ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1))
    (hC : IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯) (hn' : q ^ HAdd.hAdd (α := ℕ) 0 1 = n),
    (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
pos₁ :
  ∀ (k : ℕ) (hμ : IsPrimitiveRoot μ (q ^ (k + 1 + 1))) (hC : IsCyclotomicExtension.{0, u_1} {q ^ (k + 1 + 1)} ℚ ↥ℚ⟮ζ⟯)
    (hn' : q ^ (k + 1 + 1) = n), (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)

Tactic:
cases r with
            | zero =>
                rw [← hn', hq', zero_add, pow_one] at hn
                exact hn.false.elim
            | succ k =>
                rw [hq'] at hC hμ ⊢
                rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp

Premises used: IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow, False.elim, zero_add, pow_one, IsPrimitiveRoot.zero, LT.lt.false
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hμ : IsPrimitiveRoot μ (q ^ (r + 1))
hC : IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (r + 1) = n
hq' : ¬q = 2
neg neg₁ neg₂ neg₃ :
  ∀ (hp : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)) (hq : Nat.Prime q)
    (this : Fact (Nat.Prime q)) (r : ℕ) (hμ : IsPrimitiveRoot μ (q ^ (r + 1)))
    (hC : IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯) (hn' : q ^ (r + 1) = n) (hq' : ¬q = 2),
    (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)

Tactic:
rwa [hμ.norm_toInteger_sub_one_of_prime_ne_two hq'] at hp

Premises used: IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
t : ℕ
hn' : q ^ t = n
this : Fact (Nat.Prime q)
pos :
  ∀ (hn' : HPow.hPow (β := ℕ) q 0 = n),
    ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
pos₁ :
  ∀ (r : ℕ) (hn' : q ^ (r + 1) = n),
    ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s

Tactic:
cases t with
        | zero => simp [← hn'] at hn
        | succ r =>
          rw [← hn'] at hC hμ
          refine ⟨q, hq, r + 1, Module.finrank (ℚ⟮ζ⟯) K, r.add_one_ne_zero, hn'.symm, ?_⟩
          by_cases hq' : q = 2
          · cases r with
            | zero =>
                rw [← hn', hq', zero_add, pow_one] at hn
                exact hn.false.elim
            | succ k =>
                rw [hq'] at hC hμ ⊢
                rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp
          · rwa [hμ.norm_toInteger_sub_one_of_prime_ne_two hq'] at hp

Premises used: IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow, False.elim, zero_add, pow_one, IsPrimitiveRoot.zero, LT.lt.false
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h_1 :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
h : ∀ (q : ℕ) (_ : Nat.Prime q) (t : ℕ), q ^ t ≠ n
neg :
  ∀ (hp : p = 1)
    (h :
      (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
        HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K))
    (hn : 2 < n) (h : ∀ (q : ℕ) (_ : Nat.Prime q) (t : ℕ), q ^ t ≠ n),
    ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
neg₁ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s

Tactic:
rw [IsPrimitiveRoot.norm_toInteger_sub_one_eq_one hμ hn, one_pow,
          Int.natCast_dvd_ofNat, Nat.dvd_one] at hp

Premises used: one_pow, Nat.dvd_one, IsPrimitiveRoot.norm_toInteger_sub_one_eq_one, Int.natCast_dvd_ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : p = 1
h_1 :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
h : ∀ (q : ℕ) (_ : Nat.Prime q) (t : ℕ), q ^ t ≠ n
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s

Tactic:
(Nat.Prime.ne_one hF.out hp).elim

Premises used: False.elim, Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : p = 1
h_1 :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
h : ∀ (q : ℕ) (_ : Nat.Prime q) (t : ℕ), q ^ t ≠ n
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s

Tactic:
exact (Nat.Prime.ne_one hF.out hp).elim

Premises used: False.elim, Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h_1 :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
h : ∀ (q : ℕ) (_ : Nat.Prime q) (t : ℕ), q ^ t ≠ n
⊢ ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n

Tactic:
fun {p} a k ↦ h p a k
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h_1 :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
h : ∀ (q : ℕ) (_ : Nat.Prime q) (t : ℕ), q ^ t ≠ n
⊢ ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n

Tactic:
exact fun {p} a k ↦ h p a k
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 = n
inr :
  ∀ (hC : IsCyclotomicExtension.{0, u_1} {2} ℚ ↥ℚ⟮ζ⟯) (hμ : IsPrimitiveRoot μ n) (hμ_1 : IsPrimitiveRoot μ 2)
    (hp :
      (↑p : ℤ) ∣
        HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K))
    (h :
      (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
        HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K))
    (hn : 2 = n),
    ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ 2 = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s

Tactic:
rw [← hn] at hμ hC ⊢
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {2} ℚ ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hμ : IsPrimitiveRoot μ 2
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 = n
rw rw₁ : Eq (α := ℕ) 2 2
⊢ 2 = HPow.hPow (α := ℕ) (β := ℕ) 2 1

Tactic:
rw [pow_one]

Premises used: pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {2} ℚ ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hμ : IsPrimitiveRoot μ 2
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 = n
inr : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑2 : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ 2 = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s

Tactic:
refine ⟨2, Nat.prime_two, 1, Module.finrank ℚ⟮ζ⟯ K, one_ne_zero, by rw [pow_one], ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
rsuffices :
  ∀ (q : ℕ) (hq : Nat.Prime q) (t s : ℕ) (ht₁ : t ≠ 0) (ht₂ : n = q ^ t)
    (hs : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s), p ∣ n
⊢ p ∣ n

Tactic:
rsuffices ⟨q, hq, t, s, ht₁, ht₂, hs⟩ :
      ∃ q, q.Prime ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ (p : ℤ) ∣ (q : ℤ) ^ s := by
    obtain hn | hn := lt_or_eq_of_le hn
    · by_cases! h : ∃ q, q.Prime ∧ ∃ t, q ^ t = n
      · obtain ⟨q, hq, t, hn'⟩ := h
        have : Fact (Nat.Prime q) := ⟨hq⟩
        cases t with
        | zero => simp [← hn'] at hn
        | succ r =>
          rw [← hn'] at hC hμ
          refine ⟨q, hq, r + 1, Module.finrank (ℚ⟮ζ⟯) K, r.add_one_ne_zero, hn'.symm, ?_⟩
          by_cases hq' : q = 2
          · cases r with
            | zero =>
                rw [← hn', hq', zero_add, pow_one] at hn
                exact hn.false.elim
            | succ k =>
                rw [hq'] at hC hμ ⊢
                rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp
          · rwa [hμ.norm_toInteger_sub_one_of_prime_ne_two hq'] at hp
      · rw [IsPrimitiveRoot.norm_toInteger_sub_one_eq_one hμ hn, one_pow,
          Int.natCast_dvd_ofNat, Nat.dvd_one] at hp
        · exact (Nat.Prime.ne_one hF.out hp).elim
        · exact fun {p} a k ↦ h p a k
    · rw [← hn] at hμ hC ⊢
      refine ⟨2, Nat.prime_two, 1, Module.finrank ℚ⟮ζ⟯ K, one_ne_zero, by rw [pow_one], ?_⟩
      rwa [hμ.norm_toInteger_sub_one_of_eq_two, neg_eq_neg_one_mul, mul_pow, IsUnit.dvd_mul_left
        ((isUnit_pow_iff Module.finrank_pos.ne').mpr isUnit_neg_one)] at hp

Premises used: Nat.cast
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
q : ℕ
hq : Nat.Prime q
t s : ℕ
ht₁ : t ≠ 0
ht₂ : n = q ^ t
hs : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
⊢ p ∣ q ^ s

Tactic:
rw [← Int.natCast_pow, Int.natCast_dvd_natCast] at hs

Premises used: Int.natCast_pow, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
q : ℕ
hq : Nat.Prime q
t s : ℕ
ht₁ : t ≠ 0
ht₂ : n = q ^ t
hs : p ∣ q ^ s
⊢ p = q

Tactic:
(Nat.prime_dvd_prime_iff_eq hF.out hq).mp (hF.out.dvd_of_dvd_pow hs)

Premises used: Nat.Prime.dvd_of_dvd_pow, Nat.prime_dvd_prime_iff_eq, Iff.mp, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
q : ℕ
hq : Nat.Prime q
t s : ℕ
ht₁ : t ≠ 0
ht₂ : n = q ^ t
hs : p ∣ q ^ s
⊢ p = q

Tactic:
exact (Nat.prime_dvd_prime_iff_eq hF.out hq).mp (hF.out.dvd_of_dvd_pow hs)

Premises used: Nat.Prime.dvd_of_dvd_pow, Nat.prime_dvd_prime_iff_eq, Iff.mp, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
q : ℕ
hq : Nat.Prime q
t s : ℕ
ht₁ : t ≠ 0
ht₂ : n = q ^ t
hs : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
⊢ p = q

Tactic:
have : p = q := by
    rw [← Int.natCast_pow, Int.natCast_dvd_natCast] at hs
    exact (Nat.prime_dvd_prime_iff_eq hF.out hq).mp (hF.out.dvd_of_dvd_pow hs)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
q : ℕ
hq : Nat.Prime q
t s : ℕ
ht₁ : t ≠ 0
ht₂ : n = q ^ t
hs : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
this : p = q
rw : q ∣ q ^ t
⊢ p ∣ n

Tactic:
rw [ht₂, this]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
q : ℕ
hq : Nat.Prime q
t s : ℕ
ht₁ : t ≠ 0
ht₂ : n = q ^ t
hs : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
this : p = q
⊢ q ∣ q ^ t

Tactic:
dvd_pow_self _ ht₁

Premises used: dvd_pow_self
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
q : ℕ
hq : Nat.Prime q
t s : ℕ
ht₁ : t ≠ 0
ht₂ : n = q ^ t
hs : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
this : p = q
⊢ q ∣ q ^ t

Tactic:
exact dvd_pow_self _ ht₁

Premises used: dvd_pow_self
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
⊢ IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)

Tactic:
have hζ := IsCyclotomicExtension.zeta_spec (p ^ k) ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
⊢ NumberField K

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {p ^ k} ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
a :
  Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (NumberField.discr K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) :
      ℚ)
⊢ NumberField.discr K =
    HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
apply (algebraMap ℤ ℚ).injective_int

Premises used: Algebra.algebraMap, Rat, Int, RingHom.injective_int
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ K) (p ^ k)
this : NumberField K
pB₁ : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
a :
  Algebra.discr (ι := Fin pB₁.dim) ℚ (B := K)
      (⇑(Module.Basis.localizationLocalization ℚ ℤ⁰ K pB₁.basis) : (a : Fin pB₁.dim) → K) =
    (algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1)))
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (NumberField.discr K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ (k - 1) * ((p - 1) * k - 1))) :
      ℚ)

Tactic:
rw [← NumberField.discr_eq_discr _ pB₁.basis, ← Algebra.discr_localizationLocalization ℤ ℤ⁰ K]

Premises used: nonZeroDivisors, NumberField.discr_eq_discr, Int, PowerBasis.basis, Algebra.discr_localizationLocalization