exact caseII hreg hodd hprod' hgcd case e'
case pos
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ↑p ∣ a / d * (b / d) * (c / d)
⊢ False

case neg
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ¬↑p ∣ a / d * (b / d) * (c / d)
⊢ False
case neg
p : ℕ
inst✝ : Fact p.Prime
hreg : IsRegularPrime p
hodd : p ≠ 2
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
e : a ^ p + b ^ p = c ^ p
hprod : a * b * c ≠ 0
e' : (a / {a, b, c}.gcd id) ^ p + (b / {a, b, c}.gcd id) ^ p = (c / {a, b, c}.gcd id) ^ p
hgcd : {a / {a, b, c}.gcd id, b / {a, b, c}.gcd id, c / {a, b, c}.gcd id}.gcd id = 1
hprod' : a / {a, b, c}.gcd id * (b / {a, b, c}.gcd id) * (c / {a, b, c}.gcd id) ≠ 0
d : ℤ := {a, b, c}.gcd id
case : ¬↑p ∣ a / d * (b / d) * (c / d)
⊢ False