awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Odd n
⊢ torsionOrder K = if Even n then n else 2 * n
have inr : torsionOrder K = 2 * n
Tactic: rw [if_neg (Nat.not_even_iff_odd.mpr 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 : Odd n
⊢ torsionOrder K = 2 * n
have inr : ∀ (this : 2 * 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 ?_
-- 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 : Odd n
inr : ∀ (this : 2 * n = n.lcm (torsionOrder K)), torsionOrder K = 2 * n
⊢ torsionOrder K = 2 * n
have inr₁ : ¬n = n.lcm (torsionOrder K)
Tactic: have := (Nat.eq_or_eq_of_totient_eq_totient (Nat.dvd_lcm_left _ _) h_main).resolve_left ?_
-- 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 : Odd n
this : 2 * n = n.lcm (torsionOrder K)
⊢ torsionOrder K = 2 * n
have inr : n ∣ torsionOrder K
Tactic: rw [this, eq_comm, Nat.lcm_eq_right_iff_dvd]
-- 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 : Odd n
⊢ ¬n = n.lcm (torsionOrder K)
have inr : ¬torsionOrder K ∣ n
Tactic: rw [eq_comm, Nat.lcm_eq_left_iff_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hn : 2 < n
⊢ nrRealPlaces K = 0
have this : NumberField K
Tactic: have := IsCyclotomicExtension.numberField {n} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hn : 2 < n
⊢ IsTotallyComplex K
have this : NumberField K
Tactic: have := IsCyclotomicExtension.numberField {n} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
⊢ nrComplexPlaces K = φ n / 2
have this : NumberField K
Tactic: have := IsCyclotomicExtension.numberField {n} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
⊢ nrComplexPlaces K = φ n / 2
have pos : ∀ (hn : 2 < n), nrComplexPlaces K = φ n / 2
Tactic: by_cases hn : 2 < n
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
pos : ∀ (hn : 2 < n), nrComplexPlaces K = φ n / 2
⊢ nrComplexPlaces K = φ n / 2
have neg : ∀ (hn : ¬2 < n), nrComplexPlaces K = φ n / 2
Tactic: by_cases hn : 2 < n
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
⊢ nrComplexPlaces K = φ n / 2
have pos : ∀ (k : ℕ) (hk : φ n = k + k), nrComplexPlaces K = φ n / 2
Tactic: obtain ⟨k, hk : φ n = k + k⟩ := totient_even hn
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
k : ℕ
hk : φ n = k + k
⊢ nrComplexPlaces K = φ n / 2
have key : nrRealPlaces K + 2 * nrComplexPlaces K = Module.finrank ℚ K
Tactic: have key := card_add_two_mul_card_eq_rank K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : 2 < n
k : ℕ
hk : φ n = k + k
key : nrRealPlaces K + 2 * nrComplexPlaces K = Module.finrank ℚ K
⊢ nrComplexPlaces K = φ n / 2
have key₁ : nrComplexPlaces K = k
Tactic: rw [nrRealPlaces_eq_zero K hn, zero_add, IsCyclotomicExtension.finrank (n := n) K
      (cyclotomic.irreducible_rat (NeZero.pos _)), hk, ← two_mul,
      Nat.mul_right_inj (by simp)] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
⊢ φ n = 1
have pos : ∀ (h1 : 1 < n), φ n = 1
Tactic: by_cases h1 : 1 < n
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
pos : ∀ (h1 : 1 < n), φ n = 1
⊢ φ n = 1
have neg : ∀ (h1 : ¬1 < n), φ n = 1
Tactic: by_cases h1 : 1 < n
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : 1 < n
⊢ φ n = 1
have h₁ : n = 2
Tactic: convert! totient_two
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
h1 : ¬1 < n
⊢ φ n = 1
have h₁ : n = 1
Tactic: convert! totient_one
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this : NumberField K
hn : ¬2 < n
⊢ nrComplexPlaces K = φ n / 2
have this₁ : φ n = 1
Tactic: have : φ n = 1 := by
      by_cases h1 : 1 < n
      · convert! totient_two
        exact (eq_of_le_of_not_lt (succ_le_of_lt h1) hn).symm
      · convert! totient_one
        exact eq_of_le_of_not_lt (not_lt.mp h1) (by simp [NeZero.ne _])
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this_1 : NumberField K
hn : ¬2 < n
this : φ n = 1
⊢ nrComplexPlaces K = φ n / 2
have neg : nrComplexPlaces K = 1 / 2
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this_1 : NumberField K
hn : ¬2 < n
this : φ n = 1
⊢ nrComplexPlaces K = 1 / 2
have neg : Module.finrank ℚ K = 1
Tactic: apply nrComplexPlaces_eq_zero_of_finrank_eq_one
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
this_1 : NumberField K
hn : ¬2 < n
this neg : φ n = 1
⊢ Module.finrank ℚ K = 1
have neg₁ : Eq (α := ℕ) 1 1
Tactic: rw [IsCyclotomicExtension.finrank K (cyclotomic.irreducible_rat (NeZero.pos n)), this]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
x : K
hx : x ^ n = 1
⊢ (σ : (a : K) → K) x =
    x ^ ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
have obtain : ∀ (a : ℕ) (hx : (zeta n ℚ K ^ a) ^ n = 1),
  (σ : (a : K) → K) (zeta n ℚ K ^ a) =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
Tactic: obtain ⟨a, -, rfl⟩ := (zeta_spec n ℚ K).eq_pow_of_pow_eq_one hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
a : ℕ
hx : (zeta n ℚ K ^ a) ^ n = 1
⊢ (σ : (a : K) → K) (zeta n ℚ K ^ a) =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
have rw : HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
  (zeta n ℚ K ^ a) ^
    ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
Tactic: rw [map_pow, pow_right_comm, galEquivZMod, autEquivPow_apply, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, IsPrimitiveRoot.autToPow_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
a : ℕ
hx : (zeta n ℚ K ^ a) ^ n = 1
rw :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
⊢ (σ : (a : K) → K) (zeta n ℚ K ^ a) =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
have rw₁ : HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
  (zeta n ℚ K ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) ^
    a
Tactic: rw [map_pow, pow_right_comm, galEquivZMod, autEquivPow_apply, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, IsPrimitiveRoot.autToPow_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
a : ℕ
hx : (zeta n ℚ K ^ a) ^ n = 1
rw :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
rw₁ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) ^
      a
⊢ (σ : (a : K) → K) (zeta n ℚ K ^ a) =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
have rw₂ : HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
  (zeta n ℚ K ^
      ZMod.val (n := n) (↑(((autEquivPow K sorry : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) ^
    a
Tactic: rw [map_pow, pow_right_comm, galEquivZMod, autEquivPow_apply, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, IsPrimitiveRoot.autToPow_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
a : ℕ
hx : (zeta n ℚ K ^ a) ^ n = 1
rw :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
rw₁ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) ^
      a
rw₂ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n) (↑(((autEquivPow K ⋯ : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) ^
      a
⊢ (σ : (a : K) → K) (zeta n ℚ K ^ a) =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
have rw₃ : HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
  (zeta n ℚ K ^
      ZMod.val (n := n)
        (↑(OneHom.toFun (↑(IsPrimitiveRoot.autToPow ℚ (μ := zeta n ℚ K) sorry) : OneHom Gal(K/ℚ) (ZMod n)ˣ) σ) : ZMod n)) ^
    a
Tactic: rw [map_pow, pow_right_comm, galEquivZMod, autEquivPow_apply, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, IsPrimitiveRoot.autToPow_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
a : ℕ
hx : (zeta n ℚ K ^ a) ^ n = 1
rw :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
rw₁ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) ^
      a
rw₂ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n) (↑(((autEquivPow K ⋯ : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) ^
      a
rw₃ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n)
          (↑(OneHom.toFun (↑(IsPrimitiveRoot.autToPow ℚ (μ := zeta n ℚ K) ⋯) : OneHom Gal(K/ℚ) (ZMod n)ˣ) σ) :
            ZMod n)) ^
      a
⊢ (σ : (a : K) → K) (zeta n ℚ K ^ a) =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
have rw₄ : HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
  (zeta n ℚ K ^
      ZMod.val (n := n)
        (↑((((↑(IsPrimitiveRoot.autToPow ℚ (μ := zeta n ℚ K) sorry) : OneHom Gal(K/ℚ) (ZMod n)ˣ) :
                  OneHom Gal(K/ℚ) (ZMod n)ˣ) :
                (a : Gal(K/ℚ)) → (ZMod n)ˣ)
              σ) :
          ZMod n)) ^
    a
Tactic: rw [map_pow, pow_right_comm, galEquivZMod, autEquivPow_apply, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, IsPrimitiveRoot.autToPow_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
a : ℕ
hx : (zeta n ℚ K ^ a) ^ n = 1
rw :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
rw₁ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) ^
      a
rw₂ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n) (↑(((autEquivPow K ⋯ : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) ^
      a
rw₃ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n)
          (↑(OneHom.toFun (↑(IsPrimitiveRoot.autToPow ℚ (μ := zeta n ℚ K) ⋯) : OneHom Gal(K/ℚ) (ZMod n)ˣ) σ) :
            ZMod n)) ^
      a
rw₄ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n)
          (↑((((↑(IsPrimitiveRoot.autToPow ℚ (μ := zeta n ℚ K) ⋯) : OneHom Gal(K/ℚ) (ZMod n)ˣ) :
                    OneHom Gal(K/ℚ) (ZMod n)ˣ) :
                  (a : Gal(K/ℚ)) → (ZMod n)ˣ)
                σ) :
            ZMod n)) ^
      a
⊢ (σ : (a : K) → K) (zeta n ℚ K ^ a) =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
have rw₅ : HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
  (zeta n ℚ K ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow ℚ (μ := zeta n ℚ K) sorry : Gal(K/ℚ) →* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) :
          ZMod n)) ^
    a
Tactic: rw [map_pow, pow_right_comm, galEquivZMod, autEquivPow_apply, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, IsPrimitiveRoot.autToPow_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
a : ℕ
hx : (zeta n ℚ K ^ a) ^ n = 1
rw :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
rw₁ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) ^
      a
rw₂ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n) (↑(((autEquivPow K ⋯ : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) ^
      a
rw₃ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n)
          (↑(OneHom.toFun (↑(IsPrimitiveRoot.autToPow ℚ (μ := zeta n ℚ K) ⋯) : OneHom Gal(K/ℚ) (ZMod n)ˣ) σ) :
            ZMod n)) ^
      a
rw₄ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n)
          (↑((((↑(IsPrimitiveRoot.autToPow ℚ (μ := zeta n ℚ K) ⋯) : OneHom Gal(K/ℚ) (ZMod n)ˣ) :
                    OneHom Gal(K/ℚ) (ZMod n)ˣ) :
                  (a : Gal(K/ℚ)) → (ZMod n)ˣ)
                σ) :
            ZMod n)) ^
      a
rw₅ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a =
    (zeta n ℚ K ^
        ZMod.val (n := n)
          (↑(((IsPrimitiveRoot.autToPow ℚ (μ := zeta n ℚ K) ⋯ : Gal(K/ℚ) →* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ)
                σ) :
            ZMod n)) ^
      a
⊢ (σ : (a : K) → K) (zeta n ℚ K ^ a) =
    (zeta n ℚ K ^ a) ^
      ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
have rw₆ : HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a = HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a
Tactic: rw [map_pow, pow_right_comm, galEquivZMod, autEquivPow_apply, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, IsPrimitiveRoot.autToPow_spec]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
x : 𝓞 K
hx : x ^ n = 1
⊢ σ • x =
    x ^ ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
have a : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (σ • x) : K)
  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      (x ^
        ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) :
    K)
Tactic: apply FaithfulSMul.algebraMap_injective (𝓞 K) K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
x : 𝓞 K
hx : x ^ n = 1
⊢ (↑x : K) ^ n = 1
have rw : (↑(x ^ n) : K) = 1
Tactic: rw [← Subalgebra.coe_pow, hx, OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
x : 𝓞 K
hx : x ^ n = 1
rw : (↑(x ^ n) : K) = 1
⊢ (↑x : K) ^ n = 1
have rw₁ : Eq.{u_1 + 1} (α := K) (↑1 : K) 1
Tactic: rw [← Subalgebra.coe_pow, hx, OneMemClass.coe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Galois (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
x : 𝓞 K
hx : x ^ n = 1
rw : (↑(x ^ n) : K) = 1
rw₁ : Eq.{u_1 + 1} (α := K) (↑1 : K) 1
⊢ (↑x : K) ^ n = 1
have rw₂ : Eq.{u_1 + 1} (α := K) 1 1
Tactic: rw [← Subalgebra.coe_pow, hx, OneMemClass.coe_one]