simp only [Int.natCast_pow, Int.cast_add, Int.cast_pow, ZMod.pow_card] at h
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
h : (fun n => ↑n) (a ^ p + b ^ p) = (fun n => ↑n) (c ^ p)
⊢ ↑p ∣ c
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
h : ↑a + ↑b = ↑c
⊢ ↑p ∣ c