Prove by matching specific natural numbers in Lean

Question

I'm trying to prove in Lean 4 that for the naturals: q + q ^ 2 ≠ 7

So far, I have this proof:

example : q + q ^ 2 ≠ 7 := by
  intro h
  have q00 : q = 0 ∨ 0 < q := by exact Nat.eq_zero_or_pos q
  cases q00
  case inl h0 => -- q = 0
    have h' : q + q ^ 2 = 7 := h
    rw [h0] at h'
    norm_num at h'
  case inr hq => -- q ≥ 1 
    have q01 : q = 1 ∨ 2 ≤ q := by exact LE.le.eq_or_gt hq
    cases q01
    case inl q1 => -- q = 1
      have h' : q + q ^ 2 = 7 := h
      rw [q1] at h'
      norm_num at h'
    case inr qge2 => -- q ≥ 2
      have q2or : q = 2 ∨ 3 ≤ q := by exact LE.le.eq_or_gt qge2
      cases q2or
      case inl q2 => -- q = 2
        have h'' : q + q ^ 2 = 7 := h
        rw [q2] at h''
        norm_num at h''
      case inr qge3 => -- q ≥ 3
        have q2ge9 : 9 ≤ q * q := by exact Nat.mul_le_mul qge3 qge3
        rw [← Nat.pow_two] at q2ge9
        linarith only [h, q2ge9]

Two questions:

1. I'd like to implement a simpler pattern matching proof preserving a similar structure. Something like:

example : q + q ^ 2 ≠ 7 := by
  match q with
  | 0 => norm_num
  | 1 => norm_num
  | 2 => norm_num
  | _ =>
    sorry

Maybe it would need the zero and succ q case patterns?

2. The statement is very simple, so I'd like ideas for a simpler proof, even if totally distinct.

Answer 1

In Lean 3 the omega tactic would have done this in one line. This tactic is still being ported to Lean 4 and the last I heard was that we could be hoping to see it early next year. Until then, this works:

import Mathlib.Tactic

example (q : ℕ) : q + q ^ 2 ≠ 7 := by
  match q with
  | 0 => norm_num
  | 1 => norm_num
  | 2 => norm_num
  | (n + 3) =>
    ring_nf -- 12 + 7n + n^2 ≠ 7
    apply ne_of_gt -- 7 < 12 + 7n + n^2
    rw [Nat.add_assoc] -- 7 < 12 + blah
    apply Nat.lt_add_right -- 7 < 12
    linarith

Answer 2

Here's a proof

example (q : ℕ) : q + q ^ 2 ≠ 7 := by
  match q with
  | 0 => norm_num
  | 1 => norm_num
  | 2 => norm_num
  | q+3 =>
    calc (q + 3) + (q + 3) ^ 2 
      = 7 * q + q^2 + 12 := by ring
    _ ≠ 7 := by norm_num

Answer 3

Others have already answered how to do this by cases, but sometimes it's worth stepping back and rethinking the proof strategy. Something I notice is that the left-hand side is always even but 7 is odd. So:

import Mathlib.Data.Nat.Parity

example (q : ℕ) : q + q ^ 2 ≠ 7 := by
  intro h
  replace h := congr(Even $h)
  simp [parity_simps] at h

(This congr(...) syntax is applying Even to both sides of h, yielding Even (q + q ^ 2) = Even 7. There are other ways to do this, like using congr_arg Even h or the tactic apply_fun Even at h, but this is more general and I wanted to show it off.)