soln feedback - show there exists odd integer m ≥ integer n

Stream: new members

[rzeta0]

This is an interesting exercise from Heather Macbeths' course:

Let  $n$ be an integer. Show that there exists an integer $m \ge n$  which is odd.

The proof is started as follows:

example (n : ℤ) : ∃ m ≥ n, Odd m := by
  sorry

I thought about choosing one single expression which was always guaranteed to be both odd and grater than $n$, something like $2n^2+1$.

But then I thought why not challenge myself and do a slightly more complex proof of which splits the cases as:

• case one: $n$ is even, show there exists an odd $m \ge n$. Try $m=n+1$.
• case two: $n$ is odd, show there exists an odd $m \ge n$. Try $m=n$

For some reason I find it painful in Lean to prove $n^2 \ge n$ for integer $n$.

I came up with the following, which seems far too complex! I spent an hour trying to simplify it and I can't.

I'd welcome specific or general feedback.

One question I have is the use a in the inner "scope" which makes me think something has gone wrong.

Note: 'extra` is Heather Macbeth's positivity tactic, not in mathlib sadly (I wish it were).

example (n : ℤ) : ∃ m ≥ n, Odd m := by
  obtain h1 | h2 := Int.even_or_odd n

  -- h1 : Even n
  · obtain ⟨a, ha⟩ := h1
    dsimp [Even, Odd] at *
    use n + 1
    constructor
    · extra
    · use a
      calc
        n + 1 = (2*a) + 1 := by rw [ha]
        _ = 2*a + 1 := by ring

  -- h2: Odd n
  · obtain ⟨b, hb⟩ := h2
    dsimp [Even, Odd] at *
    use n
    constructor
    · extra
    · use b
      calc
        n = 2 * b + 1 := by rw [hb]

Also, I noticed dsimp [] at * at the top doesn't seem to work and needs repeating inside the "scopes". Is this cause for concern?

[Mario Carneiro]

in the second case, can't you just use n as the witness?

[Mario Carneiro]

there is no need to dsimp [Odd] in this case

[Mario Carneiro]

or pattern match on h2

[Mauricio Collares]

import Mathlib.Algebra.Ring.Int

example (n : ℤ) : ∃ m ≥ n, Odd m := by
  obtain ⟨k, h1 | h2⟩ := Int.even_or_odd' n

  -- h1 : Even n
  · use n + 1
    constructor
    · exact Int.le.intro 1 rfl
    · rw [h1]
      use k

  -- h2: Odd n
  · use n
    constructor
    · exact Int.le_refl n
    · rw [h2]
      use k

works, not sure if that's what you had in mind (both exact lines are the output of exact?)

[Mauricio Collares]

Regarding your other remark, $n^2 \ge n$ is n.le_self_sq, also found by exact?

[rzeta0]

Thanks Mauricio - I haven't learned about exact nor the ? yet but i appreciate your reply.

[rzeta0]

---

Does no-one think the four uses of use is an indication the proof is twice as complex as it needs to be, because it should only need two witnesses?

[Mario Carneiro]

yes, that's exactly what I said

[Mario Carneiro]

example (n : ℤ) : ∃ m ≥ n, Odd m := by
  obtain h1 | h2 := Int.even_or_odd n
  -- h1 : Even n
  · use n + 1
    constructor
    · exact Int.le.intro 1 rfl
    · exact h1.add_one

  -- h2: Odd n
  · use n

[rzeta0]

Thanks Mario - I will need to think about your example as I haven't yet learned what exact or rfl do yet in the course I'm following.