-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
/-- We have that `hζ.toInteger - 1` does not divide `2`. -/
lemma toInteger_sub_one_not_dvd_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hodd : p ≠ 2) : ¬ hζ.toInteger - 1 ∣ 2 := fun h ↦ by
  have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
  replace h : hζ.toInteger - 1 ∣ ↑(2 : ℤ)

Proof state:
case hx
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : hζ.toInteger - 1 ∣ ↑2
⊢ Prime ↑↑p

Tactic:
exact Nat.prime_iff_prime_int.1 hp.1

Result:
no goals

Proof state:
case refine_3
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : ↑↑p ∣ 2
⊢ ↑p ∣ ↑2

Tactic:
exact Int.ofNat_dvd.mp h

Result:
no goals

Proof state:
case refine_2
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : ↑↑p ∣ 2
⊢ Prime ↑2

Tactic:
exact Nat.prime_iff.1 Nat.prime_two

Result:
no goals

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
h : hζ.toInteger - 1 ∣ 2
⊢ False

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
h : hζ.toInteger - 1 ∣ 2
this : NumberField K
⊢ False

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
h : hζ.toInteger - 1 ∣ 2
this : NumberField K
⊢ False

Tactic:
replace h : hζ.toInteger - 1 ∣ ↑(2 : ℤ) := by simp [h]

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : hζ.toInteger - 1 ∣ ↑2
⊢ False

Proof state:
case hx
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : hζ.toInteger - 1 ∣ ↑2
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
rw [hζ.norm_toInteger_sub_one_of_prime_ne_two hodd]

Result:
case hx
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : hζ.toInteger - 1 ∣ ↑2
⊢ Prime ↑↑p

Proof state:
case refine_1
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : ↑↑p ∣ 2
⊢ Prime ↑p

Tactic:
exact Nat.prime_iff.1 hp.1

Result:
no goals

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : ↑↑p ∣ 2
⊢ False

Tactic:
refine hodd <| PNat.coe_inj.1 <| (prime_dvd_prime_iff_eq ?_ ?_).1 ?_

Result:
case refine_1
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : ↑↑p ∣ 2
⊢ Prime ↑p

case refine_2
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : ↑↑p ∣ 2
⊢ Prime ↑2

case refine_3
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : ↑↑p ∣ 2
⊢ ↑p ∣ ↑2

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : hζ.toInteger - 1 ∣ ↑2
⊢ False

Tactic:
rw [← Ideal.norm_dvd_iff, hζ.norm_toInteger_sub_one_of_prime_ne_two hodd] at h

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : ↑↑p ∣ 2
⊢ False

case hx
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K
h : hζ.toInteger - 1 ∣ ↑2
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
h : hζ.toInteger - 1 ∣ 2
this : NumberField K
⊢ hζ.toInteger - 1 ∣ ↑2

Tactic:
simp [h]

Result:
no goals