rcases hx with (H | H | H) <;> simp [H]
case refine'_2
p : ℕ
a b c : ℤ
hpri : p.Prime
hp5 : 5 ≤ p
hprod : a * b * c ≠ 0
h : a ^ p + b ^ p = c ^ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ≡ b [ZMOD ↑p]
x : ℤ
hx : x = a ∨ x = -b ∨ x = -c
⊢ x ∈ {a, -c, -b}
no goals