question about Ico

Stream: mathlib4

[Gaolei He]

In Lean4 language, we have the condition that

(n m x : ℕ) x ∈ Ico (m + 1 + 1) (n + 1 + 1)

how do we prove that

1 ≤ x

[Ruben Van de Velde]

Try providing a #mwe

[Gaolei He]

Here's my code

import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Choose.Sum

open Finset Nat
theorem f (n m x : ℕ) (hx : x ∈ Ico (m + 1) (n + 1)) : 1 ≤ x := by

  sorry

[Jireh Loreaux]

import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Choose.Sum

open Finset Nat
theorem f (n m x : ℕ) (hx : x ∈ Ico (m + 1) (n + 1)) : 1 ≤ x :=
  m.zero_lt_succ.trans_le (mem_Ico.mp hx).1

[Jireh Loreaux]

m.zero_lt_succ says that 0 < m.succ (i.e., 0 < m + 1). and (mem_Ico.mp hx).1 says m+1 ≤ x. We chain these inequalities together with docs#LT.lt.trans_le to get 0 < x, and because, for natural numbers, a b : ℕ, a < b is defined as a + 1 ≤ b, this shows 1 ≤ x.

[Ruben Van de Velde]

That's a bit naughty

[Jireh Loreaux]

Here's a non-naughty proof, which is perhaps more beginner friendly:

import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Choose.Sum

open Finset Nat
theorem f (n m x : ℕ) (hx : x ∈ Ico (m + 1) (n + 1)) : 1 ≤ x := by
  apply Nat.succ_le_of_lt
  rw [mem_Ico] at hx
  calc
    0 < m + 1 := m.zero_lt_succ
    _ ≤ x := hx.1

[Ruben Van de Velde]

Or also:

import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Choose.Sum

open Finset Nat
theorem f (n m x : ℕ) (hx : x ∈ Ico (m + 1) (n + 1)) : 1 ≤ x :=
  le_of_add_le_right (mem_Ico.mp hx).1

[Jireh Loreaux]

yes, I also had: Nat.le_add_left 1 m |>.trans (mem_Ico.mp hx).1

[Ruben Van de Velde]

Or how I got there:

import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Choose.Sum

-- all found by `apply?`
example (a b c : ℕ) (h : a + b ≤ c) : a ≤ c := by exact Nat.le_of_add_right_le h
example (a b c : ℕ) (h : a + b ≤ c) : b ≤ c := by exact le_of_add_le_right h
example {α : Type*} [CanonicallyOrderedAddCommMonoid α] (a b c : α) (h : a + b ≤ c) : a ≤ c := by exact le_of_add_le_left h
example {α : Type*} [CanonicallyOrderedAddCommMonoid α] (a b c : α) (h : a + b ≤ c) : b ≤ c := by exact le_of_add_le_right h

[Gaolei He]

Jireh Loreaux said:

Here's a non-naughty proof, which is perhaps more beginner friendly:

import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Choose.Sum

open Finset Nat
theorem f (n m x : ℕ) (hx : x ∈ Ico (m + 1) (n + 1)) : 1 ≤ x := by
  apply Nat.succ_le_of_lt
  rw [mem_Ico] at hx
  calc
    0 < m + 1 := m.zero_lt_succ
    _ ≤ x := hx.1

worked fine for me, a beginner friendly answer

[Notification Bot]

Gaolei He has marked this topic as resolved.

[Notification Bot]

Gaolei He has marked this topic as unresolved.

[Gaolei He]

I want to know that this is correct or not?
If true, how to prove it?

import Mathlib.Data.Nat.Choose.Basic
theorem h (x : ℕ) : x - 1 + 1 = x := by

  sorry

[Daniel Weber]

This isn't always true, as 0 - 1 + 1 = 0 + 1 = 1 ≠ 0, but see docs#Nat.sub_add_cancel

[Gaolei He]

It seems that lean4 defines 0 - 1 = 0
I found this theorem in docs#Nat.zero_sub

[Etienne Marion]

The substraction of two nat has to be a nat, so it is truncated at 0, ie if a <= b then a-b=0