awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (goal)
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 : 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)ˣ
⊢ OneHom.toFun (M := L ≃ₐ[K] L) (↑(IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯) : OneHom (L ≃ₐ[K] L) (ZMod n)ˣ)
      ((fun (t : (ZMod n)ˣ) ↦
          (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) ⋯ : L ≃ₐ[K] L))
        x) =
    x
have simp : ((IsPrimitiveRoot.autToPow K (μ := zeta n K L) sorry : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
    (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K sorry) sorry) =
  x
Tactic: simp only [MonoidHom.toFun_eq_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (goal)
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 : 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)ˣ
⊢ ((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
      (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K ⋯) ⋯) =
    x
have generalize_proofs : ∀ (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)))),
  ((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: generalize_proofs _ h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (hypothesis)
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)))
⊢ ((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
have 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 sorry) h)) :
        ZMod n) =
  (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K sorry) h : (a : L) → L)
    (zeta n K L)
Tactic: have key := hζ.autToPow_spec K ((hζ.powerBasis K).equivOfMinpoly ((hμ x).powerBasis K) h)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (hypothesis)
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)
⊢ ((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
have this : (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K sorry) h : (a : L) → L)
    (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) =
  PowerBasis.gen (IsPrimitiveRoot.powerBasis K sorry)
Tactic: have := (hζ.powerBasis K).equivOfMinpoly_gen ((hμ x).powerBasis K) h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (hypothesis)
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 ⋯)
⊢ ((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
have this₁ : (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K sorry) h : (a : L) → L)
    (zeta n K L) =
  PowerBasis.gen (IsPrimitiveRoot.powerBasis K sorry)
Tactic: rw [hζ.powerBasis_gen K] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (hypothesis)
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 ⋯)
⊢ ((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
have 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 sorry) h)) :
        ZMod n) =
  zeta n K L ^ (↑x : ZMod n).val
Tactic: rw [this, IsPrimitiveRoot.powerBasis_gen] at key
Cleared hypotheses: key, this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (hypothesis)
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 ⋯)
⊢ ((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
have 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 sorry) h)) :
        ZMod n) =
  (↑(↑hζ.toRootsOfUnity : Lˣ) : L) ^ (↑x : ZMod n).val
Tactic: nth_rw 1 5 [← hζ.val_toRootsOfUnity_coe] at key
Cleared hypotheses: key, this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (hypothesis)
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 ⋯)
⊢ ((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
have 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 sorry) h)) :
                ZMod n)) :
        Lˣ) :
    L) =
  (↑(↑(hζ.toRootsOfUnity ^ (↑x : ZMod n).val) : Lˣ) : L)
Tactic: simp only [← rootsOfUnity.coe_pow] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (hypothesis)
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)
⊢ ((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
have 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 sorry) h)) :
        ZMod n) =
  hζ.toRootsOfUnity ^ (↑x : ZMod n).val
Tactic: replace key := rootsOfUnity.coe_injective key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (hypothesis)
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
⊢ ((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
have 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 sorry) 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
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (hypothesis)
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 pf) h) =
    x
have 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 sorry) h)) :
    ZMod n) =
  (↑x : ZMod n)
Tactic: simp only [ZMod.natCast_val, ZMod.cast_id', id] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (goal)
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)
⊢ (fromZetaAut hμ h : (a : L) → L) (zeta n K L) = μ
have simp_rw : (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis (n := n) K (ζ := zeta n K L) sorry)
        (IsPrimitiveRoot.powerBasis K (ζ :=
          zeta n K L ^
            (↑(ZMod.unitOfCoprime (Exists.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ) sorry) sorry) : ZMod n).val)
          sorry)
        sorry :
      (a : L) → L)
    (zeta n K L) =
  μ
Tactic: simp_rw [fromZetaAut, autEquivPow_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (goal)
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μ)))
⊢ (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K hμ) pf_1 : (a : L) → L)
      (zeta n K L) =
    μ
have nth_rewrite : (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K hμ) pf_1 : (a : L) → L)
    (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) =
  μ
Tactic: nth_rewrite 4 [← hζ.powerBasis_gen K]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (goal)
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μ)))
⊢ (PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ) (IsPrimitiveRoot.powerBasis K hμ) pf_1 : (a : L) → L)
      (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) =
    μ
have rw : zeta n K L ^ (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val = μ
Tactic: rw [PowerBasis.equivOfMinpoly_gen, hμ.powerBasis_gen K]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Gal (goal)
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 ^ (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val = μ
have h₁ : (↑(ZMod.unitOfCoprime (h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)) pf) : ZMod n).val =
  h.choose (p := fun (i : ℕ) ↦ i < n ∧ zeta n K L ^ i = μ)
Tactic: convert! h.choose_spec.2
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type w
B : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : IsDomain B
inst_6 : NeZero.{z} (R := B) (↑n : B)
⊢ Eq.{z + 1} (α := B) ((aeval (zeta n A B) : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)
have rw : IsPrimitiveRoot (zeta n A B) n
Tactic: rw [← eval_map_algebraMap, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type w
B : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : IsDomain B
inst_6 : NeZero.{z} (R := B) (↑n : B)
⊢ IsRoot (cyclotomic n B) (zeta n A B)
have a : IsRoot (cyclotomic n B) (zeta n A B) ↔
  Eq.{z + 1} (α := B) ((aeval (zeta n A B) : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)
Tactic: convert! aeval_zeta n A B using 0
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type w
B : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension {n} A B
inst_5 : IsDomain B
inst_6 : NeZero.{z} (R := B) (↑n : B)
⊢ IsRoot (cyclotomic n B) (zeta n A B) ↔
    Eq.{z + 1} (α := B) ((aeval (zeta n A B) : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)
have a : eval (zeta n A B) (cyclotomic n B) = 0 ↔
  Eq.{z + 1} (α := B) ((aeval (zeta n A B) : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)
Tactic: rw [IsRoot.def, aeval_def, eval₂_eq_eval_map, map_cyclotomic]