case refine'_1
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
l : ℝ
hl : l < Subadditive.lim h
⊢ ∀ᶠ (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 > Subadditive.lim h
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
⊢ Tendsto (fun n => u n / ↑n) atTop (𝓝 (Subadditive.lim h))
refine' tendsto_order.2 ⟨fun l hl => _, fun L hL => _⟩
no goals
case refine'_1
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
l : ℝ
hl : l < Subadditive.lim h
⊢ ∀ᶠ (b : ℕ) in atTop, l < u b / ↑b
refine' eventually_atTop.2
  ⟨1, fun n hn => hl.trans_le (h.lim_le_div hbdd (zero_lt_one.trans_le hn).ne')⟩
case refine'_2.intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > Subadditive.lim h
n : ℕ
npos : 0 < n
hn : u n / ↑n < L
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L
case refine'_2
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > Subadditive.lim h
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L
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⟩
no goals
case refine'_2.intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > Subadditive.lim h
n : ℕ
npos : 0 < n
hn : u n / ↑n < L
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L
exact h.eventually_div_lt_of_div_lt npos.ne' hn
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
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > Subadditive.lim h
⊢ ∃ n, 0 < n ∧ u n / ↑n < L
rw [Subadditive.lim] at hL
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
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
rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩
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
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
rcases (mem_image _ _ _).1 hx with ⟨n, hn, rfl⟩
no goals
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
exact ⟨n, zero_lt_one.trans_le hn, xL⟩
no goals
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
⊢ Set.Nonempty ((fun n => u n / ↑n) '' Ici 1)
simp