Theorem: not_seq_limit_of_tendstoinfinity (LeanTeaching/TutoLib.lean)

State before:
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
⊢ tendsto_infinity u → ∀ (x : ℝ), ¬seq_limit u x
Tactic:
intros lim_infinie x lim_x
State after:
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
⊢ False

State before:
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
⊢ False
Tactic:
cases' lim_x 1 (by linarith) with N hN
State after:
case intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
⊢ False

State before:
case intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
⊢ False
Tactic:
cases' lim_infinie (x+2) with N' hN'
State after:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
N' : ℕ
hN' : ∀ n ≥ N', u n ≥ x + 2
⊢ False

State before:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
N' : ℕ
hN' : ∀ n ≥ N', u n ≥ x + 2
⊢ False
Tactic:
let N₀ := max N N'
State after:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
N' : ℕ
hN' : ∀ n ≥ N', u n ≥ x + 2
N₀ : ℕ := max N N'
⊢ False

State before:
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
N' : ℕ
hN' : ∀ n ≥ N', u n ≥ x + 2
N₀ : ℕ := max N N'
⊢ False
Tactic:
specialize hN N₀ (le_max_left _ _)
State after:
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

State before:
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
Tactic:
specialize hN' N₀ (le_max_right _ _)
State after:
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

State before:
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
Tactic:
rw [abs_le] at hN
State after:
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 : -1 ≤ u N₀ - x ∧ u N₀ - x ≤ 1
hN' : u N₀ ≥ x + 2
⊢ False

State before:
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 : -1 ≤ u N₀ - x ∧ u N₀ - x ≤ 1
hN' : u N₀ ≥ x + 2
⊢ False
Tactic:
linarith
State after:
no goals

State before:
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
⊢ 1 > 0
Tactic:
linarith
State after:
no goals