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
⊢ Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)

Tactic:
have hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K) :=
    cyclotomic_irreducible_pow_of_irreducible_pow hpri.1 (by lia) hirr
-- 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)
set :
  let η := ζ ^ p ^ s - 1;
  (Algebra.norm K : (a : L) → K) η = HPow.hPow (α := K) (↑p : K) (p ^ s)
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)

Tactic:
set η := ζ ^ p ^ s - 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 η
rw : IsPrimitiveRoot (ζ ^ p ^ s) (p ^ (k + 1 - s))
⊢ IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))

Tactic:
rw [sub_add_cancel]

Premises used: sub_add_cancel
-- 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 η
⊢ IsPrimitiveRoot (ζ ^ p ^ s) (p ^ (k + 1 - s))

Tactic:
IsPrimitiveRoot.pow (pos_of_neZero (p ^ (k + 1))) hζ ?_

Premises used: IsPrimitiveRoot.pow, HPow.hPow, HAdd.hAdd, Nat.pos_of_neZero, OfNat.ofNat
-- 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 η
refine : p ^ (k + 1) = p ^ s * p ^ (k + 1 - s)
⊢ IsPrimitiveRoot (ζ ^ p ^ s) (p ^ (k + 1 - s))

Tactic:
refine IsPrimitiveRoot.pow (pos_of_neZero (p ^ (k + 1))) hζ ?_

Premises used: IsPrimitiveRoot.pow, HPow.hPow, HAdd.hAdd, Nat.pos_of_neZero, OfNat.ofNat
-- 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 η
rw : p ^ (k + 1) = p ^ (s + (k + 1 - s))
rw₁ : p ^ (k + 1) = p ^ (k + 1 - s + s)
rw₂ rw₃ : p ^ (k + 1) = p ^ k.succ
⊢ p ^ (k + 1) = p ^ s * p ^ (k + 1 - s)

Tactic:
rw [← pow_add, add_comm s, Nat.sub_add_cancel (le_trans hs (Nat.le_succ k))]

Premises used: pow_add, Nat.le_succ, add_comm, Nat.sub_add_cancel, le_trans
-- 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 η
⊢ IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))

Tactic:
have hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s)) := by
    rw [sub_add_cancel]
    refine IsPrimitiveRoot.pow (pos_of_neZero (p ^ (k + 1))) hζ ?_
    rw [← pow_add, add_comm s, Nat.sub_add_cancel (le_trans hs (Nat.le_succ k))]
-- 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))
⊢ Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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))
refine_1 : LE.le (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
refine_2 : LE.le (α := IntermediateField K L) K⟮η + 1⟯ K⟮η⟯
⊢ Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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))
refine_1 : Membership.mem (γ := IntermediateField K L) K⟮η + 1⟯ η
⊢ LE.le (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯

Tactic:
rw [IntermediateField.adjoin_simple_le_iff]

Premises used: IntermediateField.adjoin_simple_le_iff
-- 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))
refine_2 : Membership.mem (γ := IntermediateField K L) K⟮η⟯ (η + 1)
⊢ LE.le (α := IntermediateField K L) K⟮η + 1⟯ K⟮η⟯

Tactic:
rw [IntermediateField.adjoin_simple_le_iff]

Premises used: IntermediateField.adjoin_simple_le_iff
-- 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))
refine_1 : Membership.mem (γ := IntermediateField K L) K⟮η + 1⟯ (η + 1 - 1)
⊢ Membership.mem (γ := IntermediateField K L) K⟮η + 1⟯ η

Tactic:
nth_rw 2 [← add_sub_cancel_right η 1]

Premises used: add_sub_cancel_right, OfNat.ofNat
-- 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))
⊢ Membership.mem (γ := IntermediateField K L) K⟮η + 1⟯ (η + 1 - 1)

Tactic:
sub_mem (IntermediateField.mem_adjoin_simple_self K (η + 1)) (one_mem _)

