Lean's way of simple term transformations

Stream: new members

[André Beyer]

Hi!
I'm often struggling with transforming terms from one to another. Here's an example:

h : 0 ≤ (n - 1) ^ 2
⊢ 2 ≤ n + 1 / n

This is easy on paper:

$$0 \le (n - 1)^2 \iff 0 \le n^2 - 2n + 1 \iff 2n \le n^2 + 1 \iff 2 \le n + \frac{1}{n}$$

I don't know how to best archive this using Lean - what are the best practices in such cases? Any suggestions? Thanks in advance!

[Bryan Gin-ge Chen]

I suppose n is a natural number coerced to a rational number? Note that you'll need an additional hypothesis of n \ne 0 since 1/0 is defined to be 0 in mathlib.

[Lars Ericson]

Something like this plus what Bryan just said:

import tactic

theorem ineq_on_n (n: ℕ) : 0 ≤ (n-1)^2 ↔ 2*n ≤ n^2+1 :=
begin
  split,
  {
    intro h,
    refine eq.le _,
    sorry,
  },
  {
    intro h,
    exact zero_le ((n - 1) ^ 2),
  }
end

[Johan Commelin]

@André Beyer Please state problems in the form of

import whatever.you.need

example (n : nat?rat?real?) : etc :=
sorry

See also #mwe <- this is a link

[Mario Carneiro]

Here's a proof along those general lines:

import data.real.basic

example (n : ℝ) (h : n > 0) : 2 ≤ n + 1 / n :=
begin
  refine le_of_mul_le_mul_left _ h,
  simp [mul_add, ne_of_gt h],
  rw ← sub_nonneg,
  convert pow_two_nonneg (n - 1),
  ring,
end

[Mario Carneiro]

the hard part is dealing with the division, as others said

[Mario Carneiro]

for the most part you can just clear denominators, make it a polynomial equation, and let ring take care of the rest

[Bryan Gin-ge Chen]

I was just writing up a very similar proof which uses field_simp instead of the explicit lemma le_of_mul_le_mul_left:

import tactic
import tactic.field_simp

example {n : ℚ} (h : 0 < n) : 2 ≤ n + 1 / n :=
begin
  have H : n*n + 1 - 2*n = (n - 1) * (n - 1) := by ring,
  field_simp [ne_of_gt h],
  rw [le_div_iff h, ← sub_nonneg, H],
  exact mul_self_nonneg _,
end

[Mario Carneiro]

Ah, so that's how you are supposed to use field_simp here. You can also put the ring at the end like this:

example (n : ℝ) (h : n > 0) : 2 ≤ n + 1 / n :=
begin
  field_simp [ne_of_gt h],
  rw [le_div_iff h, ← sub_nonneg],
  convert pow_two_nonneg (n - 1),
  ring,
end

[André Beyer]

Looks good, thank you!