-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem sub_one_norm_isPrimePow (hn : IsPrimePow (n : ℕ)) [IsCyclotomicExtension {n} K L]
    (hirr : Irreducible (cyclotomic (n : ℕ) K)) (h : n ≠ 2) : norm K (ζ - 1) = (n : ℕ).minFac

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
hn : IsPrimePow ↑n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
h : n ≠ 2
this : 2 < n
⊢ (Algebra.norm K) (ζ - 1) = ↑(↑n).minFac

Tactic:
letI hprime : Fact (n : ℕ).minFac.Prime := ⟨minFac_prime (IsPrimePow.ne_one hn)⟩

Result:
n : ℕ+
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
hn : IsPrimePow ↑n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
h : n ≠ 2
this : 2 < n
hprime : Fact (Nat.Prime (↑n).minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }
⊢ (Algebra.norm K) (ζ - 1) = ↑(↑n).minFac

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
hn : IsPrimePow ↑n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
h : n ≠ 2
this : 2 < n
hprime : Fact (Nat.Prime (↑n).minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }
⊢ ↑(eval 1 (cyclotomic ((↑n).minFac ^ (↑n).factorization (↑n).minFac) ℤ)) = ↑(↑n).minFac

Tactic:
obtain ⟨k, hk⟩ : ∃ k, (n : ℕ).factorization (n : ℕ).minFac = k + 1 :=
  exists_eq_succ_of_ne_zero
    (((n : ℕ).factorization.mem_support_toFun (n : ℕ).minFac).1 <|
      mem_primeFactors_iff_mem_primeFactorsList.2 <|
        (mem_primeFactorsList (IsPrimePow.ne_zero hn)).2 ⟨hprime.out, minFac_dvd _⟩)

Result:
case intro
n : ℕ+
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
hn : IsPrimePow ↑n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
h : n ≠ 2
this : 2 < n
hprime : Fact (Nat.Prime (↑n).minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }
k : ℕ
hk : (↑n).factorization (↑n).minFac = k + 1
⊢ ↑(eval 1 (cyclotomic ((↑n).minFac ^ (↑n).factorization (↑n).minFac) ℤ)) = ↑(↑n).minFac

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
hn : IsPrimePow ↑n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
h : n ≠ 2
this : 2 < n
hprime : Fact (Nat.Prime (↑n).minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }
⊢ ↑(eval 1 (cyclotomic ↑n ℤ)) = ↑(↑n).minFac

Tactic:
nth_rw 1 [← IsPrimePow.minFac_pow_factorization_eq hn]

Result:
n : ℕ+
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
hn : IsPrimePow ↑n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
h : n ≠ 2
this : 2 < n
hprime : Fact (Nat.Prime (↑n).minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }
⊢ ↑(eval 1 (cyclotomic ((↑n).minFac ^ (↑n).factorization (↑n).minFac) ℤ)) = ↑(↑n).minFac

Proof state:
case intro
n : ℕ+
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
hn : IsPrimePow ↑n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
h : n ≠ 2
this : 2 < n
hprime : Fact (Nat.Prime (↑n).minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }
k : ℕ
hk : (↑n).factorization (↑n).minFac = k + 1
⊢ ↑(eval 1 (cyclotomic ((↑n).minFac ^ (↑n).factorization (↑n).minFac) ℤ)) = ↑(↑n).minFac

Tactic:
simp [hk, sub_one_norm_eq_eval_cyclotomic hζ this hirr]

Result:
no goals

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
hn : IsPrimePow ↑n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
h : n ≠ 2
⊢ (Algebra.norm K) (ζ - 1) = ↑(↑n).minFac

Tactic:
have :=
  (coe_lt_coe 2 _).1
    (lt_of_le_of_ne (succ_le_of_lt (IsPrimePow.one_lt hn))
      (Function.Injective.ne PNat.coe_injective h).symm)

Result:
n : ℕ+
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
hn : IsPrimePow ↑n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
h : n ≠ 2
this : 2 < n
⊢ (Algebra.norm K) (ζ - 1) = ↑(↑n).minFac

Proof state:
n : ℕ+
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
hn : IsPrimePow ↑n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
h : n ≠ 2
this : 2 < n
hprime : Fact (Nat.Prime (↑n).minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }
⊢ (Algebra.norm K) (ζ - 1) = ↑(↑n).minFac

Tactic:
rw [sub_one_norm_eq_eval_cyclotomic hζ this hirr]

Result:
n : ℕ+
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ ↑n
hn : IsPrimePow ↑n
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic (↑n) K)
h : n ≠ 2
this : 2 < n
hprime : Fact (Nat.Prime (↑n).minFac) := { out := minFac_prime (IsPrimePow.ne_one hn) }
⊢ ↑(eval 1 (cyclotomic ↑n ℤ)) = ↑(↑n).minFac