awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 + 1 - s))

Tactic:
hη
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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⟮η⟯
h : p ^ (k - s + 1) = p ^ (k + 1 - s)
⊢ IsPrimitiveRoot (↑(η₁ + 1) : L) (p ^ (k - s + 1))

Tactic:
convert! hη using 1
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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⟮η⟯
h h₁ : p ^ (k - s + 1) = p ^ (k - s + 1)
⊢ p ^ (k - s + 1) = p ^ (k + 1 - s)

Tactic:
rw [Nat.sub_add_comm hs]

Premises used: Nat.sub_add_comm
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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))

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]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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))
⊢ FiniteDimensional K L

Tactic:
have := IsCyclotomicExtension.finiteDimensional {p ^ (k + 1)} K L
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ IsGalois K L

Tactic:
have := IsCyclotomicExtension.isGalois {p ^ (k + 1)} K L
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
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)
⊢ (Algebra.norm K : (a : L) → K) η = HPow.hPow (α := K) (↑p : K) (p ^ s)

Tactic:
rw [norm_eq_norm_adjoin K]

Premises used: Algebra.norm_eq_norm_adjoin
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
refine_1 : IsPrimePow (p ^ (k - s + 1))
⊢ 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
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ IsPrimePow (p ^ (k - s + 1))

Tactic:
hpri.1.isPrimePow.pow (Nat.succ_ne_zero _)

Premises used: Nat.succ_ne_zero, Nat.Prime.isPrimePow, IsPrimePow.pow, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ IsPrimePow (p ^ (k - s + 1))

Tactic:
exact hpri.1.isPrimePow.pow (Nat.succ_ne_zero _)

Premises used: Nat.succ_ne_zero, Nat.Prime.isPrimePow, IsPrimePow.pow, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ 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

Premises used: add_sub_cancel_right
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 :
  HPow.hPow (α := K) (↑(p ^ (k - s + 1)).minFac : 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)

Tactic:
rw [H]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
refine_2₁ : Module.finrank (↥K⟮η⟯) L = p ^ s
⊢ HPow.hPow (α := K) (↑(p ^ (k - s + 1)).minFac : K) (Module.finrank (↥K⟮η⟯) L) = HPow.hPow (α := K) (↑p : K) (p ^ s)

Tactic:
congr
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 : k - s + 1 ≠ 0
⊢ (p ^ (k - s + 1)).minFac = p

Tactic:
rw [Nat.pow_minFac, hpri.1.minFac_eq]

Premises used: Nat.Prime.minFac_eq, Nat.pow_minFac, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ k - s + 1 ≠ 0

Tactic:
Nat.succ_ne_zero _

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ k - s + 1 ≠ 0

Tactic:
exact Nat.succ_ne_zero _

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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.{u, v} K ↥K⟮η⟯ * Module.finrank (↥K⟮η⟯) L = Module.finrank K L

Tactic:
have := Module.finrank_mul_finrank K K⟮η⟯ L
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : Module.finrank.{u, v} K ↥K⟮η⟯ * Module.finrank (↥K⟮η⟯) L = Module.finrank K L
⊢ (p - 1) * (p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L) = (p - 1) * p ^ (k.succ - 1)

Tactic:
rw [IsCyclotomicExtension.finrank L hirr, IsCyclotomicExtension.finrank K⟮η⟯ hirr₁,
    Nat.totient_prime_pow hpri.out (k - s).succ_pos, Nat.totient_prime_pow hpri.out k.succ_pos,
    mul_comm _ (p - 1), mul_assoc, mul_comm (p ^ (k.succ - 1))] at this

Premises used: Nat.totient_prime_pow, mul_assoc, HSub.hSub, Membership.mem, IsCyclotomicExtension.finrank, Subtype, HPow.hPow, Nat.succ_pos, IntermediateField.adjoin, mul_comm, Singleton.singleton, OfNat.ofNat, Nat.succ, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : (p - 1) * (p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L) = (p - 1) * p ^ (k.succ - 1)
⊢ p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)

Tactic:
replace this := mul_left_cancel₀ (tsub_pos_iff_lt.2 hpri.out.one_lt).ne' this
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
simp : k = k - s + s
⊢ k.succ - 1 = (k - s).succ - 1 + s

Tactic:
simp only [Nat.succ_sub_succ_eq_sub, tsub_zero]

Premises used: tsub_zero, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
⊢ k = k - s + s

Tactic:
(Nat.sub_add_cancel hs).symm

Premises used: Nat.sub_add_cancel, Eq.symm
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
⊢ k = k - s + s

Tactic:
exact (Nat.sub_add_cancel hs).symm

Premises used: Nat.sub_add_cancel, Eq.symm
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
⊢ k.succ - 1 = (k - s).succ - 1 + s

Tactic:
have Hex : k.succ - 1 = (k - s).succ - 1 + s := by
    simp only [Nat.succ_sub_succ_eq_sub, tsub_zero]
    exact (Nat.sub_add_cancel hs).symm
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
Hex : k.succ - 1 = (k - s).succ - 1 + s
⊢ p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ ((k - s).succ - 1) * p ^ s

Tactic:
rw [Hex, pow_add] at this

Premises used: pow_add
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
Hex : k.succ - 1 = (k - s).succ - 1 + s
this₁ : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ ((k - s).succ - 1) * p ^ s
⊢ k.succ - 1 = (k - s).succ - 1 + s

Tactic:
rw [Hex, pow_add] at this

Premises used: pow_add