replace hqpri : Prime (q : ℤ) := prime_iff_natAbs_prime.2 (by simp [hqpri])
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hqpri : q.Prime
hq : q ∣ a.gcd b
⊢ False
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
H : a ^ p + b ^ p = c ^ p
hpzero : p ≠ 0
hgcd : {a, b, c}.gcd id = 1
h : a.gcd b ≠ 1
q : ℕ
hq : q ∣ a.gcd b
hqpri : _root_.Prime ↑q
⊢ False