Case I easier

theorem caseI_easier {a b c : ℤ} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p)    (hgcd : ({a, b, c} : Finset ℤ).gcd id = 1) (hab : ¬a ≡ b [ZMOD p])    (caseI : ¬↑p ∣ a * b * c) :    a ^ p + b ^ p ≠ c ^ p := by  set ζ := zeta p ℤ R  have hζ := zeta_spec p ℤ R  intro H  obtain ⟨k₁, k₂, hcong, hdiv⟩ := ex_fin_div hp5 hreg hζ hgcd caseI H  have key : ↑(p : ℤ) ∣ ∑ j ∈ range p, f a b k₁ k₂ j • ζ ^ j := by    convert! hdiv using 1    have h01 : 0 ≠ 1 := zero_ne_one    have h0k₁ := aux0k₁ hpri.out hp5 hζ caseI hcong hdiv    have h0k₂ := aux0k₂ hpri.out hp5 hζ hab hcong hdiv    have h1k₁ := aux1k₁ hpri.out hp5 hζ hab hcong hdiv    have h1k₂ := aux1k₂ hpri.out hp5 hζ caseI hcong hdiv    have hk₁k₂ : (k₁ : ℕ) ≠ (k₂ : ℕ) := auxk₁k₂ hpri.out hcong    simp_rw [f, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right h01, and_assoc,      ne_and_eq_iff_right h1k₁, ne_and_eq_iff_right h0k₁, ne_and_eq_iff_right hk₁k₂,      ne_and_eq_iff_right h1k₂, ne_and_eq_iff_right h0k₂, Finset.range_filter_eq]    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]    ring  rw [sum_range] at key  refine caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_right ?_ _) _)  exact dvd_coeff_cycl_integer hpri.out hζ (auxf hp5 a b k₁ k₂) key    ⟨0, hpri.out.pos⟩