awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
h : HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) (φ (HPow.hPow (β := ℕ) p 1) / 2)
⊢ HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) (φ (p ^ HAdd.hAdd (α := ℕ) 0 1) / 2)
have h₁ : HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) (φ p / 2)
Tactic: rw [zero_add, pow_one, totient_prime hp.out]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
h : HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) (φ (HPow.hPow (β := ℕ) p 1) / 2)
h₁ : HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) (φ p / 2)
⊢ HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) (φ (p ^ HAdd.hAdd (α := ℕ) 0 1) / 2)
have h₂ : HPow.hPow (α := K) (-1) ((p - 1) / 2) = HPow.hPow (α := K) (-1) ((p - 1) / 2)
Tactic: rw [zero_add, pow_one, totient_prime hp.out]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ HPow.hPow (α := K) (↑p : K) (p - 2) =
    HPow.hPow (α := K) (↑p : K) (HPow.hPow (β := ℕ) p 0 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1))
have h : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) (1 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1))
Tactic: rw [_root_.pow_zero, one_mul, zero_add, mul_one, Nat.sub_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
h : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) (1 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1))
⊢ HPow.hPow (α := K) (↑p : K) (p - 2) =
    HPow.hPow (α := K) (↑p : K) (HPow.hPow (β := ℕ) p 0 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1))
have h₁ : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1)
Tactic: rw [_root_.pow_zero, one_mul, zero_add, mul_one, Nat.sub_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
h : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) (1 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1))
h₁ : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1)
h₂ : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) ((p - 1) * 1 - 1)
⊢ HPow.hPow (α := K) (↑p : K) (p - 2) =
    HPow.hPow (α := K) (↑p : K) (HPow.hPow (β := ℕ) p 0 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1))
have h₃ : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) (p - 1 - 1)
Tactic: rw [_root_.pow_zero, one_mul, zero_add, mul_one, Nat.sub_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Discriminant (goal)
Goal:
p : ℕ
K : Type u
L : Type v
ζ : L
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
hζ' : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
h : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) (1 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1))
h₁ : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1)
h₂ : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) ((p - 1) * 1 - 1)
h₃ : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) (p - 1 - 1)
⊢ HPow.hPow (α := K) (↑p : K) (p - 2) =
    HPow.hPow (α := K) (↑p : K) (HPow.hPow (β := ℕ) p 0 * ((p - 1) * HAdd.hAdd (α := ℕ) 0 1 - 1))
have h₄ : HPow.hPow (α := K) (↑p : K) (p - 2) = HPow.hPow (α := K) (↑p : K) (p - HAdd.hAdd (α := ℕ) 1 1)
Tactic: rw [_root_.pow_zero, one_mul, zero_add, mul_one, Nat.sub_sub]
-- 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
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
⊢ (↑f : L →ₐ[K] L) = (↑g : L →ₐ[K] L)
have h : Eq (α := L) (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
  (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
Tactic: apply (hμ.powerBasis K).algHom_ext
-- 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
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
⊢ Eq (α := L) (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
have h : Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
  (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
Tactic: rw [AlgEquiv.coe_algHom, AlgEquiv.coe_algHom, powerBasis_gen,
      ← autToPow_spec K hμ g, ← autToPow_spec K hμ f, hfg]
-- 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
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
h :
  Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
⊢ Eq (α := L) (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
have h₁ : Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
  ((g : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
Tactic: rw [AlgEquiv.coe_algHom, AlgEquiv.coe_algHom, powerBasis_gen,
      ← autToPow_spec K hμ g, ← autToPow_spec K hμ f, hfg]
-- 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
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
h :
  Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
h₁ :
  Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    ((g : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
⊢ Eq (α := L) (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
have h₂ : Eq (α := L) ((f : (a : L) → L) μ : L) ((g : (a : L) → L) μ : L)
Tactic: rw [AlgEquiv.coe_algHom, AlgEquiv.coe_algHom, powerBasis_gen,
      ← autToPow_spec K hμ g, ← autToPow_spec K hμ f, hfg]
-- 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
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
h :
  Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
h₁ :
  Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    ((g : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
h₂ : Eq (α := L) ((f : (a : L) → L) μ : L) ((g : (a : L) → L) μ : L)
⊢ Eq (α := L) (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
have h₃ : (f : (a : L) → L) μ =
  μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g) : ZMod n)
Tactic: rw [AlgEquiv.coe_algHom, AlgEquiv.coe_algHom, powerBasis_gen,
      ← autToPow_spec K hμ g, ← autToPow_spec K hμ f, hfg]
-- 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
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
h :
  Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
h₁ :
  Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    ((g : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
h₂ : Eq (α := L) ((f : (a : L) → L) μ : L) ((g : (a : L) → L) μ : L)
h₃ :
  (f : (a : L) → L) μ =
    μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g) : ZMod n)
⊢ Eq (α := L) (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
have h₄ : μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f) : ZMod n) =
  μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g) : ZMod n)
Tactic: rw [AlgEquiv.coe_algHom, AlgEquiv.coe_algHom, powerBasis_gen,
      ← autToPow_spec K hμ g, ← autToPow_spec K hμ f, hfg]
-- 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
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
h :
  Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
h₁ :
  Eq (α := L) ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    ((g : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
h₂ : Eq (α := L) ((f : (a : L) → L) μ : L) ((g : (a : L) → L) μ : L)
h₃ :
  (f : (a : L) → L) μ =
    μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g) : ZMod n)
h₄ :
  μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f) : ZMod n) =
    μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g) : ZMod n)
⊢ Eq (α := L) (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
    (((↑g : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hμ)) : L)
have h₅ : μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g) : ZMod n) =
  μ ^ ZMod.val (n := n) (↑(((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g) : ZMod n)
Tactic: rw [AlgEquiv.coe_algHom, AlgEquiv.coe_algHom, powerBasis_gen,
      ← autToPow_spec K hμ g, ← autToPow_spec K hμ f, hfg]
-- 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μ : IsPrimitiveRoot μ n
inst_4 : Algebra K L
inst_5 : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
hfg :
  Eq (α := (ZMod n)ˣ) (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) f : (ZMod n)ˣ)
    (((autToPow K hμ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ) g : (ZMod n)ˣ)
⊢ f = g
have this : (↑f : L →ₐ[K] L) = (↑g : L →ₐ[K] L)
Tactic: have : f.toAlgHom = g.toAlgHom := by
    apply (hμ.powerBasis K).algHom_ext
    rw [AlgEquiv.coe_algHom, AlgEquiv.coe_algHom, powerBasis_gen,
      ← autToPow_spec K hμ g, ← autToPow_spec K hμ f, hfg]
-- 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 : 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 := ⋯
t : (ZMod n)ˣ
⊢ Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)))
have this : NeZero.{u_1} (R := K) (↑n : K)
Tactic: haveI := IsCyclotomicExtension.neZero' n K L
-- 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 := ⋯
t : (ZMod n)ˣ
this : NeZero.{u_1} (R := K) (↑n : K)
⊢ Eq (α := K[X]) (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)))
    (minpoly K (PowerBasis.gen (IsPrimitiveRoot.powerBasis K ⋯)))
