internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.CaseI.auxf0k₁
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
⊢ f0k₁ b p ↑⟨2, ⋯⟩ = 0
Tactic:
have hpred : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ p.pred := by
  intro h
  simp only [Fin.ext_iff, Fin.val_mk] at h
  replace h := h.symm
  rw [Nat.pred_eq_sub_one] at h
  omega
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
⊢ f0k₁ b p ↑⟨2, ⋯⟩ = 0
Theorem: FltRegular.CaseI.auxf0k₁
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
⊢ f0k₁ b p ↑⟨2, ⋯⟩ = 0
Tactic:
simp only [f0k₁, OfNat.ofNat_ne_one, ite_false, ite_eq_right_iff, neg_eq_zero]
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
⊢ 2 = p.pred → b = 0
Theorem: FltRegular.CaseI.auxf0k₁
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
⊢ 2 = p.pred → b = 0
Tactic:
intro h2
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
h2 : 2 = p.pred
⊢ b = 0
Theorem: FltRegular.CaseI.auxf0k₁
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
h2 : 2 = p.pred
⊢ b = 0
Tactic:
exfalso
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
h2 : 2 = p.pred
⊢ False
Theorem: FltRegular.CaseI.auxf0k₁
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
h2 : 2 = p.pred
⊢ False
Tactic:
apply hpred
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
h2 : 2 = p.pred
⊢ ↑⟨2, ⋯⟩ = p.pred
Theorem: FltRegular.CaseI.auxf0k₁
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
h2 : 2 = p.pred
⊢ ↑⟨2, ⋯⟩ = p.pred
Tactic:
simp [h2]
Proof state after:
no goals
Theorem: FltRegular.CaseI.auxf0k₁
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
⊢ ↑⟨2, ⋯⟩ ≠ p.pred
Tactic:
intro h
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
h : ↑⟨2, ⋯⟩ = p.pred
⊢ False
Theorem: FltRegular.CaseI.auxf0k₁
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
h : ↑⟨2, ⋯⟩ = p.pred
⊢ False
Tactic:
simp only [Fin.ext_iff, Fin.val_mk] at h
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
h : 2 = p.pred
⊢ False
Theorem: FltRegular.CaseI.auxf0k₁
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
h : 2 = p.pred
⊢ False
Tactic:
replace h := h.symm
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
h : p.pred = 2
⊢ False
Theorem: FltRegular.CaseI.auxf0k₁
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
h : p.pred = 2
⊢ False
Tactic:
rw [Nat.pred_eq_sub_one] at h
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
h : p - 1 = 2
⊢ False
Theorem: FltRegular.CaseI.auxf0k₁
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
h : p - 1 = 2
⊢ False
Tactic:
omega
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
⊢ 0 ≠ ↑k₁
Tactic:
symm
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
⊢ ↑k₁ ≠ 0
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
⊢ ↑k₁ ≠ 0
Tactic:
intro habs
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : ↑k₁ = 0
⊢ False
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : ↑k₁ = 0
⊢ False
Tactic:
rw [show (k₁ : ℤ) = 0 by simpa using habs, zero_sub] at hcong
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : ↑k₁ = 0
⊢ False
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : ↑k₁ = 0
⊢ False
Tactic:
rw [habs, _root_.pow_zero, mul_one, add_sub_cancel_left, aux_cong0k₁ hpri hcong] at hdiv
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
⊢ False
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
⊢ False
Tactic:
nth_rw 1 [show ζ = ζ ^ ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) by simp] at hdiv
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
⊢ False
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
⊢ False
Tactic:
have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₁ b p j • ζ ^ j := by
  convert hdiv using 1
  have h : 1 ≠ p.pred := fun h => by linarith [pred_eq_succ_iff.1 h.symm]
  simp_rw [f0k₁, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right h,
    Finset.range_filter_eq]
  simp [hpri.one_lt, Nat.sub_lt hpri.pos, sub_eq_add_neg]
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
key : ↑↑p ∣ ∑ j ∈ range p, f0k₁ b p j • ζ ^ j
⊢ False
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
key : ↑↑p ∣ ∑ j ∈ range p, f0k₁ b p j • ζ ^ j
⊢ False
Tactic:
rw [sum_range] at key
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
key : ↑↑p ∣ ∑ i : Fin p, f0k₁ b p ↑i • ζ ^ ↑i
⊢ False
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
key : ↑↑p ∣ ∑ i : Fin p, f0k₁ b p ↑i • ζ ^ ↑i
⊢ False
Tactic:
refine' caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_left _ _) _)
Proof state after:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
key : ↑↑p ∣ ∑ i : Fin p, f0k₁ b p ↑i • ζ ^ ↑i
⊢ ↑p ∣ b
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
key : ↑↑p ∣ ∑ i : Fin p, f0k₁ b p ↑i • ζ ^ ↑i
⊢ ↑p ∣ b
Tactic:
replace hpri : (P : ℕ).Prime := hpri
Proof state after:
p : ℕ
hpri✝ : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
key : ↑↑p ∣ ∑ i : Fin p, f0k₁ b p ↑i • ζ ^ ↑i
hpri : (↑⟨p, ⋯⟩).Prime
⊢ ↑p ∣ b
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri✝ : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
key : ↑↑p ∣ ∑ i : Fin p, f0k₁ b p ↑i • ζ ^ ↑i
hpri : (↑⟨p, ⋯⟩).Prime
⊢ ↑p ∣ b
Tactic:
simpa [f0k₁] using dvd_coeff_cycl_integer hpri hζ (auxf0k₁ hpri hp5 b) key ⟨1, hpri.one_lt⟩
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
habs : ↑k₁ = 0
⊢ ↑↑k₁ = 0
Tactic:
simpa using habs
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
⊢ ζ = ζ ^ ↑⟨1, ⋯⟩
Tactic:
simp
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
⊢ ↑↑p ∣ ∑ j ∈ range p, f0k₁ b p j • ζ ^ j
Tactic:
convert hdiv using 1
Proof state after:
case h.e'_4
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
⊢ ∑ j ∈ range p, f0k₁ b p j • ζ ^ j = ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
case h.e'_4
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
⊢ ∑ j ∈ range p, f0k₁ b p j • ζ ^ j = ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
Tactic:
have h : 1 ≠ p.pred := fun h => by linarith [pred_eq_succ_iff.1 h.symm]
Proof state after:
case h.e'_4
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
h : 1 ≠ p.pred
⊢ ∑ j ∈ range p, f0k₁ b p j • ζ ^ j = ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
case h.e'_4
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
h : 1 ≠ p.pred
⊢ ∑ j ∈ range p, f0k₁ b p j • ζ ^ j = ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
Tactic:
simp_rw [f0k₁, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right h,
  Finset.range_filter_eq]
