Theorem: seq_limit_id (LeanTeaching/TutoLib.lean)

State before:
⊢ tendsto_infinity fun n => ↑n
Tactic:
intros A
State after:
A : ℝ
⊢ ∃ N, ∀ n ≥ N, (fun n => ↑n) n ≥ A

State before:
A : ℝ
⊢ ∃ N, ∀ n ≥ N, (fun n => ↑n) n ≥ A
Tactic:
cases' exists_nat_gt A with N hN
State after:
case intro
A : ℝ
N : ℕ
hN : A < ↑N
⊢ ∃ N, ∀ n ≥ N, (fun n => ↑n) n ≥ A

State before:
case intro
A : ℝ
N : ℕ
hN : A < ↑N
⊢ ∃ N, ∀ n ≥ N, (fun n => ↑n) n ≥ A
Tactic:
use N
State after:
case h
A : ℝ
N : ℕ
hN : A < ↑N
⊢ ∀ n ≥ N, (fun n => ↑n) n ≥ A

State before:
case h
A : ℝ
N : ℕ
hN : A < ↑N
⊢ ∀ n ≥ N, (fun n => ↑n) n ≥ A
Tactic:
intros n hn
State after:
case h
A : ℝ
N : ℕ
hN : A < ↑N
n : ℕ
hn : n ≥ N
⊢ (fun n => ↑n) n ≥ A

State before:
case h
A : ℝ
N : ℕ
hN : A < ↑N
n : ℕ
hn : n ≥ N
⊢ (fun n => ↑n) n ≥ A
Tactic:
have : (n : ℝ) ≥ N := by exact_mod_cast hn
State after:
case h
A : ℝ
N : ℕ
hN : A < ↑N
n : ℕ
hn : n ≥ N
this : ↑n ≥ ↑N
⊢ (fun n => ↑n) n ≥ A

State before:
case h
A : ℝ
N : ℕ
hN : A < ↑N
n : ℕ
hn : n ≥ N
this : ↑n ≥ ↑N
⊢ (fun n => ↑n) n ≥ A
Tactic:
linarith
State after:
no goals

State before:
A : ℝ
N : ℕ
hN : A < ↑N
n : ℕ
hn : n ≥ N
⊢ ↑n ≥ ↑N
Tactic:
exact_mod_cast hn
State after:
no goals