have simp : Eq (α := K[X]) (minpoly K (zeta n K L)) (minpoly K (zeta n K L ^ (↑t : ZMod n).val))
Tactic: simp only [IsPrimitiveRoot.powerBasis_gen]
-- 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 : 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 := ⋯
t : (ZMod n)ˣ
this : NeZero.{u_1} (R := K) (↑n : K)
⊢ Eq (α := K[X]) (minpoly K (zeta n K L)) (minpoly K (zeta n K L ^ (↑t : ZMod n).val))
have hr : Eq (α := K[X]) (cyclotomic n K) (minpoly K (zeta n K L ^ (↑t : ZMod n).val))
Tactic: have hr :=
            IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible
              ((zeta_spec n K L).pow_of_coprime _ (ZMod.val_coe_unit_coprime t)) h
-- 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 := ⋯
f : L ≃ₐ[K] L
⊢ PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
      (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
        zeta n K L ^
          ZMod.val (n := n)
            (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                    (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                  f) :
              ZMod n))
        ⋯)
      ⋯ =
    f
have a : (↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
        (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
          zeta n K L ^
            ZMod.val (n := n)
              (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) sorry : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                      (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                    f) :
                ZMod n))
          sorry)
        sorry) :
    L →ₐ[K] L) =
  (↑f : L →ₐ[K] L)
Tactic: apply AlgEquiv.coe_algHom_injective
-- 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 := ⋯
f : L ≃ₐ[K] L
⊢ (↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
            zeta n K L ^
              ZMod.val (n := n)
                (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                        (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                      f) :
                  ZMod n))
            ⋯)
          ⋯) :
      L →ₐ[K] L) =
    (↑f : L →ₐ[K] L)
have a : Eq (α := L)
  (((↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
              (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
                zeta n K L ^
                  ZMod.val (n := n)
                    (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) sorry : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                            (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                          f) :
                      ZMod n))
                sorry)
              sorry) :
          L →ₐ[K] L) :
        (a : L) → L)
      (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) :
    L)
  (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) : L)
Tactic: apply (hζ.powerBasis K).algHom_ext
-- 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 := ⋯
f : L ≃ₐ[K] L
⊢ Eq (α := L)
    (((↑(PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
                (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
                  zeta n K L ^
                    ZMod.val (n := n)
                      (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                              (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                            f) :
                        ZMod n))
                  ⋯)
                ⋯) :
            L →ₐ[K] L) :
          (a : L) → L)
        (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) :
      L)
    (((↑f : L →ₐ[K] L) : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) : L)
have a : Eq (α := L)
  ((PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
          (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
            zeta n K L ^
              ZMod.val (n := n)
                (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) sorry : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                        (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                      f) :
                  ZMod n))
            sorry)
          sorry :
        (a : L) → L)
      (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) :
    L)
  ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) : L)
Tactic: simp only [AlgEquiv.coe_algHom]
-- 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 := ⋯
f : L ≃ₐ[K] L
⊢ Eq (α := L)
    ((PowerBasis.equivOfMinpoly (IsPrimitiveRoot.powerBasis K hζ)
            (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
              zeta n K L ^
                ZMod.val (n := n)
                  (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) ⋯ : (L ≃ₐ[K] L) →* (ZMod n)ˣ) :
                          (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                        f) :
                    ZMod n))
              ⋯)
            ⋯ :
          (a : L) → L)
        (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) :
      L)
    ((f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ)) : L)
have a : PowerBasis.gen
    (IsPrimitiveRoot.powerBasis (n := n) K (ζ :=
      zeta n K L ^
        ZMod.val (n := n)
          (↑(((IsPrimitiveRoot.autToPow K (μ := zeta n K L) sorry : (L ≃ₐ[K] L) →* (ZMod n)ˣ) : (a : L ≃ₐ[K] L) → (ZMod n)ˣ)
                f) :
            ZMod n))
      sorry) =
  (f : (a : L) → L) (PowerBasis.gen (IsPrimitiveRoot.powerBasis K hζ))
Tactic: rw [PowerBasis.equivOfMinpoly_gen]