awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : ζ = 1
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
pos : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) 1 : K) (1 : K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
have pos₁ : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap K L : (a : K) → L) 1 : L) : K) (1 : K)
Tactic: rw [hζ, show 1 = algebraMap K L 1 by simp, Algebra.norm_algebraMap, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : ζ = 1
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
pos : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) 1 : K) (1 : K)
pos₁ : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap K L : (a : K) → L) 1 : L) : K) (1 : K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
have pos₂ : HPow.hPow (α := K) 1 (Module.finrank K L) = 1
Tactic: rw [hζ, show 1 = algebraMap K L 1 by simp, Algebra.norm_algebraMap, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : ζ = 1
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : n = 1
pos : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) 1 : K) (1 : K)
pos₁ : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ((algebraMap K L : (a : K) → L) 1 : L) : K) (1 : K)
pos₂ : HPow.hPow (α := K) 1 (Module.finrank K L) = 1
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
have pos₃ : Eq.{u + 1} (α := K) 1 1
Tactic: rw [hζ, show 1 = algebraMap K L 1 by simp, Algebra.norm_algebraMap, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : ¬n = 1
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
have h1₁ : 2 ≤ n
Tactic: replace h1 : 2 ≤ n := (two_le_iff n).mpr ⟨NeZero.ne _, h1⟩
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
h1 : 2 ≤ n
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
have neg : HPow.hPow (α := K) (-1) (φ n) = 1
Tactic: rw [← hζ.powerBasis_gen K, PowerBasis.norm_gen_eq_coeff_zero_minpoly, hζ.powerBasis_gen K,
      ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, cyclotomic_coeff_zero K h1, mul_one,
      hζ.powerBasis_dim K, ← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, natDegree_cyclotomic]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
L : Type v
inst : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ n
K : Type u_1
inst_1 : Field K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
inst_4 : Algebra K L
hodd : Odd n
⊢ Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
have hz : Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ ^ n) : K) ((Algebra.norm K : (a : L) → K) 1 : K)
Tactic: have hz := congr_arg (norm K) ((IsPrimitiveRoot.iff_def _ n).1 hζ).1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
L : Type v
inst : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ n
K : Type u_1
inst_1 : Field K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
inst_4 : Algebra K L
hodd : Odd n
hz : Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ ^ n) : K) ((Algebra.norm K : (a : L) → K) 1 : K)
⊢ Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
have hz₁ : HPow.hPow (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) n = HPow.hPow (α := K) 1 n
Tactic: rw [← (algebraMap K L).map_one, Algebra.norm_algebraMap, one_pow, map_pow, ← one_pow n] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (if n = 2 then -1 else 1 : K)
have pos : ∀ (hn : n = 2), Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (-1 : K)
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
pos : ∀ (hn : n = 2), Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (-1 : K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (if n = 2 then -1 else 1 : K)
have neg : ∀ (hn : ¬n = 2), Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (1 : K)
Tactic: split_ifs with hn
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : CommRing L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsDomain L
inst_5 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
hn : n = 2
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (-1 : K)
have inst : NeZero (R := ℕ) 2
Tactic: subst hn
Cleared hypotheses: n, inst, hζ, inst_5, hirr, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst_1 : NeZero n
K : Type u
L : Type v
inst_2 : CommRing L
ζ : L
inst_3 : Field K
inst_4 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_5 : IsDomain L
inst_6 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
hn : n = 2
inst : NeZero (R := ℕ) 2
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (-1 : K)
have hζ₁ : IsPrimitiveRoot ζ 2
Tactic: subst hn
Cleared hypotheses: n, inst_1, hζ, inst_6, hirr, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst_1 : NeZero n
K : Type u
L : Type v
inst_2 : CommRing L
ζ : L
inst_3 : Field K
inst_4 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_5 : IsDomain L
inst_6 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
hn : n = 2
inst : NeZero (R := ℕ) 2
hζ₁ : IsPrimitiveRoot ζ 2
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (-1 : K)
have inst₁ : IsCyclotomicExtension {2} K L
Tactic: subst hn
Cleared hypotheses: n, inst_1, hζ, inst_6, hirr, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst_1 : NeZero n
K : Type u
L : Type v
inst_2 : CommRing L
ζ : L
inst_3 : Field K
inst_4 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_5 : IsDomain L
inst_6 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
hn : n = 2
inst : NeZero (R := ℕ) 2
hζ₁ : IsPrimitiveRoot ζ 2
inst₁ : IsCyclotomicExtension {2} K L
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (-1 : K)
have hirr₁ : Irreducible (M := K[X]) (cyclotomic 2 K)
Tactic: subst hn
Cleared hypotheses: n, inst_1, hζ, inst_6, hirr, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
K : Type u
L : Type v
inst : CommRing L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
inst_3 : IsDomain L
inst_4 : NeZero (R := ℕ) 2
hζ : IsPrimitiveRoot ζ 2
inst_5 : IsCyclotomicExtension {2} K L
hirr : Irreducible (M := K[X]) (cyclotomic 2 K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) ζ : K) (-1 : K)
have pos : HPow.hPow (α := K) (-1) (φ 2) = -1
Tactic: rw [norm_eq_neg_one_pow (K := K) hζ, IsCyclotomicExtension.finrank _ hirr]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
K : Type u
L : Type v
inst : CommRing L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
inst_3 : IsDomain L
inst_4 : NeZero (R := ℕ) 2
hζ : IsPrimitiveRoot ζ 2
inst_5 : IsCyclotomicExtension {2} K L
hirr : Irreducible (M := K[X]) (cyclotomic 2 K)
⊢ HPow.hPow (α := K) (-1) (φ 2) = -1
have pos : Eq.{u + 1} (α := K) (↑(Int.negSucc 0 ^ φ 2) : K) (↑(Int.negSucc 0) : K)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑(eval 1 (cyclotomic n ℤ)) : K) : K)
have this : NeZero.{u} (R := K) (↑n : K)
Tactic: haveI := IsCyclotomicExtension.neZero' n K L
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑(eval 1 (cyclotomic n ℤ)) : K) : K)
have obtain : ∀ (z : E) (hz : IsRoot (cyclotomic n E) z),
  Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑(eval 1 (cyclotomic n ℤ)) : K) : K)
