replace h := congr_arg (fun n : ℤ => (n : ZMod p)) h
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
h : a ^ p + b ^ p = c ^ p
hab : a ≡ b [ZMOD ↑p]
hbc : b ≡ -c [ZMOD ↑p]
this : Fact p.Prime := { out := hpri }
⊢ ↑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 : (fun n => ↑n) (a ^ p + b ^ p) = (fun n => ↑n) (c ^ p)
⊢ ↑p ∣ c