simp only [hpri.out.pos, hpri.out.one_lt, if_true, zsmul_eq_mul, sum_singleton, _root_.pow_zero,
  mul_one, pow_one, Fin.is_lt, neg_smul, sum_neg_distrib, Ne, zero_smul, sum_const_zero,
  add_zero]
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
h1k₁ : 1 ≠ ↑k₁
h1k₂ : 1 ≠ ↑k₂
hk₁k₂ : ↑k₁ ≠ ↑k₂
⊢ ∑ x ∈ if 0 < p then {0} else ∅, a • ζ ^ x +
      (∑ x ∈ if 1 < p then {1} else ∅, b • ζ ^ x +
        (∑ x ∈ if ↑k₁ < p then {↑k₁} else ∅, -a • ζ ^ x +
          (∑ x ∈ if ↑k₂ < p then {↑k₂} else ∅, -b • ζ ^ x +
            ∑ x ∈ filter (fun a => a ≠ 0 ∧ a ≠ 1 ∧ a ≠ ↑k₁ ∧ a ≠ ↑k₂) (range p), 0 • ζ ^ x))) =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
case h.e'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
h01 : 0 ≠ 1
h0k₁ : 0 ≠ ↑k₁
h0k₂ : 0 ≠ ↑k₂
h1k₁ : 1 ≠ ↑k₁
h1k₂ : 1 ≠ ↑k₂
hk₁k₂ : ↑k₁ ≠ ↑k₂
⊢ ↑a + (↑b * ζ + (-(↑a * ζ ^ ↑k₁) + -(↑b * ζ ^ ↑k₂))) =
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