awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ LE.le (α := IntermediateField K L) K⟮η + 1⟯ K⟮η⟯
have refine_2 : Membership.mem (γ := IntermediateField K L) K⟮η⟯ (η + 1)
Tactic: rw [IntermediateField.adjoin_simple_le_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ Membership.mem (γ := IntermediateField K L) K⟮η + 1⟯ η
have refine_1 : Membership.mem (γ := IntermediateField K L) K⟮η + 1⟯ (η + 1 - 1)
Tactic: nth_rw 2 [← add_sub_cancel_right η 1]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
have HKη : Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
Tactic: have HKη : K⟮η⟯ = K⟮η + 1⟯ := by
      refine le_antisymm ?_ ?_
      all_goals rw [IntermediateField.adjoin_simple_le_iff]
      · nth_rw 2 [← add_sub_cancel_right η 1]
        exact sub_mem (IntermediateField.mem_adjoin_simple_self K (η + 1)) (one_mem _)
      · exact add_mem (IntermediateField.mem_adjoin_simple_self K η) (one_mem _)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
⊢ IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
have rw : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η + 1⟯
Tactic: rw [HKη]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
⊢ IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η + 1⟯
have H : Eq (α := Subalgebra K L) (IntermediateField.toSubalgebra K⟮η + 1⟯) K[η + 1]
Tactic: have H := IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
      ((integral {p ^ (k + 1)} K L).isIntegral (η + 1)).isAlgebraic
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
H : Eq (α := Subalgebra K L) (IntermediateField.toSubalgebra K⟮η + 1⟯) K[η + 1]
⊢ IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η + 1⟯
have refine : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥(IntermediateField.toSubalgebra K⟮η + 1⟯)
Tactic: refine IsCyclotomicExtension.equiv _ _ _ (h := ?_) (.refl : K⟮η + 1⟯.toSubalgebra ≃ₐ[K] _)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
H : Eq (α := Subalgebra K L) (IntermediateField.toSubalgebra K⟮η + 1⟯) K[η + 1]
⊢ IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥(IntermediateField.toSubalgebra K⟮η + 1⟯)
have rw : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K[η + 1]
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
H : Eq (α := Subalgebra K L) (IntermediateField.toSubalgebra K⟮η + 1⟯) K[η + 1]
hη' : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K[η + 1]
have h : Eq (α := Set ℕ) {p ^ (k - s + 1)} {p ^ (k + 1 - s)}
Tactic: convert! hη'.adjoin_isCyclotomicExtension K using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
H : Eq (α := Subalgebra K L) (IntermediateField.toSubalgebra K⟮η + 1⟯) K[η + 1]
hη' : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ Eq (α := Set ℕ) {p ^ (k - s + 1)} {p ^ (k + 1 - s)}
have h : Eq (α := Set ℕ) {p ^ (k - s + 1)} {p ^ (k - s + 1)}
Tactic: rw [Nat.sub_add_comm hs]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ (Algebra.norm K : (a : L) → K) η = HPow.hPow (α := K) (↑p : K) (p ^ s)
have this : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
Tactic: have : IsCyclotomicExtension {p ^ (k - s + 1)} K K⟮η⟯ := by
    have HKη : K⟮η⟯ = K⟮η + 1⟯ := by
      refine le_antisymm ?_ ?_
      all_goals rw [IntermediateField.adjoin_simple_le_iff]
      · nth_rw 2 [← add_sub_cancel_right η 1]
        exact sub_mem (IntermediateField.mem_adjoin_simple_self K (η + 1)) (one_mem _)
      · exact add_mem (IntermediateField.mem_adjoin_simple_self K η) (one_mem _)
    rw [HKη]
    have H := IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
      ((integral {p ^ (k + 1)} K L).isIntegral (η + 1)).isAlgebraic
    refine IsCyclotomicExtension.equiv _ _ _ (h := ?_) (.refl : K⟮η + 1⟯.toSubalgebra ≃ₐ[K] _)
    rw [H]
    have hη' : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s)) := by simpa using hη
    convert! hη'.adjoin_isCyclotomicExtension K using 1
    rw [Nat.sub_add_comm hs]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
this : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
⊢ IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
have apply : IsPrimitiveRoot (↑(η₁ + 1) : L) (p ^ (k - s + 1))
Tactic: apply coe_submonoidClass_iff.1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
this : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
⊢ IsPrimitiveRoot (↑(η₁ + 1) : L) (p ^ (k - s + 1))
have h : p ^ (k - s + 1) = p ^ (k + 1 - s)
Tactic: convert! hη using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
this : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
⊢ p ^ (k - s + 1) = p ^ (k + 1 - s)
have h : p ^ (k - s + 1) = p ^ (k - s + 1)
Tactic: rw [Nat.sub_add_comm hs]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
this : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
⊢ (Algebra.norm K : (a : L) → K) η = HPow.hPow (α := K) (↑p : K) (p ^ s)
have hη₁ : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
Tactic: replace hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1)) := by
    apply coe_submonoidClass_iff.1
    convert! hη using 1
    rw [Nat.sub_add_comm hs]
