replace H := congr_arg (fun x : ℤ => (x : ZMod p)) H.symm
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
x y z : ℤ
H : x ^ ↑p + y ^ ↑p = z ^ ↑p
caseI : ¬↑↑p ∣ x * y * z
habs : ↑x + ↑y = 0
⊢ 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 : (fun x => ↑x) (z ^ ↑p) = (fun x => ↑x) (x ^ ↑p + y ^ ↑p)
⊢ False