simp only [Int.cast_add, Int.cast_pow, ZMod.pow_card, habs,
  ZMod.intCast_zmod_eq_zero_iff_dvd] at H
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
H : (fun x => ↑x) (z ^ ↑p) = (fun x => ↑x) (x ^ ↑p + y ^ ↑p)
⊢ False
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
H : ↑↑p ∣ z
⊢ False