simple yet meaningful examples of using lemmas

Stream: new members

[rzeta0]

I'm trying to come up with simple educational example that uses a lemma.

The following I thought was simple as a first introduction to applying lemmas.

import Mathlib.Tactic

example {n : ℕ} (h: n = 1): n ≠ 5 := by
  apply ne_of_lt
  calc
    n = 1 := by rw [h]
    _ < 5 := by norm_num

However, I just realised that this example feels fake because it is contrived. I don't need to apply the lemma. Comparing numbers with norm_num is sufficient, as the following shows:

example {n : ℕ} (h: n = 1): n ≠ 5 := by
  calc
    n = 1 := by rw [h]
    _ ≠ 5 := by norm_num

Because my knowledge of the lemmas in mathlib is very little, I'm asking for ideas of lemmas and simple theorems they can prove ... but which don't feel fake as educational examples like the one I came up with above.

I'd like the domain to remain about familiar numbers like N or Q or Z, not sets or other objects.

---

A few days ago I did post an example that used Nat.even_or_odd' to show by cases that $n^2+n$ is even, but the resulting code is too large for a first educational "by beginners, for beginners" example.

[Damiano Testa]

You could use

example {n : ℕ} (h : n < 5): n ≠ 5 := by
  apply ne_of_lt h

[rzeta0]

good example - i wish i had thought of it.

[rzeta0]

i'd welcome more examples, so do keep them coming!

[Bjørn Kjos-Hanssen]

This one I feel like I have proved many times:

import Mathlib

example {n : ℕ} (h : n < 2): n = 0 ∨ n = 1 := by
  have : n ≤ 1 := Nat.le_of_lt_succ h
  exact Nat.le_one_iff_eq_zero_or_eq_one.mp this

[Damiano Testa]

Any lemma "converts" its hypotheses to its conclusion, so you can play this game a lot. Given that there are over 150k lemmas in mathlib, there are lots of possibilities for this!

[rzeta0]

Damiano Testa said:

You could use

example {n : ℕ} (h : n < 5): n ≠ 5 := by
  apply ne_of_lt h

The following code seems "too short" that it makes me suspicious that it is wrong. Is the program valid and of "good enough" style?

example {n : ℕ} (h: n < 5): n ≠ 5 := by
  apply ne_of_lt
  apply h

[Damiano Testa]

It depends on what you mean by "style": if I were writing for Mathlib, I would use h.ne (untested), but for teaching I would use one of the two tactic forms that you have, at least initially.