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' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
letI : NumberField K := IsCyclotomicExtension.numberField { p } ℚ _
State after:
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
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}

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
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
have : Fact (p : ℕ).Prime := ⟨hp⟩
State after:
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}

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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
obtain ⟨k, H⟩ := unit_inv_conj_is_root_of_unity hζ hpodd hp u
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ∃ k, ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
refine' ⟨k, _⟩
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
Tactic:
rw [← exists_int_sum_eq_zero'_aux, h, ← H, Units.val_mul, mul_assoc, ← mul_sub, _root_.map_mul,
  ← coe_unitGalConj, ← mul_assoc, ← Units.val_mul, inv_mul_self, Units.val_one, one_mul]
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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ↑u * (α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)) ∈ 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
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ↑u * (α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)) ∈ Ideal.span {↑↑p}
Tactic:
exact Ideal.mul_mem_left _ _ (pow_sub_intGalConj_mem hp α)
State after:
no goals