## Stream: new members

### Topic: Lean's way of simple term transformations

#### André Beyer (Jan 21 2021 at 17:00):

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 (Jan 21 2021 at 17:04):

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 (Jan 21 2021 at 17:08):

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 (Jan 21 2021 at 17:44):

@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 (Jan 21 2021 at 17:53):

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 (Jan 21 2021 at 17:54):

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

#### Mario Carneiro (Jan 21 2021 at 17:54):

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 (Jan 21 2021 at 17:56):

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 (Jan 21 2021 at 17:58):

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 (Jan 21 2021 at 19:59):

Looks good, thank you!

Last updated: May 08 2021 at 18:17 UTC