Cleared hypotheses: hη
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
⊢ (Algebra.norm K : (a : L) → K) η = HPow.hPow (α := K) (↑p : K) (p ^ s)
have this₁ : FiniteDimensional K L
Tactic: have := IsCyclotomicExtension.finiteDimensional {p ^ (k + 1)} K L
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this : FiniteDimensional K L
⊢ (Algebra.norm K : (a : L) → K) η = HPow.hPow (α := K) (↑p : K) (p ^ s)
have this₁ : IsGalois K L
Tactic: have := IsCyclotomicExtension.isGalois {p ^ (k + 1)} K L
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this : IsGalois K L
⊢ (Algebra.norm K : (a : L) → K) η = HPow.hPow (α := K) (↑p : K) (p ^ s)
have rw : HPow.hPow (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) (IntermediateField.AdjoinSimple.gen K η) : K)
    (Module.finrank (↥K⟮η⟯) L) =
  HPow.hPow (α := K) (↑p : K) (p ^ s)
Tactic: rw [norm_eq_norm_adjoin K]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this : IsGalois K L
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) (IntermediateField.AdjoinSimple.gen K η) : K)
      (Module.finrank (↥K⟮η⟯) L) =
    HPow.hPow (α := K) (↑p : K) (p ^ s)
have refine_2 : ∀ (H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) (η₁ + 1 - 1) : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)),
  HPow.hPow (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) (IntermediateField.AdjoinSimple.gen K η) : K)
      (Module.finrank (↥K⟮η⟯) L) =
    HPow.hPow (α := K) (↑p : K) (p ^ s)
Tactic: have H := hη.sub_one_norm_isPrimePow ?_ hirr₁ htwo
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this : IsGalois K L
refine_2 :
  ∀
    (H :
      Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) (η₁ + 1 - 1) : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)),
    HPow.hPow (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) (IntermediateField.AdjoinSimple.gen K η) : K)
        (Module.finrank (↥K⟮η⟯) L) =
      HPow.hPow (α := K) (↑p : K) (p ^ s)
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) (IntermediateField.AdjoinSimple.gen K η) : K)
      (Module.finrank (↥K⟮η⟯) L) =
    HPow.hPow (α := K) (↑p : K) (p ^ s)
have refine_1 : IsPrimePow (p ^ (k - s + 1))
Tactic: have H := hη.sub_one_norm_isPrimePow ?_ hirr₁ htwo
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) (η₁ + 1 - 1) : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) (IntermediateField.AdjoinSimple.gen K η) : K)
      (Module.finrank (↥K⟮η⟯) L) =
    HPow.hPow (α := K) (↑p : K) (p ^ s)
have H₁ : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
Tactic: rw [add_sub_cancel_right] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) (IntermediateField.AdjoinSimple.gen K η) : K)
      (Module.finrank (↥K⟮η⟯) L) =
    HPow.hPow (α := K) (↑p : K) (p ^ s)
have refine_2 : HPow.hPow (α := K) (↑(p ^ (k - s + 1)).minFac : K) (Module.finrank (↥K⟮η⟯) L) = HPow.hPow (α := K) (↑p : K) (p ^ s)
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
⊢ HPow.hPow (α := K) (↑(p ^ (k - s + 1)).minFac : K) (Module.finrank (↥K⟮η⟯) L) = HPow.hPow (α := K) (↑p : K) (p ^ s)
have refine_2 : (p ^ (k - s + 1)).minFac = p
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
refine_2 : (p ^ (k - s + 1)).minFac = p
⊢ HPow.hPow (α := K) (↑(p ^ (k - s + 1)).minFac : K) (Module.finrank (↥K⟮η⟯) L) = HPow.hPow (α := K) (↑p : K) (p ^ s)
have refine_2₁ : Module.finrank (↥K⟮η⟯) L = p ^ s
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
⊢ (p ^ (k - s + 1)).minFac = p
have refine_2 : k - s + 1 ≠ 0
Tactic: rw [Nat.pow_minFac, hpri.1.minFac_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
⊢ Module.finrank (↥K⟮η⟯) L = p ^ s
have this₁ : Module.finrank.{u, v} K ↥K⟮η⟯ * Module.finrank (↥K⟮η⟯) L = Module.finrank K L
Tactic: have := Module.finrank_mul_finrank K K⟮η⟯ L