awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hp : Dvd.dvd (α := ℤ) ((↑p : ℤ) : ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
this : NeZero n
obtain :
  ∀ (μ : ↥ℚ⟮ζ⟯) (hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯) (hμ : IsPrimitiveRoot μ n)
    (h :
      (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
        HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)),
    p ∣ n
⊢ p ∣ n

Tactic:
obtain ⟨μ, hC, hμ, h⟩ :
      ∃ μ : ℚ⟮ζ⟯, ∃ (_ : IsCyclotomicExtension {n} ℚ ℚ⟮ζ⟯), ∃ (hμ : IsPrimitiveRoot μ n),
      norm ℤ (hζ.toInteger - 1) = norm ℤ (hμ.toInteger - 1) ^ Module.finrank ℚ⟮ζ⟯ K := by
    refine ⟨IntermediateField.AdjoinSimple.gen ℚ ζ,
      intermediateField_adjoin_isCyclotomicExtension ℚ hζ, coe_submonoidClass_iff.mp hζ, ?_⟩
    have : NumberField ℚ⟮ζ⟯ := of_intermediateField _
    rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, RingOfIntegers.map_mk,
      show ζ - 1 = algebraMap ℚ⟮ζ⟯ K (IntermediateField.AdjoinSimple.gen ℚ ζ - 1) by rfl,
      ← norm_norm (S := ℚ⟮ζ⟯), Algebra.norm_algebraMap, map_pow, map_pow, ← norm_localization ℤ
      (nonZeroDivisors ℤ) (Sₘ := ℚ⟮ζ⟯), map_sub (algebraMap _ _), RingOfIntegers.map_mk, map_one]

Premises used: Rat, HSub.hSub, Membership.mem, Subtype, Int, IsCyclotomicExtension, IsPrimitiveRoot.toInteger, IntermediateField.adjoin, Algebra.norm, Singleton.singleton, OfNat.ofNat, DFunLike.coe, Module.finrank
-- 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
hp : Dvd.dvd (α := ℤ) ((↑p : ℤ) : ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)

Tactic:
rw [h] at hp
-- 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
hp : Dvd.dvd (α := ℤ) ((↑p : ℤ) : ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hp₁ :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)

Tactic:
rw [h] at hp
-- 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)
inl :
  ∀ (hn : 2 < n),
    ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
