Theorem: tendsto_coe_pnat_atTop (ForML/Dirac.lean)

State before:
⊢ Tendsto (fun n => ↑n) atTop atTop
Tactic:
rw [tendsto_atTop_atTop]
State after:
⊢ ∀ (b : ℕ), ∃ i, ∀ (a : ℕ+), i ≤ a → b ≤ ↑a

State before:
⊢ ∀ (b : ℕ), ∃ i, ∀ (a : ℕ+), i ≤ a → b ≤ ↑a
Tactic:
intro a
State after:
a : ℕ
⊢ ∃ i, ∀ (a_1 : ℕ+), i ≤ a_1 → a ≤ ↑a_1

State before:
a : ℕ
⊢ ∃ i, ∀ (a_1 : ℕ+), i ≤ a_1 → a ≤ ↑a_1
Tactic:
exists Nat.toPNat' a
State after:
a : ℕ
⊢ ∀ (a_1 : ℕ+), Nat.toPNat' a ≤ a_1 → a ≤ ↑a_1

State before:
a : ℕ
⊢ ∀ (a_1 : ℕ+), Nat.toPNat' a ≤ a_1 → a ≤ ↑a_1
Tactic:
intro x hx
State after:
a : ℕ
x : ℕ+
hx : Nat.toPNat' a ≤ x
⊢ a ≤ ↑x

State before:
a : ℕ
x : ℕ+
hx : Nat.toPNat' a ≤ x
⊢ a ≤ ↑x
Tactic:
exact Nat.le_of_pred_lt hx
State after:
no goals