Theorem: lim_le (LeanTeaching/TutoLib.lean)

State before:
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
⊢ x ≤ y
Tactic:
apply le_of_le_add_all
State after:
case a
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
⊢ ∀ ε > 0, x ≤ y + ε

State before:
case a
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
⊢ ∀ ε > 0, x ≤ y + ε
Tactic:
intros ε ε_pos
State after:
case a
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
⊢ x ≤ y + ε

State before:
case a
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
⊢ x ≤ y + ε
Tactic:
cases' hu ε ε_pos with N hN
State after:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ ε
⊢ x ≤ y + ε

State before:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ ε
⊢ x ≤ y + ε
Tactic:
specialize hN N (by linarith)
State after:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : |u N - x| ≤ ε
⊢ x ≤ y + ε

State before:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : |u N - x| ≤ ε
⊢ x ≤ y + ε
Tactic:
specialize ineg N
State after:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : |u N - x| ≤ ε
ineg : u N ≤ y
⊢ x ≤ y + ε

State before:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : |u N - x| ≤ ε
ineg : u N ≤ y
⊢ x ≤ y + ε
Tactic:
rw [abs_le] at hN
State after:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : -ε ≤ u N - x ∧ u N - x ≤ ε
ineg : u N ≤ y
⊢ x ≤ y + ε

State before:
case a.intro
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : -ε ≤ u N - x ∧ u N - x ≤ ε
ineg : u N ≤ y
⊢ x ≤ y + ε
Tactic:
linarith
State after:
no goals

State before:
x y : ℝ
u : ℕ → ℝ
hu : seq_limit u x
ineg : ∀ (n : ℕ), u n ≤ y
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ ε
⊢ N ≥ N
Tactic:
linarith
State after:
no goals