Theorem: two_not_cube (Flt/Primes.lean)

State before:
r : ℕ
⊢ r ^ 3 ≠ 2
Tactic:
have : 1 ≤ 3 := by norm_num
State after:
r : ℕ
this : 1 ≤ 3
⊢ r ^ 3 ≠ 2

State before:
r : ℕ
this : 1 ≤ 3
⊢ r ^ 3 ≠ 2
Tactic:
apply Monotone.ne_of_lt_of_lt_nat (Nat.pow_left_strictMono this).monotone 1 <;> norm_num
State after:
no goals

State before:
r : ℕ
⊢ 1 ≤ 3
Tactic:
norm_num
State after:
no goals