Is there a tactic for solving such trivial goals (lean theorem proving)?

Question

I'm a beginner and I'm stuck with the following:

import tactic.linarith
import tactic.suggest

noncomputable theory
open_locale classical

lemma two_ne_four_mul_any (n:ℕ) : 2 ≠ 2 * 2 * n := begin
  cases n,
  linarith,
  rw mul_assoc,
  ???
end

The state is now:

n : ℕ
⊢ 2 ≠ 2 * (2 * n.succ)

and it seams so trivial, that I thought there must be a tactic for solving it. But linarith, ring, simp, trivial don't work.

So, did I miss some important import?

I also tried to solve this using existing lemmas. In a first step I wanted to reach:

n : ℕ
⊢ 1 ≠ 2 * n.succ

in the hope that some higher level tactic would now see that it is true. However, I don't know how to do some operation on both sides of an equation. Shouldn't it be somehow possible to divide both sides by 2?

My plan was to proceed by changing the rhs to 2*(n+1) and 2n+2 and maybe the goal to

⊢ 0 ≠ 2 * n + 1

in the hope of finding applicable lemmas in the library.

Answer 1

linarith knows linear arithmetic, and this is a linear arithmetic goal, but it is obscured by the use of nat.succ. If you rewrite it away then linarith will work.

example (n : ℕ): 2 ≠ 2 * (2 * n.succ) :=
by rw nat.succ_eq_add_one; linarith