Tactic: obtain ⟨z, hz⟩ := IsAlgClosed.exists_root _ (degree_cyclotomic_pos n E (NeZero.pos _)).ne.symm
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑(eval 1 (cyclotomic n ℤ)) : K) : K)
have a : Eq.{v + 1} (α := E) (((algebraMap K E : K →+* E) : (a : K) → E) ((Algebra.norm K : (a : L) → K) (ζ - 1)) : E)
  (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K) : E)
Tactic: apply (algebraMap K E).injective
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this : IsGalois K L := ⋯
⊢ Eq.{v + 1} (α := E) (((algebraMap K E : K →+* E) : (a : K) → E) ((Algebra.norm K : (a : L) → K) (ζ - 1)) : E)
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K) : E)
have a : Eq.{v + 1} (α := E) (∏ σ : L →ₐ[K] E, (σ : (a : L) → E) (ζ - 1))
  (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
Tactic: rw [norm_eq_prod_embeddings]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this : IsGalois K L := ⋯
| ∏ σ : L →ₐ[K] E, (σ : (a : L) → E) (ζ - 1)
have s : Finset.univ
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this : IsGalois K L := ⋯
s : Finset.univ
| ∏ σ : L →ₐ[K] E, (σ : (a : L) → E) (ζ - 1)
have f : fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) (ζ - 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this : IsGalois K L := ⋯
| fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) (ζ - 1)
have f : ∀ (x : L →ₐ[K] E), (x : (a : L) → E) (ζ - 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this : IsGalois K L := ⋯
x : L →ₐ[K] E
| (x : (a : L) → E) (ζ - 1)
have f : -1 * HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E)
Tactic: rw [← neg_sub, map_neg, map_sub, map_one, neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this : IsGalois K L := ⋯
| ∏ σ : L →ₐ[K] E, (σ : (a : L) → E) (ζ - 1)
have f : ∀ (x : L →ₐ[K] E), -1 * HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E)
Tactic: congr
    rfl
    ext
    rw [← neg_sub, map_neg, map_sub, map_one, neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this : IsGalois K L := ⋯
⊢ Eq.{v + 1} (α := E) (∏ σ : L →ₐ[K] E, (σ : (a : L) → E) (ζ - 1))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have a : Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, -1 * HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
  (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
Tactic: conv_lhs =>
    congr
    rfl
    ext
    rw [← neg_sub, map_neg, map_sub, map_one, neg_eq_neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this : IsGalois K L := ⋯
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, -1 * HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have a : Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
  (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
Tactic: rw [prod_mul_distrib, prod_const, Finset.card_univ, AlgHom.card,
    IsCyclotomicExtension.finrank L hirr, (totient_even h).neg_one_pow, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this : IsGalois K L := ⋯
⊢ ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
have rw : Eq.{v + 1} (α := E) (∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E))
  (∏ x : ↥(primitiveRoots n E), eval 1 (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (↑x : E) : E[X])))
Tactic: rw [cyclotomic', eval_prod, ← @Finset.prod_attach E E, ← univ_eq_attach]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this : IsGalois K L := ⋯
⊢ Eq.{v + 1} (α := E) (∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E))
    (∏ x : ↥(primitiveRoots n E), eval 1 (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) (↑x : E) : E[X])))
have refine : ∀ (σ : L →ₐ[K] E),
  HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) =
    eval 1
      (HSub.hSub (α := E[X]) X
        ((C : (a : E) → E[X])
          (↑((hζ.embeddingsEquivPrimitiveRoots E hirr : (a : L →ₐ[K] E) → ↥(primitiveRoots n E)) σ) : E)))