inr :
  ∀ (hn : 2 = 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:
obtain hn | hn := lt_or_eq_of_le hn

Premises used: lt_or_eq_of_le
-- 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
pos :
  ∀ (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 :
  ∀ (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
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s

Tactic:
by_cases! h : ∃ q, q.Prime ∧ ∃ t, q ^ t = n
-- 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
pos :
  ∀ (q : ℕ) (hq : Nat.Prime q) (t : ℕ) (hn' : q ^ t = 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:
obtain ⟨q, hq, t, hn'⟩ := h
-- 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
q : ℕ
hq : Nat.Prime q
t : ℕ
hn' : q ^ t = n
⊢ Fact (Nat.Prime q)

Tactic:
have : Fact (Nat.Prime q) := ⟨hq⟩
-- 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
this : Fact (Nat.Prime q)
hn' : HPow.hPow (β := ℕ) q 0 = n
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s

Tactic:
simp [← hn'] at hn
-- 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
this : Fact (Nat.Prime q)
r : ℕ
hn' : q ^ (r + 1) = n
⊢ IsPrimitiveRoot μ (q ^ (r + 1))

Tactic:
rw [← hn'] at hC hμ
-- 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
this : Fact (Nat.Prime q)
r : ℕ
hn' : q ^ (r + 1) = n
hμ₁ : IsPrimitiveRoot μ (q ^ (r + 1))
⊢ IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯

Tactic:
rw [← hn'] at hC hμ
-- 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
this : Fact (Nat.Prime q)
r : ℕ
hn' : q ^ (r + 1) = n
hμ₁ : IsPrimitiveRoot μ (q ^ (r + 1))
hC₁ : IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
⊢ q ^ (r + 1) = n

Tactic:
rw [← hn'] at hC hμ
-- 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
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s

Tactic:
⟨q, hq, r + 1, Module.finrank (ℚ⟮ζ⟯) K, r.add_one_ne_zero, hn'.symm, ?_⟩

Premises used: Rat, Nat.add_one_ne_zero, Membership.mem, Subtype, HAdd.hAdd, And.intro, IntermediateField.adjoin, Exists.intro, Singleton.singleton, OfNat.ofNat, Eq.symm, Module.finrank
-- 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
pos : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s

Tactic:
refine ⟨q, hq, r + 1, Module.finrank (ℚ⟮ζ⟯) K, r.add_one_ne_zero, hn'.symm, ?_⟩
-- 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
pos : ∀ (hq' : q = 2), (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
neg : ∀ (hq' : ¬q = 2), (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)

Tactic:
by_cases hq' : q = 2
-- 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
hμ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1)
hC : IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ HAdd.hAdd (α := ℕ) 0 1 = n
⊢ LT.lt (α := ℕ) 2 2

Tactic:
rw [← hn', hq', zero_add, pow_one] at hn

Premises used: zero_add, 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_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
hμ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1)
hC : IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ HAdd.hAdd (α := ℕ) 0 1 = n
hn₁ : LT.lt (α := ℕ) 2 2
⊢ Nat.Prime q

Tactic:
rw [← hn', hq', zero_add, pow_one] at hn

Premises used: zero_add, 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_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
hμ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1)
hC : IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ HAdd.hAdd (α := ℕ) 0 1 = n
hn₁ : LT.lt (α := ℕ) 2 2
hq₁ : Nat.Prime q
⊢ Fact (Nat.Prime q)

Tactic:
rw [← hn', hq', zero_add, pow_one] at hn

Premises used: zero_add, 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_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
hμ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1)
hC : IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ HAdd.hAdd (α := ℕ) 0 1 = n
hn₁ : LT.lt (α := ℕ) 2 2
hq₁ : Nat.Prime q
this₁ : Fact (Nat.Prime q)
⊢ q = 2

Tactic:
rw [← hn', hq', zero_add, pow_one] at hn

Premises used: zero_add, 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_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
hμ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1)
hC : IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ HAdd.hAdd (α := ℕ) 0 1 = n
hn₁ : LT.lt (α := ℕ) 2 2
hq₁ : Nat.Prime q
this₁ : Fact (Nat.Prime q)
hq'₁ : q = 2
⊢ IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1)

Tactic:
rw [← hn', hq', zero_add, pow_one] at hn

Premises used: zero_add, 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_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
hμ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1)
hC : IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ HAdd.hAdd (α := ℕ) 0 1 = n
hn₁ : LT.lt (α := ℕ) 2 2
hq₁ : Nat.Prime q
this₁ : Fact (Nat.Prime q)
hq'₁ : q = 2
hμ₁ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯

Tactic:
rw [← hn', hq', zero_add, pow_one] at hn

Premises used: zero_add, 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_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
hμ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1)
hC : IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ HAdd.hAdd (α := ℕ) 0 1 = n
hn₁ : LT.lt (α := ℕ) 2 2
hq₁ : Nat.Prime q
this₁ : Fact (Nat.Prime q)
hq'₁ : q = 2
hμ₁ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1)
hC₁ : IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯
⊢ q ^ HAdd.hAdd (α := ℕ) 0 1 = n

Tactic:
rw [← hn', hq', zero_add, pow_one] at hn

Premises used: zero_add, 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_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)
q : ℕ
hn : LT.lt (α := ℕ) 2 2
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
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)

Tactic:
hn.false.elim

Premises used: False.elim, 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)
q : ℕ
hn : LT.lt (α := ℕ) 2 2
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
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)

Tactic:
exact hn.false.elim

Premises used: False.elim, 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)
hq' : q = 2
k : ℕ
hμ : IsPrimitiveRoot μ (q ^ (k + 1 + 1))
hC : IsCyclotomicExtension.{0, u_1} {q ^ (k + 1 + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (k + 1 + 1) = n
pos :
  ∀ (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 (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)

Tactic:
rw [hq'] at hC hμ ⊢