have hodd : p ≠ 2 := by
  intro h
  rw [h] at H hI
  refine' hI _
  refine' Dvd.dvd.mul_left _ _
  simp only [Nat.cast_ofNat] at hI ⊢
  rw [← even_iff_two_dvd, ← Int.odd_iff_not_even] at hI
  rw [← even_iff_two_dvd, ← Int.even_pow' (show 2 ≠ 0 by norm_num), ← H]
  exact (Int.Odd.of_mul_left (Odd.of_mul_left hI)).pow.add_odd
    (Int.Odd.of_mul_right (Odd.of_mul_left hI)).pow
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
⊢ False
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
⊢ False