awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
refine_1 :
  ∀ {x : CyclotomicField n ℚ} (h : IsIntegral ℤ x),
    Membership.mem (γ := Subalgebra ℤ (CyclotomicField n ℚ)) (adjoin ℤ {b : CyclotomicField n ℚ | b ^ n = 1}) x
⊢ IsIntegralClosure (CyclotomicRing n ℤ ℚ) ℤ (CyclotomicField n ℚ)
have refine_2 : ∀ {x : CyclotomicField n ℚ},
  (∃ (y : CyclotomicRing n ℤ ℚ),
      (algebraMap (CyclotomicRing n ℤ ℚ) (CyclotomicField n ℚ) : (a : CyclotomicRing n ℤ ℚ) → CyclotomicField n ℚ) y =
        x) →
    IsIntegral ℤ x
Tactic: refine ⟨IsFractionRing.injective _ _, fun {x} => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
x : CyclotomicField n ℚ
h : IsIntegral ℤ x
⊢ Membership.mem (γ := Subalgebra ℤ (CyclotomicField n ℚ)) (adjoin ℤ {b : CyclotomicField n ℚ | b ^ n = 1}) x
have refine_1 : ∀ (y : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)])
  (h :
    IsIntegral ℤ (A := CyclotomicField n ℚ)
      ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
            (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
          y :
        CyclotomicField n ℚ)),
  Membership.mem (α := CyclotomicField n ℚ) (γ := Subalgebra ℤ (CyclotomicField n ℚ))
    (adjoin ℤ {b : CyclotomicField n ℚ | b ^ n = 1})
    ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
          (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
        y :
      CyclotomicField n ℚ)
Tactic: obtain ⟨y, rfl⟩ := (isIntegralClosure_adjoin_singleton hζ).isIntegral_iff.1 h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
y : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField n ℚ)
    ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
          (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
        y :
      CyclotomicField n ℚ)
⊢ Membership.mem (α := CyclotomicField n ℚ) (γ := Subalgebra ℤ (CyclotomicField n ℚ))
    (adjoin ℤ {b : CyclotomicField n ℚ | b ^ n = 1})
    ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
          (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
        y :
      CyclotomicField n ℚ)
have refine_1 : Subset (α := Set (CyclotomicField n ℚ)) {zeta n ℚ (CyclotomicField n ℚ)} {b : CyclotomicField n ℚ | b ^ n = 1}
Tactic: refine adjoin_mono ?_ y.2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
y : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField n ℚ)
    ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
          (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
        y :
      CyclotomicField n ℚ)
⊢ Subset (α := Set (CyclotomicField n ℚ)) {zeta n ℚ (CyclotomicField n ℚ)} {b : CyclotomicField n ℚ | b ^ n = 1}
have refine_1 : HPow.hPow (α := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n = 1
Tactic: simp only [Set.singleton_subset_iff, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : NeZero n
inst_2 : CharZero K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.integralPowerBasis.gen = (↑hζ.toInteger : K)
have rw : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
    ((hζ.adjoinEquivRingOfIntegers : (a : ↥ℤ[ζ]) → 𝓞 K)
        (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x) ζ sorry) :
      𝓞 K) =
  (↑hζ.toInteger : K)
Tactic: rw [integralPowerBasis, PowerBasis.map_gen, adjoin.powerBasis'_gen]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : NeZero n
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯] ⊤
have refine : Membership.mem (γ := Subalgebra ℤ (𝓞 K))
  ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) sorry]
  hζ.integralPowerBasis.gen
Tactic: refine hζ.integralPowerBasis.adjoin_eq_top_of_gen_mem_adjoin ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : NeZero n
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ Membership.mem (γ := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯]
    hζ.integralPowerBasis.gen
have h : hζ.integralPowerBasis.gen =
  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) sorry + 1