Proof state after:
case h.e'_4
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
h : 1 ≠ p.pred
⊢ ∑ x ∈ if 1 < p then {1} else ∅, b • ζ ^ x +
      (∑ x ∈ if p.pred < p then {p.pred} else ∅, -b • ζ ^ x +
        ∑ x ∈ filter (fun a => a ≠ 1 ∧ a ≠ p.pred) (range p), 0 • ζ ^ x) =
    ↑b * ζ ^ 1 - ↑b * ζ ^ p.pred
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
case h.e'_4
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
h : 1 ≠ p.pred
⊢ ∑ x ∈ if 1 < p then {1} else ∅, b • ζ ^ x +
      (∑ x ∈ if p.pred < p then {p.pred} else ∅, -b • ζ ^ x +
        ∑ x ∈ filter (fun a => a ≠ 1 ∧ a ≠ p.pred) (range p), 0 • ζ ^ x) =
    ↑b * ζ ^ 1 - ↑b * ζ ^ p.pred
Tactic:
simp [hpri.one_lt, Nat.sub_lt hpri.pos, sub_eq_add_neg]
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux0k₁
Proof state before:
p : ℕ
hpri : p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
caseI : ¬↑p ∣ a * b * c
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ -1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑b * ζ ^ ↑⟨1, ⋯⟩ - ↑b * ζ ^ ↑⟨p.pred, ⋯⟩
habs : ↑k₁ = 0
h : 1 = p.pred
⊢ False
Tactic:
linarith [pred_eq_succ_iff.1 h.symm]
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux_cong0k₂
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ k = ⟨1, ⋯⟩
Tactic:
refine' Fin.ext _
Proof state after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ ↑k = ↑⟨1, ⋯⟩
Theorem: FltRegular.CaseI.aux_cong0k₂
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ ↑k = ↑⟨1, ⋯⟩
Tactic:
rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
Proof state after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ (↑↑k).val = ↑⟨1, ⋯⟩
Theorem: FltRegular.CaseI.aux_cong0k₂
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ (↑↑k).val = ↑⟨1, ⋯⟩
Tactic:
suffices ((k : ℤ) : ZMod p).val = 1 by simpa
Proof state after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ (↑↑↑k).val = 1
Theorem: FltRegular.CaseI.aux_cong0k₂
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ (↑↑↑k).val = 1
Tactic:
rw [← ZMod.intCast_eq_intCast_iff] at hcong
Proof state after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑1
⊢ (↑↑↑k).val = 1
Theorem: FltRegular.CaseI.aux_cong0k₂
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑1
⊢ (↑↑↑k).val = 1
Tactic:
rw [hcong, Int.cast_one]
Proof state after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑1
⊢ ZMod.val 1 = 1
Theorem: FltRegular.CaseI.aux_cong0k₂
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑1
⊢ ZMod.val 1 = 1
Tactic:
haveI : Fact p.Prime := ⟨hpri⟩
Proof state after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑1
this : Fact p.Prime
⊢ ZMod.val 1 = 1
Theorem: FltRegular.CaseI.aux_cong0k₂
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑1
this : Fact p.Prime
⊢ ZMod.val 1 = 1
Tactic:
simp [ZMod.val_one]
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux_cong0k₂
Proof state before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
this : (↑↑↑k).val = 1
⊢ (↑↑k).val = ↑⟨1, ⋯⟩
Tactic:
simpa
Proof state after:
no goals
Theorem: FltRegular.CaseI.auxf0k₂
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
⊢ ∃ i, f0k₂ a b ↑i = 0
Tactic:
refine' ⟨⟨2, two_lt hp5⟩, _⟩
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
⊢ f0k₂ a b ↑⟨2, ⋯⟩ = 0
Theorem: FltRegular.CaseI.auxf0k₂
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
⊢ f0k₂ a b ↑⟨2, ⋯⟩ = 0
Tactic:
have h1 : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ 1 := by
  intro h
  simp only [Fin.ext_iff, Fin.val_mk] at h; contradiction
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h1 : ↑⟨2, ⋯⟩ ≠ 1
⊢ f0k₂ a b ↑⟨2, ⋯⟩ = 0
Theorem: FltRegular.CaseI.auxf0k₂
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h1 : ↑⟨2, ⋯⟩ ≠ 1
⊢ f0k₂ a b ↑⟨2, ⋯⟩ = 0
Tactic:
have hzero : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ 0 := by
  intro h
  simp only [Fin.ext_iff, Fin.val_mk] at h
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h1 : ↑⟨2, ⋯⟩ ≠ 1
hzero : ↑⟨2, ⋯⟩ ≠ 0
⊢ f0k₂ a b ↑⟨2, ⋯⟩ = 0
Theorem: FltRegular.CaseI.auxf0k₂
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h1 : ↑⟨2, ⋯⟩ ≠ 1
hzero : ↑⟨2, ⋯⟩ ≠ 0
⊢ f0k₂ a b ↑⟨2, ⋯⟩ = 0
Tactic:
simp only [f0k₂, h1, if_false, hzero, one_lt_two.ne']
Proof state after:
no goals
Theorem: FltRegular.CaseI.auxf0k₂
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
⊢ ↑⟨2, ⋯⟩ ≠ 1
Tactic:
intro h
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h : ↑⟨2, ⋯⟩ = 1
⊢ False
Theorem: FltRegular.CaseI.auxf0k₂
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h : ↑⟨2, ⋯⟩ = 1
⊢ False
Tactic:
simp only [Fin.ext_iff, Fin.val_mk] at h
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h : 2 = 1
⊢ False
Theorem: FltRegular.CaseI.auxf0k₂
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h : 2 = 1
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: FltRegular.CaseI.auxf0k₂
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h1 : ↑⟨2, ⋯⟩ ≠ 1
⊢ ↑⟨2, ⋯⟩ ≠ 0
Tactic:
intro h
Proof state after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h1 : ↑⟨2, ⋯⟩ ≠ 1
h : ↑⟨2, ⋯⟩ = 0
⊢ False
Theorem: FltRegular.CaseI.auxf0k₂
Proof state before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h1 : ↑⟨2, ⋯⟩ ≠ 1
h : ↑⟨2, ⋯⟩ = 0
⊢ False
Tactic:
simp only [Fin.ext_iff, Fin.val_mk] at h
Proof state after:
no goals
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
⊢ 0 ≠ ↑k₂
Tactic:
haveI := (⟨hpri⟩ : Fact (P : ℕ).Prime)
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ 0 ≠ ↑k₂
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ 0 ≠ ↑k₂
Tactic:
symm
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ ↑k₂ ≠ 0
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ ↑k₂ ≠ 0
Tactic:
intro habs
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
⊢ False
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
⊢ False
Tactic:
replace hcong := hcong.symm
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ - 1 ≡ ↑↑k₂ [ZMOD ↑p]
⊢ False
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ - 1 ≡ ↑↑k₂ [ZMOD ↑p]
⊢ False
Tactic:
rw [show (k₂ : ℤ) = 0 by simpa using habs, ← ZMod.intCast_eq_intCast_iff, Int.cast_sub,
  Int.cast_zero, sub_eq_zero, ZMod.intCast_eq_intCast_iff] at hcong
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
⊢ False
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
⊢ False
Tactic:
rw [habs, _root_.pow_zero, mul_one, aux_cong0k₂ hpri hcong, Fin.val_mk, pow_one, add_sub_assoc,
  ← sub_mul, add_sub_right_comm, show ζ = ζ ^ ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) by simp] at hdiv
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
⊢ False
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
⊢ False
Tactic:
have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₂ a b j • ζ ^ j := by
  convert hdiv using 1
  simp_rw [f0k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right zero_ne_one,
    Finset.range_filter_eq]
  simp only [hpri.pos, hpri.one_lt, if_true, zsmul_eq_mul, Int.cast_sub, sum_singleton,
    _root_.pow_zero, mul_one, pow_one, Ne, zero_smul, sum_const_zero, add_zero, Fin.val_mk]
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ j ∈ range p, f0k₂ a b j • ζ ^ j
⊢ False
Theorem: FltRegular.CaseI.aux0k₂
Proof state before:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ j ∈ range p, f0k₂ a b j • ζ ^ j
⊢ False
Tactic:
rw [sum_range] at key
Proof state after:
p : ℕ
hpri : p.Prime
a b : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hζ : IsPrimitiveRoot ζ p
hab : ¬a ≡ b [ZMOD ↑p]
k₁ k₂ : Fin p
hdiv : ↑p ∣ ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
key : ↑↑p ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
⊢ False