-- 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:
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

Tactic:
simp

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
⊢ IsPrimitiveRoot ζ 2

Tactic:
rwa [hk, zero_add, pow_one, hp2] at hζ

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 = 0
hζ' : ζ = -1
⊢ hζ.toInteger - 1 ∣ ↑↑p

Tactic:
replace hζ' : hζ.toInteger = -1 := by
  ext
  exact hζ'

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
⊢ hζ.toInteger - 1 ∣ ↑↑p

Proof state:
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))

Tactic:
exact prime_norm_toInteger_sub_one_of_prime_pow_ne_two hζ htwo

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
⊢ hζ.toInteger - 1 ∣ ↑↑p

Tactic:
have ⟨hp2, hk⟩ := (Nat.Prime.pow_eq_iff Nat.prime_two).1 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
hp2 : ↑p = 2
hk : k + 1 = 1
⊢ 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
hp2 : ↑p = 2
hk : k = 0
hζ' : hζ.toInteger = -1
⊢ -1 - 1 ∣ ↑2

Tactic:
exact ⟨-1, by ring⟩

Result:
no goals

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ζ.toInteger - 1 ∣ ↑↑↑p

Tactic:
have H := hζ.norm_toInteger_pow_sub_one_of_prime_pow_ne_two (zero_le _) htwo

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 ^ ↑p ^ 0 - 1) = ↑↑p ^ ↑p ^ 0
⊢ 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
⊢ hζ.toInteger - 1 ∣ ↑↑p

Tactic:
suffices (hζ.toInteger - 1) ∣ (p : ℤ) by simpa

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
⊢ 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
hp2 : ↑p = 2
hk : k = 0
⊢ hζ.toInteger - 1 ∣ ↑↑p

Tactic:
have hζ' : ζ = -1 := by
  refine IsPrimitiveRoot.eq_neg_one_of_two_right ?_
  rwa [hk, zero_add, pow_one, hp2] at hζ

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ζ' : ζ = -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))
⊢ hζ.toInteger - 1 ∣ ↑↑p

Tactic:
by_cases htwo : p ^ (k + 1) = 2

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

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
⊢ 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
⊢ hζ.toInteger - 1 ∣ ↑↑↑p

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

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ζ.toInteger - 1 ∣ ↑↑↑p

Proof state:
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)

Tactic:
exact hζ'

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
⊢ ↑p ^ (k + 1) = 2

Tactic:
exact_mod_cast htwo

Result:
no goals

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 ^ ↑p ^ 0 - 1) = ↑↑p ^ ↑p ^ 0
⊢ hζ.toInteger - 1 ∣ ↑↑↑p

Tactic:
rw [pow_zero, pow_one] at 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
⊢ hζ.toInteger - 1 ∣ ↑↑↑p