simp [mul_assoc]
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
m : ℤ
hm : b = ↑(a.gcd b) * m
⊢ ↑(q * n) * m = ↑q * (↑n * m)
no goals