awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ_1 : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot (IsUnit.unit (a := hζ_1.toInteger) ⋯) n
⊢ n = orderOf (↑⋯.unit : (𝓞 K)ˣ)

Tactic:
hζ.eq_orderOf

Premises used: Units.copy, IsPrimitiveRoot.eq_orderOf, IsUnit.unit
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ_1 : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot (IsUnit.unit (a := hζ_1.toInteger) ⋯) n
⊢ n = orderOf (↑⋯.unit : (𝓞 K)ˣ)

Tactic:
exact hζ.eq_orderOf

Premises used: IsPrimitiveRoot.eq_orderOf
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ_1 : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot (IsUnit.unit (a := hζ_1.toInteger) ⋯) n
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) (↑⋯.unit : (𝓞 K)ˣ)

Tactic:
(CommGroup.mem_torsion _ _).mpr ⟨n, NeZero.pos n, ?_⟩

Premises used: Iff.mpr, Set.Mem, And.intro, Exists.intro, NeZero.pos, CommGroup.mem_torsion
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ_1 : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot (IsUnit.unit (a := hζ_1.toInteger) ⋯) n
refine : Function.IsPeriodicPt (fun (x : (𝓞 K)ˣ) ↦ (↑⋯.unit : (𝓞 K)ˣ) * x) n 1
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) (↑⋯.unit : (𝓞 K)ˣ)

Tactic:
refine (CommGroup.mem_torsion _ _).mpr ⟨n, NeZero.pos n, ?_⟩

Premises used: Iff.mpr, And.intro, Exists.intro, NeZero.pos, CommGroup.mem_torsion
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ_1 : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot (IsUnit.unit (a := hζ_1.toInteger) ⋯) n
rw : (↑⋯.unit : (𝓞 K)ˣ) ^ n = 1
⊢ Function.IsPeriodicPt (fun (x : (𝓞 K)ˣ) ↦ (↑⋯.unit : (𝓞 K)ˣ) * x) n 1

Tactic:
rw [isPeriodicPt_mul_iff_pow_eq_one]

Premises used: isPeriodicPt_mul_iff_pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ_1 : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot (IsUnit.unit (a := hζ_1.toInteger) ⋯) n
⊢ (↑⋯.unit : (𝓞 K)ˣ) ^ n = 1

Tactic:
hζ.pow_eq_one

Premises used: IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ_1 : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot (IsUnit.unit (a := hζ_1.toInteger) ⋯) n
⊢ (↑⋯.unit : (𝓞 K)ˣ) ^ n = 1

Tactic:
exact hζ.pow_eq_one

Premises used: IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
⊢ IsPrimitiveRoot (zeta n ℚ K) n

Tactic:
have hζ := hK.zeta_spec
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
rw : ∃ (μ : ↥(torsion K)), orderOf μ = Nat.card.{u} ↥(torsion K)
⊢ ∃ (μ : ↥(torsion K)), orderOf μ = torsionOrder K

Tactic:
rw [torsionOrder, Fintype.card_eq_nat_card]

Premises used: NumberField.Units.torsionOrder, Fintype.card_eq_nat_card
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
⊢ ∃ (μ : ↥(torsion K)), orderOf μ = Nat.card.{u} ↥(torsion K)

Tactic:
IsCyclic.exists_ofOrder_eq_natCard

Premises used: IsCyclic.exists_ofOrder_eq_natCard
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
⊢ ∃ (μ : ↥(torsion K)), orderOf μ = Nat.card.{u} ↥(torsion K)

Tactic:
exact IsCyclic.exists_ofOrder_eq_natCard

Premises used: IsCyclic.exists_ofOrder_eq_natCard
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
obtain : ∀ (μ : ↥(torsion K)) (hμ : orderOf μ = torsionOrder K), torsionOrder K = if Even n then n else 2 * n
⊢ torsionOrder K = if Even n then n else 2 * n

Tactic:
obtain ⟨μ, hμ⟩ : ∃ μ : torsion K, orderOf μ = torsionOrder K := by
    rw [torsionOrder, Fintype.card_eq_nat_card]
    exact IsCyclic.exists_ofOrder_eq_natCard

Premises used: NumberField.Units.torsionOrder, NumberField.Units.torsion
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : orderOf μ = torsionOrder K
⊢ IsPrimitiveRoot (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) (torsionOrder K)

Tactic:
rw [← IsPrimitiveRoot.iff_orderOf, ← IsPrimitiveRoot.coe_submonoidClass_iff,
    ← IsPrimitiveRoot.coe_units_iff] at hμ

Premises used: IsPrimitiveRoot.coe_units_iff, IsPrimitiveRoot.iff_orderOf, IsPrimitiveRoot.coe_submonoidClass_iff
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) (torsionOrder K)
⊢ IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)

Tactic:
replace hμ := hμ.map_of_injective (FaithfulSMul.algebraMap_injective (𝓞 K) K)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
⊢ IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))

Tactic:
have h := hζ.pow_mul_pow_lcm hμ (NeZero.ne _) (torsionOrder_ne_zero K)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
⊢ NeZero (n.lcm (torsionOrder K))

Tactic:
have : NeZero (n.lcm (torsionOrder K)) :=
    NeZero.of_pos <| Nat.lcm_pos_iff.mpr ⟨NeZero.pos n, torsionOrder_pos K⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this : NeZero (n.lcm (torsionOrder K))
⊢ IsCyclotomicExtension ({n} ∪ {n.lcm (torsionOrder K)}) ℚ K

