simp only [mem_insert, mem_singleton] at hx
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
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
x : ℤ
hx : x ∈ {a, b, c}
⊢ ↑q ∣ id x
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
haq : ↑q ∣ a
hbq : ↑q ∣ b
hcq : ↑q ∣ c
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ ↑q ∣ id x