specialize hN' N₀ (le_max_right _ _)
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N N' : ℕ
hN' : ∀ n ≥ N', u n ≥ x + 2
N₀ : ℕ := max N N'
hN : |u N₀ - x| ≤ 1
⊢ False
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N N' : ℕ
N₀ : ℕ := max N N'
hN : |u N₀ - x| ≤ 1
hN' : u N₀ ≥ x + 2
⊢ False