obtain ⟨n, hn⟩ := hq
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
case intro.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 : _root_.Prime ↑q
n : ℕ
hn : a.gcd b = q * n
⊢ False