Theorem: FltRegular.CaseI.exists_int_sum_eq_zero (FltRegular/NumberTheory/Cyclotomic/CaseI.lean)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑(hζ.unit' ^ (2 * k)) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
obtain ⟨k, hk⟩ := exists_int_sum_eq_zero' hζ hpodd hp x y i h
State after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑(hζ.unit' ^ (2 * k)) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}

State before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑(hζ.unit' ^ (2 * k)) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
use k
State after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑(hζ.unit' ^ (2 * ↑k)) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}

State before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑(hζ.unit' ^ (2 * ↑k)) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
convert hk
State after:
case h.e'_4.h.e'_6.h.e'_5.h.e'_3
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ hζ.unit' ^ (2 * ↑k) = (hζ.unit' ^ k) ^ 2

State before:
case h.e'_4.h.e'_6.h.e'_5.h.e'_3
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ hζ.unit' ^ (2 * ↑k) = (hζ.unit' ^ k) ^ 2
Tactic:
rw [mul_comm, zpow_mul, zpow_ofNat]
State after:
case h.e'_4.h.e'_6.h.e'_5.h.e'_3
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ (hζ.unit' ^ ↑k) ^ 2 = (hζ.unit' ^ k) ^ 2

State before:
case h.e'_4.h.e'_6.h.e'_5.h.e'_3
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ (hζ.unit' ^ ↑k) ^ 2 = (hζ.unit' ^ k) ^ 2
Tactic:
rfl
State after:
no goals