Tactic: refine Fintype.prod_equiv (hζ.embeddingsEquivPrimitiveRoots E hirr) _ _ fun σ => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this : IsGalois K L := ⋯
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have Hprod : ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
Tactic: have Hprod : (Finset.univ.prod fun σ : L →ₐ[K] E => 1 - σ ζ) = eval 1 (cyclotomic' n E) := by
    rw [cyclotomic', eval_prod, ← @Finset.prod_attach E E, ← univ_eq_attach]
    refine Fintype.prod_equiv (hζ.embeddingsEquivPrimitiveRoots E hirr) _ _ fun σ => ?_
    simp
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this : IsGalois K L := ⋯
Hprod : ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have this₁ : NeZero.{v} (R := E) (↑n : E)
Tactic: have : NeZero (n : E) := NeZero.of_faithfulSMul K _ n
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this_3 : IsGalois K L := ⋯
Hprod : ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
this : NeZero.{v} (R := E) (↑n : E)
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have a : eval 1 (cyclotomic' n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
Tactic: rw [Hprod, cyclotomic', ← cyclotomic_eq_prod_X_sub_primitiveRoots (isRoot_cyclotomic_iff.1 hz),
    ← map_cyclotomic_int, _root_.map_intCast, ← Int.cast_one, eval_intCast_map, eq_intCast,
    Int.cast_id]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field L
ζ : L
inst_2 : Field K
inst_3 : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst_4 : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (M := K[X]) (cyclotomic n K)
this_1 : NeZero.{u} (R := K) (↑n : K)
E : Type v := AlgebraicClosure L
z : E
hz : IsRoot (cyclotomic n E) z
this_2 : FiniteDimensional K L := ⋯
this_3 : IsGalois K L := ⋯
Hprod : ∏ σ : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((σ : (a : L) → E) ζ : E) = eval 1 (cyclotomic' n E)
this : NeZero.{v} (R := E) (↑n : E)
a : eval 1 (cyclotomic' n E) = ((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K)
⊢ Eq.{v + 1} (α := E) (∏ x : L →ₐ[K] E, HSub.hSub (α := E) (β := E) (1 : E) ((x : (a : L) → E) ζ : E))
    (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
have a₁ : Eq (α := E) (eval 1 (∏ μ ∈ primitiveRoots n E, HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) μ : E[X])))
  (((algebraMap K E : K →+* E) : (a : K) → E) (↑(eval 1 (cyclotomic n ℤ)) : K))
Tactic: rw [Hprod, cyclotomic', ← cyclotomic_eq_prod_X_sub_primitiveRoots (isRoot_cyclotomic_iff.1 hz),
    ← map_cyclotomic_int, _root_.map_intCast, ← Int.cast_one, eval_intCast_map, eq_intCast,
    Int.cast_id]