Theorem: exists_dvd_pow_sub_Int_pow (FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
a : 𝓞 K
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
obtain ⟨ζ, hζ⟩ := IsCyclotomicExtension.exists_prim_root ℚ (B := K) (Set.mem_singleton p)
State after:
case intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p

State before:
case intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
obtain ⟨b, k, e⟩ := exists_zeta_sub_one_dvd_sub_Int hζ a
State after:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p

State before:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
obtain ⟨r, hr⟩ := exists_add_pow_prime_eq hpri.out a (-b)
State after:
case intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (a + -↑b) ^ ↑p = a ^ ↑p + (-↑b) ^ ↑p + ↑↑p * r
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p

State before:
case intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (a + -↑b) ^ ↑p = a ^ ↑p + (-↑b) ^ ↑p + ↑↑p * r
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
obtain ⟨u, hu⟩ := (associated_zeta_sub_one_pow_prime hζ).symm
State after:
case intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (a + -↑b) ^ ↑p = a ^ ↑p + (-↑b) ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p

State before:
case intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (a + -↑b) ^ ↑p = a ^ ↑p + (-↑b) ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
rw [(Nat.Prime.odd_of_ne_two hpri.out (PNat.coe_injective.ne hp)).neg_pow, ← sub_eq_add_neg, e,
  mul_pow, ← sub_eq_add_neg] at hr
State after:
case intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (↑hζ.unit' - 1) ^ ↑p * k ^ ↑p = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p

State before:
case intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (↑hζ.unit' - 1) ^ ↑p * k ^ ↑p = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
nth_rw 1 [← Nat.sub_add_cancel (n := p) (m := 1) hpri.out.one_lt.le] at hr
State after:
case intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (↑hζ.unit' - 1) ^ (↑p - 1 + 1) * k ^ ↑p = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p

State before:
case intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (↑hζ.unit' - 1) ^ (↑p - 1 + 1) * k ^ ↑p = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
rw [pow_succ, ← hu, mul_assoc, mul_assoc] at hr
State after:
case intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
u : (𝓞 K)ˣ
hr : ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p)) = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p

State before:
case intro.intro.intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
u : (𝓞 K)ˣ
hr : ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p)) = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
Tactic:
use b, ↑u * ((hζ.unit' - 1 : 𝓞 K) * k ^ (p : ℕ)) - r
State after:
case h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
u : (𝓞 K)ˣ
hr : ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p)) = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ a ^ ↑p - ↑b ^ ↑p = ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p) - r)

State before:
case h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
b : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
u : (𝓞 K)ˣ
hr : ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p)) = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ a ^ ↑p - ↑b ^ ↑p = ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p) - r)
Tactic:
rw [mul_sub, hr, add_sub_cancel_right]
State after:
no goals