Tactic:
have := hK.union_of_isPrimitiveRoot _ _ _ h
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension ({n} ∪ {n.lcm (torsionOrder K)}) ℚ K
h₁ :
  ∀ (this : IsCyclotomicExtension ({n.lcm (torsionOrder K)} ∪ {n}) ℚ K),
    ∃ (s : ℕ), Membership.mem (γ := Set ℕ) {n.lcm (torsionOrder K)} s ∧ s ≠ 0 ∧ n ∣ s
⊢ IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K

Tactic:
rwa [Set.union_comm, ← IsCyclotomicExtension.iff_union_of_dvd] at this

Premises used: IsCyclotomicExtension.iff_union_of_dvd, Set.union_comm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension ({n.lcm (torsionOrder K)} ∪ {n}) ℚ K
⊢ Membership.mem (γ := Set ℕ) {n.lcm (torsionOrder K)} (n.lcm (torsionOrder K))

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension ({n.lcm (torsionOrder K)} ∪ {n}) ℚ K
⊢ ∃ (s : ℕ), Membership.mem (γ := Set ℕ) {n.lcm (torsionOrder K)} s ∧ s ≠ 0 ∧ n ∣ s

Tactic:
exact ⟨n.lcm (torsionOrder K), by simp, NeZero.ne _, Nat.dvd_lcm_left _ _⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this : NeZero (n.lcm (torsionOrder K))
⊢ IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K

Tactic:
have : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K := by
    have := hK.union_of_isPrimitiveRoot _ _ _ h
    rwa [Set.union_comm, ← IsCyclotomicExtension.iff_union_of_dvd] at this
    exact ⟨n.lcm (torsionOrder K), by simp, NeZero.ne _, Nat.dvd_lcm_left _ _⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
⊢ φ n = φ (n.lcm (torsionOrder K))

Tactic:
have h_main := (IsCyclotomicExtension.Rat.finrank n K).symm.trans <|
    (IsCyclotomicExtension.Rat.finrank (n.lcm (torsionOrder K)) K)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
inl : ∀ (hn : Even n), torsionOrder K = if Even n then n else 2 * n
inr : ∀ (hn : Odd n), torsionOrder K = if Even n then n else 2 * n
⊢ torsionOrder K = if Even n then n else 2 * n

Tactic:
obtain hn | hn := Nat.even_or_odd n

Premises used: Nat.even_or_odd
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Even n
inl : torsionOrder K = n
⊢ torsionOrder K = if Even n then n else 2 * n

Tactic:
rw [if_pos hn]

Premises used: if_pos
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Even n
inl : torsionOrder K ∣ n
inl₁ : n ∣ torsionOrder K
⊢ torsionOrder K = n

Tactic:
apply dvd_antisymm

Premises used: dvd_antisymm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Even n
⊢ n = n.lcm (torsionOrder K)

Tactic:
have := hn.eq_of_totient_eq_totient (Nat.dvd_lcm_left _ _) h_main
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this_2 : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Even n
this : n = n.lcm (torsionOrder K)
inl : ∀ (this : n.lcm (torsionOrder K) = n), torsionOrder K ∣ n
inl₁ inl₂ inl₃ inl₄ : ∀ (this : torsionOrder K ∣ n), torsionOrder K ∣ n
⊢ torsionOrder K ∣ n

Tactic:
rwa [eq_comm, Nat.lcm_eq_left_iff_dvd] at this

Premises used: eq_comm, Nat.lcm_eq_left_iff_dvd
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Even n
⊢ n ∣ torsionOrder K

Tactic:
dvd_torsionOrder_of_isPrimitiveRoot hζ

Premises used: NumberField.Units.dvd_torsionOrder_of_isPrimitiveRoot
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Even n
⊢ n ∣ torsionOrder K

Tactic:
exact dvd_torsionOrder_of_isPrimitiveRoot hζ

Premises used: NumberField.Units.dvd_torsionOrder_of_isPrimitiveRoot
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Odd n
inr : torsionOrder K = 2 * n
⊢ torsionOrder K = if Even n then n else 2 * n

Tactic:
rw [if_neg (Nat.not_even_iff_odd.mpr hn)]

Premises used: Iff.mpr, Nat.not_even_iff_odd, if_neg
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Odd n
inr : ∀ (this : 2 * n = n.lcm (torsionOrder K)), torsionOrder K = 2 * n
inr₁ : ¬n = n.lcm (torsionOrder K)
⊢ torsionOrder K = 2 * n

Tactic:
have := (Nat.eq_or_eq_of_totient_eq_totient (Nat.dvd_lcm_left _ _) h_main).resolve_left ?_
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this_2 : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Odd n
this : 2 * n = n.lcm (torsionOrder K)
inr : n ∣ torsionOrder K
⊢ torsionOrder K = 2 * n

Tactic:
rw [this, eq_comm, Nat.lcm_eq_right_iff_dvd]

Premises used: eq_comm, Nat.lcm_eq_right_iff_dvd
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this_2 : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Odd n
this : 2 * n = n.lcm (torsionOrder K)
⊢ n ∣ torsionOrder K

Tactic:
dvd_torsionOrder_of_isPrimitiveRoot hζ

Premises used: NumberField.Units.dvd_torsionOrder_of_isPrimitiveRoot
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot (M := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) : K)
        (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this_1 : NeZero (n.lcm (torsionOrder K))
this_2 : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Odd n
this : 2 * n = n.lcm (torsionOrder K)
⊢ n ∣ torsionOrder K

Tactic:
exact dvd_torsionOrder_of_isPrimitiveRoot hζ

Premises used: NumberField.Units.dvd_torsionOrder_of_isPrimitiveRoot