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
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 ∣ n
⊢ ¬n = n.lcm (torsionOrder K)

Tactic:
rw [eq_comm, Nat.lcm_eq_left_iff_dvd]

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 : Odd n
⊢ ¬torsionOrder K ∣ n

Tactic:
fun h ↦ Nat.not_even_iff_odd.mpr (Odd.of_dvd_nat hn h) (even_torsionOrder K)

Premises used: Iff.mpr, Nat.not_even_iff_odd, Odd.of_dvd_nat, Not, NumberField.Units.even_torsionOrder
-- 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
⊢ ¬torsionOrder K ∣ n

Tactic:
exact fun h ↦ Nat.not_even_iff_odd.mpr (Odd.of_dvd_nat hn h) (even_torsionOrder K)

Premises used: Iff.mpr, Nat.not_even_iff_odd, Odd.of_dvd_nat, NumberField.Units.even_torsionOrder
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hn : 2 < n
⊢ NumberField K

Tactic:
have := IsCyclotomicExtension.numberField {n} ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hn : 2 < n
this : NumberField K
⊢ nrRealPlaces K = 0

Tactic:
apply (IsCyclotomicExtension.zeta_spec n ℚ K).nrRealPlaces_eq_zero_of_two_lt hn

Premises used: NumberField.InfinitePlace.IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt, Rat, IsCyclotomicExtension.zeta_spec
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hn : 2 < n
this : NumberField K
⊢ IsTotallyComplex K

Tactic:
nrRealPlaces_eq_zero_iff.mp <| nrRealPlaces_eq_zero K hn

Premises used: NumberField.nrRealPlaces_eq_zero_iff, IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hn : 2 < n
this : NumberField K
⊢ IsTotallyComplex K

Tactic:
exact nrRealPlaces_eq_zero_iff.mp <| nrRealPlaces_eq_zero K hn

Premises used: NumberField.nrRealPlaces_eq_zero_iff, IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
Goal:
n : ℕ
inst : NeZero n
K : Type u
inst_1 : Field K
inst_2 : CharZero K
h : IsCyclotomicExtension {n} ℚ K
⊢ NumberField K

Tactic:
have := IsCyclotomicExtension.numberField {n} ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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
neg : ∀ (hn : ¬2 < n), nrComplexPlaces K = φ n / 2
⊢ nrComplexPlaces K = φ n / 2

Tactic:
by_cases hn : 2 < n
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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 : ∀ (k : ℕ) (hk : φ n = k + k), nrComplexPlaces K = φ n / 2
⊢ nrComplexPlaces K = φ n / 2

Tactic:
obtain ⟨k, hk : φ n = k + k⟩ := totient_even hn

Premises used: Nat.totient, Nat.totient_even
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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
⊢ nrRealPlaces K + 2 * nrComplexPlaces K = Module.finrank ℚ K

Tactic:
have key := card_add_two_mul_card_eq_rank K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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 : 2 * nrComplexPlaces K = 2 * k
⊢ Ne (α := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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 = 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

Premises used: two_mul, IsCyclotomicExtension.finrank, zero_add, IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero, Polynomial.cyclotomic.irreducible_rat, NeZero.pos, Nat.mul_right_inj
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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 : nrComplexPlaces K = k
⊢ nrComplexPlaces K = φ n / 2

Tactic:
simp [hk, key, ← two_mul]

Premises used: two_mul
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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
neg : ∀ (h1 : ¬1 < n), φ n = 1
⊢ φ n = 1

Tactic:
by_cases h1 : 1 < n
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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
⊢ φ 2 = 1

Tactic:
totient_two

Premises used: Nat.totient_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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
h₁ : n = 2
⊢ φ n = 1

Tactic:
convert! totient_two

Premises used: Nat.totient_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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 = 2

Tactic:
(eq_of_le_of_not_lt (succ_le_of_lt h1) hn).symm

Premises used: Nat.succ_le_of_lt, Eq.symm, eq_of_le_of_not_lt
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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 = 2

Tactic:
exact (eq_of_le_of_not_lt (succ_le_of_lt h1) hn).symm

Premises used: Nat.succ_le_of_lt, Eq.symm, eq_of_le_of_not_lt
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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
⊢ φ 1 = 1

Tactic:
totient_one

Premises used: Nat.totient_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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
h₁ : n = 1
⊢ φ n = 1

Tactic:
convert! totient_one

Premises used: Nat.totient_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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

Tactic:
simp [NeZero.ne _]

Premises used: NeZero.ne
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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

Tactic:
exact eq_of_le_of_not_lt (not_lt.mp h1) (by simp [NeZero.ne _])

Premises used: not_lt, Iff.mp, eq_of_le_of_not_lt
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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

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 _])
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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
neg : nrComplexPlaces K = 1 / 2
⊢ nrComplexPlaces K = φ n / 2

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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
neg : Module.finrank ℚ K = 1
⊢ nrComplexPlaces K = 1 / 2

