obtain ⟨d, rfl⟩ : a ∣ c :=
  by
  rw [← Int.pow_dvd_pow_iff (by norm_num : 3 ≠ 0), ← h]
  apply dvd_mul_right
a c : ℤ
ha : a ≠ 0
h : a ^ 3 * 2 = c ^ 3
⊢ False
case intro
a : ℤ
ha : a ≠ 0
d : ℤ
h : a ^ 3 * 2 = (a * d) ^ 3
⊢ False