Efficiently manipulating inequalities

Stream: new members

[Labyrinth]

Hi, newbie here.

I have the following hypotheses (among others):

hn' : M + ε = l
hl : -ε < u N - l ∧ u N - l < ε

My question is: How do I efficiently obtain a hypothesis of type M < u N?
(my current method is using have a bunch of times with the help of apply? to change the hypothesis into what I want)

[Ruben Van de Velde]

Please show us a #mwe (that's a link), so people can play with the goal directly rather than having to guess what the types are for everything

[Labyrinth]

Oh, right, my apologies.

Here is my full code:

import Mathlib

def seq_limit (u : ℕ → ℝ) (l : ℝ) :=
  ∀ε > 0, ∃N : ℕ, ∀n ≥ N, |u n - l| < ε

theorem ex1 {u l M} (hl : seq_limit u l) (h : ∀n, u n ≤ M) :
  l ≤ M := by
  by_contra hn
  have hn' := lt_of_not_ge hn
  apply exists_pos_add_of_lt' at hn'
  rcases hn' with ⟨ε,⟨hε,hn'⟩⟩
  specialize hl ε hε
  rcases hl with ⟨N,hl⟩
  specialize h N
  specialize hl N (Nat.le_refl N)
  rw [abs_lt] at hl

(I am aware that this is far from perfect code)

[Ruben Van de Velde]

The easy solution seems to be linarith :)

[Ruben Van de Velde]

Alternatively

import Mathlib

def seq_limit (u : ℕ → ℝ) (l : ℝ) :=
  ∀ε > 0, ∃N : ℕ, ∀n ≥ N, |u n - l| < ε

theorem ex1 {u l M} (hl : seq_limit u l) (h : ∀n, u n ≤ M) :
  l ≤ M := by
  by_contra hn
  have hn' := lt_of_not_ge hn
  apply exists_pos_add_of_lt' at hn'
  rcases hn' with ⟨ε,⟨hε,hn'⟩⟩
  specialize hl ε hε
  rcases hl with ⟨N,hl⟩
  specialize h N
  specialize hl N (Nat.le_refl N)
  rw [abs_lt] at hl
  have : M < u N := by
    rw [lt_sub_iff_add_lt', ← hn', add_neg_cancel_right] at hl
    exact hl.1
  exact h.not_gt this

[Labyrinth]

I remember seeing that somewhere, guess I'll have to read up (or get an explanation) on how it works. I tried doing this with gcongr but couldn't get it to work (come to think of it it makes sense it can't do the whole thing though I feel like it should've been able to at least remove -epsilon from both sides)

[Labyrinth]

Ah, that seems like a good way of chaining everything on few lines. Definitely looks better than what I had. Thanks Ruben!