Tactic:
apply nrComplexPlaces_eq_zero_of_finrank_eq_one

Premises used: NumberField.InfinitePlace.nrComplexPlaces_eq_zero_of_finrank_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
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
neg₁ neg₂ : Eq (α := ℕ) 1 1
⊢ Module.finrank ℚ K = 1

Tactic:
rw [IsCyclotomicExtension.finrank K (cyclotomic.irreducible_rat (NeZero.pos n)), this]

Premises used: IsCyclotomicExtension.finrank, Polynomial.cyclotomic.irreducible_rat, NeZero.pos
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
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
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)
⊢ (σ : (a : K) → K) x =
    x ^ 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

Premises used: Rat, IsCyclotomicExtension.zeta_spec, IsPrimitiveRoot.eq_pow_of_pow_eq_one, rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
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
rw₆ rw₇ :
  HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) a = HPow.hPow (α := K) ((σ : (a : K) → K) (zeta n ℚ K) : K) 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)

Tactic:
rw [map_pow, pow_right_comm, galEquivZMod, autEquivPow_apply, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, IsPrimitiveRoot.autToPow_spec]

Premises used: pow_right_comm, MonoidHom.toOneHom_coe, IsCyclotomicExtension.Rat.galEquivZMod, map_pow, IsPrimitiveRoot.autToPow_spec, OneHom.toFun_eq_coe, IsCyclotomicExtension.autEquivPow_apply
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
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 :
  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)
⊢ σ • x =
    x ^ ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)

Tactic:
apply FaithfulSMul.algebraMap_injective (𝓞 K) K

Premises used: FaithfulSMul.algebraMap_injective, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := K) 1 1
⊢ (↑x : K) ^ n = 1

Tactic:
rw [← Subalgebra.coe_pow, hx, OneMemClass.coe_one]

Premises used: OneMemClass.coe_one, Subalgebra.coe_pow
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
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
⊢ 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 galEquivZMod_apply_of_pow_eq n K σ <| by rw [← Subalgebra.coe_pow, hx, OneMemClass.coe_one]

Premises used: IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
⊢ IsPrimitiveRoot (zeta m ℚ F) m

Tactic:
have hζ := IsCyclotomicExtension.zeta_spec m ℚ F
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
this :
  ζ ^
      ZMod.val (n := m)
        (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) : ZMod m) =
    ζ ^ ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
⊢ Eq (α := ZMod m)
    (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) : ZMod m)
    (ZMod.cast (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n))

Tactic:
rw [(hζ.isOfFinOrder (NeZero.ne _)).pow_inj_mod, ← hζ.eq_orderOf,
      ← ZMod.natCast_eq_natCast_iff', ZMod.natCast_val, ZMod.natCast_val, ZMod.cast_id] at this

Premises used: IsPrimitiveRoot.eq_orderOf, ZMod.natCast_eq_natCast_iff', ZMod.natCast_val, IsOfFinOrder.pow_inj_mod, ZMod.cast_id, IsPrimitiveRoot.isOfFinOrder, NeZero.ne
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
this :
  Eq (α := ZMod m)
    (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) : ZMod m)
    (ZMod.cast (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n))