Premises used: IntermediateField.mem_adjoin_simple_self, sub_mem, HAdd.hAdd, OneMemClass.one_mem, OfNat.ofNat
-- 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))
⊢ Membership.mem (γ := IntermediateField K L) K⟮η + 1⟯ (η + 1 - 1)

Tactic:
exact sub_mem (IntermediateField.mem_adjoin_simple_self K (η + 1)) (one_mem _)

Premises used: IntermediateField.mem_adjoin_simple_self, sub_mem, HAdd.hAdd, OneMemClass.one_mem, OfNat.ofNat
-- 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))
⊢ Membership.mem (γ := IntermediateField K L) K⟮η⟯ (η + 1)

Tactic:
add_mem (IntermediateField.mem_adjoin_simple_self K η) (one_mem _)

Premises used: IntermediateField.mem_adjoin_simple_self, AddMemClass.add_mem, OneMemClass.one_mem
-- 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))
⊢ Membership.mem (γ := IntermediateField K L) K⟮η⟯ (η + 1)

Tactic:
exact add_mem (IntermediateField.mem_adjoin_simple_self K η) (one_mem _)

Premises used: IntermediateField.mem_adjoin_simple_self, AddMemClass.add_mem, OneMemClass.one_mem
-- 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))
⊢ 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 _)
-- 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))
HKη : Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
rw : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η + 1⟯
⊢ IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯

Tactic:
rw [HKη]
-- 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))
HKη : Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
⊢ 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
-- 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))
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⟯

Tactic:
IsCyclotomicExtension.equiv _ _ _ (h := ?_) (.refl : K⟮η + 1⟯.toSubalgebra ≃ₐ[K] _)

Premises used: IsCyclotomicExtension.equiv, AlgEquiv.refl
-- 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))
HKη : Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
H : Eq (α := Subalgebra K L) (IntermediateField.toSubalgebra K⟮η + 1⟯) K[η + 1]
refine : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥(IntermediateField.toSubalgebra K⟮η + 1⟯)
⊢ IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η + 1⟯

Tactic:
refine IsCyclotomicExtension.equiv _ _ _ (h := ?_) (.refl : K⟮η + 1⟯.toSubalgebra ≃ₐ[K] _)

Premises used: IsCyclotomicExtension.equiv, AlgEquiv.refl
-- 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))
HKη : Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
H : Eq (α := Subalgebra K L) (IntermediateField.toSubalgebra K⟮η + 1⟯) K[η + 1]
rw : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K[η + 1]
⊢ IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥(IntermediateField.toSubalgebra K⟮η + 1⟯)

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 η
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]
⊢ IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))

Tactic:
simpa using 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))
HKη : Eq (α := IntermediateField K L) K⟮η⟯ K⟮η + 1⟯
H : Eq (α := Subalgebra K L) (IntermediateField.toSubalgebra K⟮η + 1⟯) K[η + 1]
⊢ IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))

Tactic:
have hη' : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s)) := by simpa using 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))
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 + 1 - s)} K ↥K[η + 1]

Tactic:
hη'.adjoin_isCyclotomicExtension K

Premises used: IsPrimitiveRoot.adjoin_isCyclotomicExtension
-- 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))
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))
h : Eq (α := Set ℕ) {p ^ (k - s + 1)} {p ^ (k + 1 - s)}
⊢ IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K[η + 1]

Tactic:
convert! hη'.adjoin_isCyclotomicExtension K using 1

Premises used: IsPrimitiveRoot.adjoin_isCyclotomicExtension
-- 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))
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))
h h₁ : Eq (α := Set ℕ) {p ^ (k - s + 1)} {p ^ (k - s + 1)}
⊢ Eq (α := Set ℕ) {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))
⊢ 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]
-- 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⟮η⟯
apply : IsPrimitiveRoot (↑(η₁ + 1) : L) (p ^ (k - s + 1))
⊢ IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))

Tactic:
apply coe_submonoidClass_iff.1

Premises used: IsPrimitiveRoot.coe_submonoidClass_iff, Iff.mp