-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem not_exists_int_prime_dvd_sub_of_prime_pow_ne_two
    [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (htwo : p ^ (k + 1) ≠ 2) :
    ¬(∃ n : ℤ, (p : 𝓞 K) ∣ (hζ.toInteger - n : 𝓞 K))

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
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h : 1 = (pB.basis.repr (↑↑p * x)) ⟨1, hdim⟩ + (pB.basis.repr ↑n) ⟨1, hdim⟩
⊢ False

Tactic:
rw [show (p : 𝓞 K) * x = (p : ℤ) • x by simp, ← pB.basis.coord_apply,
  LinearMap.map_smul, ← zsmul_one, ← pB.basis.coord_apply, LinearMap.map_smul,
  show 1 = pB.gen ^ (⟨0, by omega⟩ : Fin pB.dim).1 by simp, ← pB.basis_eq_pow,
  pB.basis.coord_apply, pB.basis.coord_apply, pB.basis.repr_self_apply] at h

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
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h : 1 = ↑↑p • (pB.basis.repr x) ⟨1, hdim⟩ + n • if ⟨0, ⋯⟩ = ⟨1, hdim⟩ then 1 else 0
⊢ False

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
n : ℤ
x : 𝓞 K
h : hζ.toInteger - ↑n = ↑↑p * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
hdim : pB.dim = ↑p ^ k * (↑p - 1)
hk : k = 0
⊢ 1 < ↑p ^ k * (↑p - 1)

Tactic:
simp only [hk, zero_add, pow_one, pow_zero, one_mul, Nat.lt_sub_iff_add_lt,
  Nat.reduceAdd] at 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))
n : ℤ
x : 𝓞 K
h : hζ.toInteger - ↑n = ↑↑p * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
hdim : pB.dim = ↑p ^ k * (↑p - 1)
hk : k = 0
htwo : p ≠ 2
⊢ 2 < ↑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
n : ℤ
x : 𝓞 K
h : hζ.toInteger - ↑n = ↑↑p * x
⊢ False

Tactic:
let pB := hζ.integralPowerBasis

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
n : ℤ
x : 𝓞 K
h : hζ.toInteger - ↑n = ↑↑p * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
⊢ False

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
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h : 1 = ↑↑p * (pB.basis.repr x) ⟨1, hdim⟩
⊢ Nat.Prime (↑↑p).natAbs

Tactic:
simp [hp.1]

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
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
hdim : 1 < pB.dim
this : pB.gen = hζ.toInteger
h : 1 = (pB.basis.repr (↑↑p * x)) ⟨1, hdim⟩ + (pB.basis.repr ↑n) ⟨1, hdim⟩
⊢ ↑↑p * x = ↑↑p • x

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
⊢ ¬∃ n, ↑↑p ∣ hζ.toInteger - ↑n

Tactic:
intro ⟨n, x, h⟩

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
n : ℤ
x : 𝓞 K
h : hζ.toInteger - ↑n = ↑↑p * x
⊢ False

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
n : ℤ
x : 𝓞 K
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis
hdim : 1 < pB.dim
h : (pB.basis.repr pB.gen) ⟨1, hdim⟩ = (pB.basis.repr (↑↑p * x + ↑n)) ⟨1, hdim⟩
this : pB.gen = hζ.toInteger
⊢ pB.gen = pB.gen ^ ↑⟨1, hdim⟩

Tactic:
simp

Result:
no goals