Tactic: convert! Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ n ∣ torsionOrder K
have rw : n ∣ Nat.card.{u} ↥(torsion K)
Tactic: rw [torsionOrder, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ n ∣ Nat.card.{u} ↥(torsion K)
have hζ₁ : IsPrimitiveRoot (IsUnit.unit (a := hζ.toInteger) sorry) n
Tactic: replace hζ := (hζ.toInteger_isPrimitiveRoot).isUnit_unit (NeZero.ne n)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 ∣ Nat.card.{u} ↥(torsion K)
have h : n =
  orderOf (G := ↥(torsion K))
    (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (↑sorry.unit : (𝓞 K)ˣ) sorry)
Tactic: convert! orderOf_dvd_natCard (⟨(hζ.isUnit (NeZero.ne n)).unit, ?_⟩ : torsion K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
h :
  n =
    orderOf (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (↑⋯.unit : (𝓞 K)ˣ) ⋯)
⊢ n ∣ Nat.card.{u} ↥(torsion K)
have convert! : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) (↑sorry.unit : (𝓞 K)ˣ)
Tactic: convert! orderOf_dvd_natCard (⟨(hζ.isUnit (NeZero.ne n)).unit, ?_⟩ : torsion K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (↑⋯.unit : (𝓞 K)ˣ) ⋯)
have h : n = orderOf (↑sorry.unit : (𝓞 K)ˣ)
Tactic: rw [Subgroup.orderOf_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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)ˣ)
have refine : Function.IsPeriodicPt (fun (x : (𝓞 K)ˣ) ↦ (↑sorry.unit : (𝓞 K)ˣ) * x) n 1
Tactic: refine (CommGroup.mem_torsion _ _).mpr ⟨n, NeZero.pos n, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ Function.IsPeriodicPt (fun (x : (𝓞 K)ˣ) ↦ (↑⋯.unit : (𝓞 K)ˣ) * x) n 1
have rw : (↑sorry.unit : (𝓞 K)ˣ) ^ n = 1
Tactic: rw [isPeriodicPt_mul_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
⊢ torsionOrder K = if Even n then n else 2 * n
have hζ : IsPrimitiveRoot (zeta n ℚ K) n
Tactic: have hζ := hK.zeta_spec
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 μ = torsionOrder K
have rw : ∃ (μ : ↥(torsion K)), orderOf μ = Nat.card.{u} ↥(torsion K)
Tactic: rw [torsionOrder, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ torsionOrder K = if Even n then n else 2 * n
have obtain : ∀ (μ : ↥(torsion K)) (hμ : orderOf μ = torsionOrder K), 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ torsionOrder K = if Even n then n else 2 * n
have hμ₁ : IsPrimitiveRoot (↑(↑μ : (𝓞 K)ˣ) : 𝓞 K) (torsionOrder K)
Tactic: rw [← IsPrimitiveRoot.iff_orderOf, ← IsPrimitiveRoot.coe_submonoidClass_iff,
    ← IsPrimitiveRoot.coe_units_iff] at hμ
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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)
⊢ torsionOrder K = if Even n then n else 2 * n
have hμ₁ : 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)
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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)
⊢ torsionOrder K = if Even n then n else 2 * n
have 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))
Tactic: have h := hζ.pow_mul_pow_lcm hμ (NeZero.ne _) (torsionOrder_ne_zero K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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))
⊢ torsionOrder K = if Even n then n else 2 * n
have this : 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⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
have this₁ : IsCyclotomicExtension ({n} ∪ {n.lcm (torsionOrder K)}) ℚ K
Tactic: have := hK.union_of_isPrimitiveRoot _ _ _ h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
have h₁ : ∀ (this : IsCyclotomicExtension ({n.lcm (torsionOrder K)} ∪ {n}) ℚ K),
  ∃ (s : ℕ), Membership.mem (γ := Set ℕ) {n.lcm (torsionOrder K)} s ∧ s ≠ 0 ∧ n ∣ s
Tactic: rwa [Set.union_comm, ← IsCyclotomicExtension.iff_union_of_dvd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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))
⊢ torsionOrder K = if Even n then n else 2 * n
have this₁ : 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 _ _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ torsionOrder K = if Even n then n else 2 * n
have h_main : φ n = φ (n.lcm (torsionOrder K))
Tactic: have h_main := (IsCyclotomicExtension.Rat.finrank n K).symm.trans <|
    (IsCyclotomicExtension.Rat.finrank (n.lcm (torsionOrder K)) K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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))
⊢ torsionOrder K = if Even n then n else 2 * n
have inl : ∀ (hn : Even n), torsionOrder K = if Even n then n else 2 * n
Tactic: obtain hn | hn := Nat.even_or_odd n
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ torsionOrder K = if Even n then n else 2 * n
have inr : ∀ (hn : Odd n), torsionOrder K = if Even n then n else 2 * n
Tactic: obtain hn | hn := Nat.even_or_odd n
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ torsionOrder K = if Even n then n else 2 * n
have inl : torsionOrder K = n
Tactic: rw [if_pos hn]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ torsionOrder K = n
have inl : torsionOrder K ∣ n
Tactic: apply dvd_antisymm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 = n
have inl₁ : n ∣ torsionOrder K
Tactic: apply dvd_antisymm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ torsionOrder K ∣ n
have this₁ : n = n.lcm (torsionOrder K)
Tactic: have := hn.eq_of_totient_eq_totient (Nat.dvd_lcm_left _ _) h_main
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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)
⊢ torsionOrder K ∣ n
have inl : ∀ (this : n.lcm (torsionOrder K) = n), torsionOrder K ∣ n
Tactic: rwa [eq_comm, Nat.lcm_eq_left_iff_dvd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ torsionOrder K ∣ n
have inl₁ : ∀ (this : torsionOrder K ∣ n), torsionOrder K ∣ n
Tactic: rwa [eq_comm, Nat.lcm_eq_left_iff_dvd] at this
Cleared hypotheses: this