Theorem: Int.two_not_cube (FltRegular/FltThree/Primes.lean)

State before:
r : ℤ
⊢ r ^ 3 ≠ 2
Tactic:
intro H
State after:
r : ℤ
H : r ^ 3 = 2
⊢ False

State before:
r : ℤ
H : r ^ 3 = 2
⊢ False
Tactic:
apply two_not_cube r.natAbs
State after:
r : ℤ
H : r ^ 3 = 2
⊢ r.natAbs ^ 3 = 2

State before:
r : ℤ
H : r ^ 3 = 2
⊢ r.natAbs ^ 3 = 2
Tactic:
rw [← Int.natAbs_pow, H]
State after:
r : ℤ
H : r ^ 3 = 2
⊢ natAbs 2 = 2

State before:
r : ℤ
H : r ^ 3 = 2
⊢ natAbs 2 = 2
Tactic:
norm_num
State after:
no goals