-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
/-- In a `p ^ (k + 1)`-th cyclotomic extension of `ℚ`, we have that
  `ζ - 1` divides `p` in `𝓞 K`. -/
lemma toInteger_sub_one_dvd_prime [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) : ((hζ.toInteger - 1)) ∣ p

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ↑p ^ (k + 1) = 2
hp2 : ↑p = 2
hk : k = 0
⊢ ζ = -1

Tactic:
refine IsPrimitiveRoot.eq_neg_one_of_two_right ?_

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ↑p ^ (k + 1) = 2
hp2 : ↑p = 2
hk : k = 0
⊢ IsPrimitiveRoot ζ 2

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

Tactic:
simpa

Result:
no goals

Proof state:
case pos
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ↑p ^ (k + 1) = 2
hp2 : ↑p = 2
hk : k + 1 = 1
⊢ hζ.toInteger - 1 ∣ ↑↑p

Tactic:
simp only [add_left_eq_self] at hk

Result:
case pos
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ↑p ^ (k + 1) = 2
hp2 : ↑p = 2
hk : k = 0
⊢ hζ.toInteger - 1 ∣ ↑↑p

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

Tactic:
replace htwo : (p : ℕ) ^ (k + 1) = 2 := by exact_mod_cast htwo

Result:
case pos
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ↑p ^ (k + 1) = 2
⊢ hζ.toInteger - 1 ∣ ↑↑p

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

Tactic:
rw [← Ideal.norm_dvd_iff, H]

Result:
case neg
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
this : NumberField K
H : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p ^ 1
⊢ ↑↑p ^ 1 ∣ ↑↑p

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

Proof state:
case pos
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ↑p ^ (k + 1) = 2
hp2 : ↑p = 2
hk : k = 0
hζ' : hζ.toInteger = -1
⊢ hζ.toInteger - 1 ∣ ↑↑p

Tactic:
rw [hζ', hp2]

Result:
case pos
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ↑p ^ (k + 1) = 2
hp2 : ↑p = 2
hk : k = 0
hζ' : hζ.toInteger = -1
⊢ -1 - 1 ∣ ↑2

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ↑p ^ (k + 1) = 2
hp2 : ↑p = 2
hk : k = 0
hζ' : hζ.toInteger = -1
⊢ ↑2 = (-1 - 1) * -1

Tactic:
ring

Result:
no goals

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ↑p ^ (k + 1) = 2
hp2 : ↑p = 2
hk : k = 0
hζ' : ζ = -1
⊢ hζ.toInteger = -1

Tactic:
ext

Result:
case h
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
htwo : ↑p ^ (k + 1) = 2
hp2 : ↑p = 2
hk : k = 0
hζ' : ζ = -1
⊢ ↑hζ.toInteger = ↑(-1)