Theorem: FltRegular.CaseI.aux0k₂ (FltRegular/CaseI/AuxLemmas.lean)

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)
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₂

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
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

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
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

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
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

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
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

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
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

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]
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

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
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

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 ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
⊢ False
Tactic:
refine' hab _
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
⊢ a ≡ b [ZMOD ↑p]

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 ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
⊢ a ≡ b [ZMOD ↑p]
Tactic:
symm
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
⊢ b ≡ a [ZMOD ↑p]

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 ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
⊢ b ≡ a [ZMOD ↑p]
Tactic:
rw [← ZMod.intCast_eq_intCast_iff, ZMod.intCast_eq_intCast_iff_dvd_sub]
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
⊢ ↑p ∣ a - b

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 ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
⊢ ↑p ∣ a - b
Tactic:
have hpri₁ : (P : ℕ).Prime := hpri
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
hpri₁ : (↑⟨p, ⋯⟩).Prime
⊢ ↑p ∣ a - b

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 ∣ ∑ i : Fin p, f0k₂ a b ↑i • ζ ^ ↑i
hpri₁ : (↑⟨p, ⋯⟩).Prime
⊢ ↑p ∣ a - b
Tactic:
simpa [f0k₂] using dvd_coeff_cycl_integer hpri₁ hζ (auxf0k₂ hpri hp5 a b) key ⟨0, hpri.pos⟩
State after:
no goals

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]
⊢ ↑↑k₂ = 0
Tactic:
simpa using habs
State after:
no goals

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) * ζ
this : Fact (↑⟨p, ⋯⟩).Prime
habs : ↑k₂ = 0
hcong : ↑↑k₁ ≡ 1 [ZMOD ↑p]
⊢ ζ = ζ ^ ↑⟨1, ⋯⟩
Tactic:
simp
State after:
no goals

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]
⊢ ↑↑p ∣ ∑ j ∈ range p, f0k₂ a b j • ζ ^ j
Tactic:
convert hdiv using 1
State after:
case h.e'_4
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]
⊢ ∑ j ∈ range p, f0k₂ a b j • ζ ^ j = ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩

State before:
case h.e'_4
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]
⊢ ∑ j ∈ range p, f0k₂ a b j • ζ ^ j = ↑a - ↑b + (↑b - ↑a) * ζ ^ ↑⟨1, ⋯⟩
Tactic:
simp_rw [f0k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right zero_ne_one,
  Finset.range_filter_eq]
State after:
case h.e'_4
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]
⊢ ∑ x ∈ if 0 < p then {0} else ∅, (a - b) • ζ ^ x +
      (∑ x ∈ if 1 < p then {1} else ∅, (b - a) • ζ ^ x + ∑ x ∈ filter (fun a => a ≠ 0 ∧ a ≠ 1) (range p), 0 • ζ ^ x) =
    ↑a - ↑b + (↑b - ↑a) * ζ ^ 1

State before:
case h.e'_4
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]
⊢ ∑ x ∈ if 0 < p then {0} else ∅, (a - b) • ζ ^ x +
      (∑ x ∈ if 1 < p then {1} else ∅, (b - a) • ζ ^ x + ∑ x ∈ filter (fun a => a ≠ 0 ∧ a ≠ 1) (range p), 0 • ζ ^ x) =
    ↑a - ↑b + (↑b - ↑a) * ζ ^ 1
Tactic:
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]
State after:
no goals