awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
key :
  zeta n K L ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L)
⊢ (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)

Tactic:
have := (hζ.powerBasis K).equivOfMinpoly_gen ((hμ x).powerBasis K) h
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
key :
  zeta n K L ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L)
this :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)
⊢ (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)

Tactic:
rw [hζ.powerBasis_gen K] at this

Premises used: IsPrimitiveRoot.powerBasis_gen
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
key :
  zeta n K L ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L)
this :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)
⊢ zeta n K L ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    zeta n K L ^ (↑x : ZMod n).val

Tactic:
rw [this, IsPrimitiveRoot.powerBasis_gen] at key

Premises used: IsPrimitiveRoot.powerBasis_gen
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
key :
  zeta n K L ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L)
this :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)
key₁ :
  zeta n K L ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    zeta n K L ^ (↑x : ZMod n).val
⊢ (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)

Tactic:
rw [this, IsPrimitiveRoot.powerBasis_gen] at key

Premises used: IsPrimitiveRoot.powerBasis_gen
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
key :
  zeta n K L ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    zeta n K L ^ (↑x : ZMod n).val
this :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)
⊢ (↑(↑hζ.toRootsOfUnity : Lˣ) : L) ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    (↑(↑hζ.toRootsOfUnity : Lˣ) : L) ^ (↑x : ZMod n).val

Tactic:
nth_rw 1 5 [← hζ.val_toRootsOfUnity_coe] at key

Premises used: IsPrimitiveRoot.val_toRootsOfUnity_coe
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
key :
  zeta n K L ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    zeta n K L ^ (↑x : ZMod n).val
this :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)
key₁ :
  (↑(↑hζ.toRootsOfUnity : Lˣ) : L) ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    (↑(↑hζ.toRootsOfUnity : Lˣ) : L) ^ (↑x : ZMod n).val
⊢ (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)

Tactic:
nth_rw 1 5 [← hζ.val_toRootsOfUnity_coe] at key

Premises used: IsPrimitiveRoot.val_toRootsOfUnity_coe
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
key :
  (↑(↑hζ.toRootsOfUnity : Lˣ) : L) ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    (↑(↑hζ.toRootsOfUnity : Lˣ) : L) ^ (↑x : ZMod n).val
this :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)
⊢ (↑(↑(hζ.toRootsOfUnity ^
              ZMod.val (n := n)
                (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯)
                        h)) :
                  ZMod n)) :
          Lˣ) :
      L) =
    (↑(↑(hζ.toRootsOfUnity ^ (↑x : ZMod n).val) : Lˣ) : L)

Tactic:
simp only [← rootsOfUnity.coe_pow] at key

Premises used: rootsOfUnity.coe_pow
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
this :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)
key :
  (↑(↑(hζ.toRootsOfUnity ^
              ZMod.val (n := n)
                (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯)
                        h)) :
                  ZMod n)) :
          Lˣ) :
      L) =
    (↑(↑(hζ.toRootsOfUnity ^ (↑x : ZMod n).val) : Lˣ) : L)
⊢ hζ.toRootsOfUnity ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    hζ.toRootsOfUnity ^ (↑x : ZMod n).val

Tactic:
replace key := rootsOfUnity.coe_injective key
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
this :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)
key :
  hζ.toRootsOfUnity ^
      ZMod.val (n := n)
        (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
              (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
          ZMod n) =
    hζ.toRootsOfUnity ^ (↑x : ZMod n).val
⊢ Eq (α := ZMod n)
    (↑(ZMod.val (n := n)
          (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
            ZMod n)) :
      ZMod n)
    (↑(↑x : ZMod n).val : ZMod n)

Tactic:
rw [pow_eq_pow_iff_modEq, ← Subgroup.orderOf_coe, ← orderOf_units, hζ.val_toRootsOfUnity_coe,
        ← (zeta_spec n K L).eq_orderOf, ← ZMod.natCast_eq_natCast_iff] at key

Premises used: IsPrimitiveRoot.eq_orderOf, IsPrimitiveRoot.val_toRootsOfUnity_coe, orderOf_units, pow_eq_pow_iff_modEq, IsCyclotomicExtension.zeta_spec, ZMod.natCast_eq_natCast_iff, Subgroup.orderOf_coe
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
this :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)
key :
  Eq (α := ZMod n)
    (↑(ZMod.val (n := n)
          (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
            ZMod n)) :
      ZMod n)
    (↑(↑x : ZMod n).val : ZMod n)
