-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem norm_sub_one_of_prime_ne_two' [hpri : Fact (p : ℕ).Prime]
    [hcyc : IsCyclotomicExtension {p} K L] (hζ : IsPrimitiveRoot ζ p)
    (hirr : Irreducible (cyclotomic p K)) (h : p ≠ 2) : norm K (ζ - 1) = p

Proof state:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime ↑p)
hcyc : IsCyclotomicExtension {p} K L
hζ : IsPrimitiveRoot ζ ↑p
h : p ≠ 2
hirr : Irreducible (cyclotomic (↑p ^ (0 + 1)) K)
⊢ IsPrimitiveRoot ζ (↑p ^ (0 + 1))

Tactic:
simp [hζ]

Result:
no goals

Proof state:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime ↑p)
hcyc : IsCyclotomicExtension {p} K L
h : p ≠ 2
hirr : Irreducible (cyclotomic (↑p ^ (0 + 1)) K)
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
⊢ (Algebra.norm K) (ζ - 1) = ↑↑p

Tactic:
simpa using norm_sub_one_of_prime_ne_two hζ hirr h

Result:
no goals

Proof state:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime ↑p)
hcyc : IsCyclotomicExtension {p} K L
hζ : IsPrimitiveRoot ζ ↑p
h : p ≠ 2
hirr : Irreducible (cyclotomic (↑p ^ (0 + 1)) K)
⊢ (Algebra.norm K) (ζ - 1) = ↑↑p

Tactic:
replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1) : ℕ) := by simp [hζ]

Result:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime ↑p)
hcyc : IsCyclotomicExtension {p} K L
h : p ≠ 2
hirr : Irreducible (cyclotomic (↑p ^ (0 + 1)) K)
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ (Algebra.norm K) (ζ - 1) = ↑↑p

Proof state:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime ↑p)
hcyc : IsCyclotomicExtension {p} K L
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
h : p ≠ 2
⊢ Irreducible (cyclotomic (↑p ^ (0 + 1)) K)

Tactic:
simp [hirr]

Result:
no goals

Proof state:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime ↑p)
hcyc : IsCyclotomicExtension {p} K L
h : p ≠ 2
hirr : Irreducible (cyclotomic (↑p ^ (0 + 1)) K)
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ IsCyclotomicExtension {p ^ (0 + 1)} K L

Tactic:
simp [hcyc]

Result:
no goals

Proof state:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime ↑p)
hcyc : IsCyclotomicExtension {p} K L
h : p ≠ 2
hirr : Irreducible (cyclotomic (↑p ^ (0 + 1)) K)
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ (Algebra.norm K) (ζ - 1) = ↑↑p

Tactic:
haveI : IsCyclotomicExtension {p ^ (0 + 1)} K L := by simp [hcyc]

Result:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime ↑p)
hcyc : IsCyclotomicExtension {p} K L
h : p ≠ 2
hirr : Irreducible (cyclotomic (↑p ^ (0 + 1)) K)
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
⊢ (Algebra.norm K) (ζ - 1) = ↑↑p

Proof state:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime ↑p)
hcyc : IsCyclotomicExtension {p} K L
hζ : IsPrimitiveRoot ζ ↑p
hirr : Irreducible (cyclotomic (↑p) K)
h : p ≠ 2
⊢ (Algebra.norm K) (ζ - 1) = ↑↑p

Tactic:
replace hirr : Irreducible (cyclotomic (p ^ (0 + 1) : ℕ) K) := by simp [hirr]

Result:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
hpri : Fact (Nat.Prime ↑p)
hcyc : IsCyclotomicExtension {p} K L
hζ : IsPrimitiveRoot ζ ↑p
h : p ≠ 2
hirr : Irreducible (cyclotomic (↑p ^ (0 + 1)) K)
⊢ (Algebra.norm K) (ζ - 1) = ↑↑p