obtain ⟨q, hqpri, hq⟩ := exists_prime_and_dvd h
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
⊢ 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 : ℕ
hqpri : q.Prime
hq : q ∣ a.gcd b
⊢ False