-- Mathlib/Analysis/Subadditive.lean
theorem tendsto_lim (hbdd : BddBelow (range fun n => u n / n)) :
    Tendsto (fun n => u n / n) atTop (𝓝 h.lim)

Proof state:
case refine_2.intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > h.lim
n : ℕ
npos : 0 < n
hn : u n / ↑n < L
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L

Tactic:
exact h.eventually_div_lt_of_div_lt npos.ne' hn

Result:
no goals

Proof state:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
⊢ ((fun n => u n / ↑n) '' Ici 1).Nonempty

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
n : ℕ
hn : n ∈ Ici 1
hx : u n / ↑n ∈ (fun n => u n / ↑n) '' Ici 1
xL : u n / ↑n < L
⊢ ∃ n, 0 < n ∧ u n / ↑n < L

Tactic:
exact ⟨n, zero_lt_one.trans_le hn, xL⟩

Result:
no goals

Proof state:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > h.lim
⊢ ∃ n, 0 < n ∧ u n / ↑n < L

Tactic:
rw [Subadditive.lim] at hL

Result:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
⊢ ∃ n, 0 < n ∧ u n / ↑n < L

Proof state:
case intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
x : ℝ
hx : x ∈ (fun n => u n / ↑n) '' Ici 1
xL : x < L
⊢ ∃ n, 0 < n ∧ u n / ↑n < L

Tactic:
rcases (mem_image _ _ _).1 hx with ⟨n, hn, rfl⟩

Result:
case intro.intro.intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
n : ℕ
hn : n ∈ Ici 1
hx : u n / ↑n ∈ (fun n => u n / ↑n) '' Ici 1
xL : u n / ↑n < L
⊢ ∃ n, 0 < n ∧ u n / ↑n < L

Proof state:
case refine_2
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L

Tactic:
obtain ⟨n, npos, hn⟩ : ∃ n : ℕ, 0 < n ∧ u n / n < L := by
  rw [Subadditive.lim] at hL
  rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩
  rcases (mem_image _ _ _).1 hx with ⟨n, hn, rfl⟩
  exact ⟨n, zero_lt_one.trans_le hn, xL⟩

Result:
case refine_2.intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > h.lim
n : ℕ
npos : 0 < n
hn : u n / ↑n < L
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L

Proof state:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
⊢ ∃ n, 0 < n ∧ u n / ↑n < L

Tactic:
rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩

Result:
case intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
x : ℝ
hx : x ∈ (fun n => u n / ↑n) '' Ici 1
xL : x < L
⊢ ∃ n, 0 < n ∧ u n / ↑n < L

Proof state:
case refine_1
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
l : ℝ
hl : l < h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, l < u b / ↑b

Tactic:
refine eventually_atTop.2
  ⟨1, fun n hn => hl.trans_le (h.lim_le_div hbdd (zero_lt_one.trans_le hn).ne')⟩

Result:
no goals

Proof state:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
⊢ Tendsto (fun n => u n / ↑n) atTop (𝓝 h.lim)

Tactic:
refine tendsto_order.2 ⟨fun l hl => ?_, fun L hL => ?_⟩

Result:
case refine_1
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
l : ℝ
hl : l < h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, l < u b / ↑b

case refine_2
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > h.lim
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L