-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem zeta_sub_one_prime_of_two_pow [IsCyclotomicExtension {(2 : ℕ+) ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑((2 : ℕ+) ^ (k + 1))) :
    Prime (hζ.toInteger - 1)

Proof state:
case h.e'_3.a
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (n✝ + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (n✝ + 1 + 1))
this : NumberField K := numberField {2 ^ (n✝ + 1 + 1)} ℚ K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = (algebraMap ℤ ℚ) 2

Tactic:
simp only [PNat.pow_coe, id.map_eq_id, RingHomCompTriple.comp_eq, RingHom.coe_coe,
  Subalgebra.coe_val, algebraMap_int_eq, map_natCast]

Result:
case h.e'_3.a
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (n✝ + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (n✝ + 1 + 1))
this : NumberField K := numberField {2 ^ (n✝ + 1 + 1)} ℚ K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = (Int.castRingHom ℚ) 2

Proof state:
case h.e'_3
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (n✝ + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (n✝ + 1 + 1))
this : NumberField K := numberField {2 ^ (n✝ + 1 + 1)} ℚ K
⊢ (Algebra.norm ℤ) (hζ.toInteger - 1) = 2

Tactic:
apply RingHom.injective_int (algebraMap ℤ ℚ)

Result:
case h.e'_3.a
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (n✝ + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (n✝ + 1 + 1))
this : NumberField K := numberField {2 ^ (n✝ + 1 + 1)} ℚ K
⊢ (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (hζ.toInteger - 1)) = (algebraMap ℤ ℚ) 2

Proof state:
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (n✝ + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (n✝ + 1 + 1))
this : NumberField K := numberField {2 ^ (n✝ + 1 + 1)} ℚ K
⊢ 0 < 2 ^ (n✝ + 1 + 1)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3.a
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
this : NumberField K := numberField {2 ^ (0 + 1)} ℚ K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = -2

Tactic:
simpa only [zero_add, pow_one, AddSubgroupClass.coe_sub, OneMemClass.coe_one,
    pow_zero]
  using hζ.norm_pow_sub_one_two (cyclotomic.irreducible_rat
    (by simp only [zero_add, pow_one, Nat.ofNat_pos]))

Result:
no goals

Proof state:
case refine_2
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))
this : NumberField K := numberField {2 ^ (k + 1)} ℚ K
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
cases k

Result:
case refine_2.zero
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
this : NumberField K := numberField {2 ^ (0 + 1)} ℚ K
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

case refine_2.succ
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (n✝ + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (n✝ + 1 + 1))
this : NumberField K := numberField {2 ^ (n✝ + 1 + 1)} ℚ K
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Proof state:
case h.e'_3.a
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (n✝ + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (n✝ + 1 + 1))
this : NumberField K := numberField {2 ^ (n✝ + 1 + 1)} ℚ K
⊢ (algebraMap ℤ ℚ) ((Algebra.norm ℤ) (hζ.toInteger - 1)) = (algebraMap ℤ ℚ) 2

Tactic:
rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)]

Result:
case h.e'_3.a
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (n✝ + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (n✝ + 1 + 1))
this : NumberField K := numberField {2 ^ (n✝ + 1 + 1)} ℚ K
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = (algebraMap ℤ ℚ) 2

Proof state:
case refine_2.zero
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
this : NumberField K := numberField {2 ^ (0 + 1)} ℚ K
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
convert Prime.neg Int.prime_two

Result:
case h.e'_3
K : Type u
inst✝² : Field K
ζ : K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {2 ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(2 ^ (0 + 1))
this : NumberField K := numberField {2 ^ (0 + 1)} ℚ K
⊢ (Algebra.norm ℤ) (hζ.toInteger - 1) = -2