Theorem: tendsto_coe_atTop (PrimeNumberTheoremAnd/ZetaBounds.lean)

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

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

State before:
b : ℝ
⊢ ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑a
Tactic:
use ⌊b⌋.toNat + 1
State after:
case h
b : ℝ
⊢ ∀ (a : ℕ), ⌊b⌋.toNat + 1 ≤ a → b ≤ ↑a

State before:
case h
b : ℝ
⊢ ∀ (a : ℕ), ⌊b⌋.toNat + 1 ≤ a → b ≤ ↑a
Tactic:
intro a ha
State after:
case h
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
⊢ b ≤ ↑a

State before:
case h
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
⊢ b ≤ ↑a
Tactic:
by_cases a_zero : a = 0
State after:
case pos
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : a = 0
⊢ b ≤ ↑a

case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
⊢ b ≤ ↑a

State before:
case pos
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : a = 0
⊢ b ≤ ↑a
Tactic:
simp [a_zero] at ha
State after:
no goals

State before:
case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
⊢ b ≤ ↑a
Tactic:
by_cases h : ⌊b⌋.toNat < a
State after:
case pos
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : ⌊b⌋.toNat < a
⊢ b ≤ ↑a

case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : ¬⌊b⌋.toNat < a
⊢ b ≤ ↑a

State before:
case pos
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : ⌊b⌋.toNat < a
⊢ b ≤ ↑a
Tactic:
exact (Int.floor_lt.mp <| (Int.toNat_lt' a_zero).mp h).le
State after:
no goals

State before:
case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : ¬⌊b⌋.toNat < a
⊢ b ≤ ↑a
Tactic:
simp only [not_lt] at h
State after:
case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : a ≤ ⌊b⌋.toNat
⊢ b ≤ ↑a

State before:
case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : a ≤ ⌊b⌋.toNat
⊢ b ≤ ↑a
Tactic:
absurd le_trans ha h
State after:
case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : a ≤ ⌊b⌋.toNat
⊢ ¬⌊b⌋.toNat + 1 ≤ ⌊b⌋.toNat

State before:
case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : a ≤ ⌊b⌋.toNat
⊢ ¬⌊b⌋.toNat + 1 ≤ ⌊b⌋.toNat
Tactic:
simp
State after:
no goals