to prove n^2<=n^3

Stream: new members

[Zihao Zhang]

import Mathlib

example {n:Nat}:n^2<=n^3:=by
  sorry

Is there a straightforward lemma stating that for natural numbers $a, m, n$ with $m \le n$, we have $a^m \le a^n$?

[Zihao Zhang]

(deleted)

[Michael Rothgang]

My first hint is to switch to integers first:

import Mathlib

example {n:Nat} (hn : 1 < n) : n^2 ≤ n^3 := by
  zify at hn ⊢
  sorry

[Michael Rothgang]

There is such a lemma for integers. If you get stuck trying to find it, please tell us what you tried so we can help you for the future (as opposed to just answering one question).

[Kenny Lau]

@Zihao Zhang _ ^ _ ≤ _ ^ _ on Loogle

[Zihao Zhang]

@Kenny LauI think using _ ^ _ ≤ _ ^ _ is a good way to search for lemmas in Loogle — I mean using this kind of pattern matching.

[Zihao Zhang]

Michael Rothgang said:

There is such a lemma for integers. If you get stuck trying to find it, please tell us what you tried so we can help you for the future (as opposed to just answering one question).

I’m not good at finding existing theorems. Do you know any good methods? Right now, the only tool I know is Loogle.

[Kenny Lau]

I literally just told you how to

[Ruben Van de Velde]

Though there's no need to the extra hypothesis:

example {n:Nat}:n^2<=n^3:=by
  cases n with
  | zero => simp
  | succ n =>
    -- using `apply?`, first result
    refine Nat.pow_le_pow_right ?_ ?_ <;> grind

[Michael Rothgang]

Zihao Zhang said:

I’m not good at finding existing theorems. Do you know any good methods? Right now, the only tool I know is Loogle.
````

I see. So, for the next time: have you tried using loogle? What pattern did you use? What results did you get? (This time, it seems your question has been answered already.)

[Michael Rothgang]

My other advice would be lean on mathlib's tactics more. If a tactic can solve your goal, that's nicer than memorising lemma names. Do you know any tactics that could apply here (e.g., after the zify step)?

[Moritz Doll]

No memorization required

example {n:Nat} : n^2 ≤ n^3 := by
  induction n with
  | zero => simp
  | succ =>
    gcongr
    all_goals
    simp

[Shreyas Srinivas]

import Mathlib

example {n : ℕ}:n^2<=n^3:=by
  cases n with
  | zero =>
      simp
  | succ n =>
      bound

[Michael Rothgang]

I know there are solutions with tactics, I found one myself. I was specifically trying not to just hand out a solution :-)