IFF Question

Stream: new members

[Dev-Indra]

Here is the iff lemma I am trying to prove:

lemma another_helper (u v : ℕ) : v ≤ u ↔ v*v ≤ v*u :=
begin
    split,

    induction v with d hd,
    rw mul_zero,
    rw zero_mul,
    simp,

    rw succ_eq_add_one,
    rw mul_add,
    rw mul_one,
    rw mul_comm,
    rw mul_add,
    rw mul_one,
    rw add_mul,
    rw one_mul,


end

I am trying to prove the first goal with induction, but I am stuck after the last line. Can anyone help, or suggest a better way to prove this?

[Kevin Buzzard]

You should use {} brackets to ensure that you only have one goal at all times. Your question is hard for me to understand because your code doesn't compile and I'm not entirely sure which rewrites are supposed to apply to which goals.

[Shing Tak Lam]

There is a lemma in mathlib called mul_le_mul_left, which you can use by importing data.nat.basic. To solve your inductive case here, you can just use

intro h,
apply nat.mul_le_mul_left (succ d) h,

instead of the bunch of rws. Which will close the goal.

Also you don't need induction here, since you don't need the induction hypotheses.

As mul_le_mul_left is already an iff statement, you can pretty much just use it to solve your goal without needing to split it.

A complete proof just using mul_le_mul_left as an iff statement is like this:

lemma another_helper (u v : ℕ) : v ≤ u ↔ v*v ≤ v*u :=
begin
  cases v,
  { split,
    { intro h,
      simp,
    },
    intro, exact zero_le u,
  },
  {
    symmetry,
    apply mul_le_mul_left,
    simp,
  }
end

[Kevin Buzzard]

@Dev-Indra: note the brackets @Shing Tak Lam used!

[Shing Tak Lam]

I've golfed it slightly :) Apparently norm_num is a lot more powerful than I thought.

lemma another_helper (u v : ℕ) : v ≤ u ↔ v*v ≤ v*u :=
begin
  cases v,
  { norm_num },
  norm_num
end

Curiously, just norm_num by itself doesn't work, but using casesthen norm_num does.

[Dev-Indra]

Thanks. @Kevin Buzzard I will take note of the use of {}