rwa rwa₁ rwa₂ rwa₃ :
  Eq (α := ZMod m)
    (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) : ZMod m)
    (↑((ZMod.unitsMap h : (a : (ZMod n)ˣ) → (ZMod m)ˣ)
          (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ)) :
      ZMod m)
⊢ Eq (α := (ZMod m)ˣ)
    (((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F) : (ZMod m)ˣ)
    ((ZMod.unitsMap h : (a : (ZMod n)ˣ) → (ZMod m)ˣ)
        (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) :
      (ZMod m)ˣ)

Tactic:
rwa [Units.ext_iff]

Premises used: Units.ext_iff
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
suffices :
  ζ ^
      ZMod.val (n := m)
        (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) : ZMod m) =
    ζ ^ ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)
⊢ Eq (α := (ZMod m)ˣ)
    (((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F) : (ZMod m)ˣ)
    ((ZMod.unitsMap h : (a : (ZMod n)ˣ) → (ZMod m)ˣ)
        (((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) :
      (ZMod m)ˣ)

Tactic:
suffices ζ ^ (galEquivZMod m F (σ.restrictNormal F)).val.val = ζ ^ (galEquivZMod n K σ).val.val by
    rw [(hζ.isOfFinOrder (NeZero.ne _)).pow_inj_mod, ← hζ.eq_orderOf,
      ← ZMod.natCast_eq_natCast_iff', ZMod.natCast_val, ZMod.natCast_val, ZMod.cast_id] at this
    rwa [Units.ext_iff]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
a :
  Eq.{u_1 + 1} (α := K)
    ((algebraMap F K : (a : F) → K)
        (ζ ^
          ZMod.val (n := m)
            (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) :
              ZMod m)) :
      K)
    ((algebraMap F K : (a : F) → K)
        (ζ ^
          ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) :
      K)
⊢ ζ ^
      ZMod.val (n := m)
        (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) : ZMod m) =
    ζ ^ ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)

Tactic:
apply FaithfulSMul.algebraMap_injective F K

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
a : HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) ζ : K) n = 1
⊢ Eq.{u_1 + 1} (α := K)
    ((algebraMap F K : (a : F) → K)
        (ζ ^
          ZMod.val (n := m)
            (↑(((galEquivZMod m F : Gal(F/ℚ) ≃* (ZMod m)ˣ) : (a : Gal(F/ℚ)) → (ZMod m)ˣ) (σ.restrictNormal F)) :
              ZMod m)) :
      K)
    ((algebraMap F K : (a : F) → K)
        (ζ ^
          ZMod.val (n := n) (↑(((galEquivZMod n K : Gal(K/ℚ) ≃* (ZMod n)ˣ) : (a : Gal(K/ℚ)) → (ZMod n)ˣ) σ) : ZMod n)) :
      K)

Tactic:
rw [map_pow, map_pow, ← galEquivZMod_apply_of_pow_eq, ← AlgEquiv.restrictNormal_commutes,
      galEquivZMod_apply_of_pow_eq m _ _ hζ.pow_eq_one, map_pow]

Premises used: map_pow, IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq, AlgEquiv.restrictNormal_commutes, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
inst_2 : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst_3 : NeZero m
F : Type u_2
inst_4 : Field F
inst_5 : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst_6 : Algebra F K
inst_7 : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
a : Eq.{u_1 + 1} (α := K) ((algebraMap F K : (a : F) → K) (ζ ^ n) : K) (1 : K)
a₁ : Eq.{u_1 + 1} (α := K) ((algebraMap F K : (a : F) → K) 1 : K) (1 : K)
a₂ a₃ : Eq.{u_1 + 1} (α := K) 1 1
⊢ HPow.hPow (α := K) ((algebraMap F K : (a : F) → K) ζ : K) n = 1

Tactic:
rw [← map_pow, (hζ.pow_eq_one_iff_dvd _).mpr h, map_one]

Premises used: Iff.mpr, map_pow, map_one, IsPrimitiveRoot.pow_eq_one_iff_dvd