intro H
case h
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
⊢ a ^ 3 + b ^ 3 ≠ c ^ 3
case h
a✝ b✝ c✝ : ℤ
ha✝ : a✝ ≠ 0
hb✝ : b✝ ≠ 0
hc✝ : c✝ ≠ 0
x✝ : ℕ
h✝ : Int.natAbs (a✝ * b✝ * c✝) = x✝
k' : ℕ
IH : ∀ (m : ℕ), m < k' → ∀ {a b c : ℤ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → Int.natAbs (a * b * c) = m → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
h : Int.natAbs (a * b * c) = k'
H : a ^ 3 + b ^ 3 = c ^ 3
⊢ False