⊢ (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
          (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
      ZMod n) =
    (↑x : ZMod n)

Tactic:
simp only [ZMod.natCast_val, ZMod.cast_id', id] at key

Premises used: id, ZMod.natCast_val, ZMod.cast_id'
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
this :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)
key :
  (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
          (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
      ZMod n) =
    (↑x : ZMod n)
⊢ ((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K pf) h) =
    x

Tactic:
Units.ext key

Premises used: Units.ext
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := ⋯
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t : ZMod n).val) n := ⋯
x : (ZMod n)ˣ
pf : IsPrimitiveRoot (zeta n K L ^ (↑x : ZMod n).val) n
h :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K pf)))
this :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h : (a : L) → L)
      (zeta n K L) =
    PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)
key :
  (↑(((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
          (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) h)) :
      ZMod n) =
    (↑x : ZMod n)
⊢ ((IsPrimitiveRoot.autToPow K hζ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K pf) h) =
    x

Tactic:
exact Units.ext key

Premises used: Units.ext
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h : Irreducible (M := K[X]) (cyclotomic n K)
simp_rw :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis (n := n) K (ζ := zeta n K L) ⋯)
          (IsPrimitiveRoot.powerBasis K (ζ :=
            zeta n K L ^
              (↑(ZMod.unitOfCoprime (Exists.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ) ⋯) ⋯) : ZMod n).val)
            ⋯)
          ⋯ :
        (a : L) → L)
      (zeta n K L) =
    μ
⊢ (fromZetaAut hμ h : (a : L) → L) (zeta n K L) = μ

Tactic:
simp_rw [fromZetaAut, autEquivPow_symm_apply]

Premises used: IsCyclotomicExtension.fromZetaAut, IsCyclotomicExtension.autEquivPow_symm_apply
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n
h : ∃ i < n, zeta n K L ^ i = μ
pf : h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ).Coprime n
hμ :
  IsPrimitiveRoot
    (zeta n K L ^ (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val) n
pf_1 :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)))
nth_rewrite :
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K hμ) pf_1 : (a : L) → L)
      (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) =
    μ
⊢ (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K hμ) pf_1 : (a : L) → L)
      (zeta n K L) =
    μ

Tactic:
nth_rewrite 4 [← hζ.powerBasis_gen K]

Premises used: IsPrimitiveRoot.powerBasis_gen
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n
h : ∃ i < n, zeta n K L ^ i = μ
pf : h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ).Coprime n
hμ :
  IsPrimitiveRoot
    (zeta n K L ^ (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val) n
pf_1 :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)))
rw : zeta n K L ^ (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val = μ
⊢ (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K hμ) pf_1 : (a : L) → L)
      (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) =
    μ

Tactic:
rw [PowerBasis.equivOfMinpoly_gen, hμ.powerBasis_gen K]

Premises used: IsPrimitiveRoot.powerBasis_gen, PowerBasis.equivOfMinpoly_gen
-- Module: Mathlib.NumberTheory.Cyclotomic.Gal
Goal:
n : ℕ
inst : NeZero n
K : Type u_1
inst_1 : Field K
L : Type u_2
μ : L
inst_2 : CommRing L
inst_3 : IsDomain L
hμ_1 : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
h_1 : Irreducible (M := K[X]) (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n
h : ∃ i < n, zeta n K L ^ i = μ
pf : h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ).Coprime n
hμ :
  IsPrimitiveRoot
    (zeta n K L ^ (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val) n
pf_1 :
  Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)))
⊢ zeta n K L ^ h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ) = μ

Tactic:
h.choose_spec.2

Premises used: Exists.choose_spec, And.right