α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => r * f x) l atTop
refine' tendsto_atTop.2 fun b => _
case intro
α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
case intro
α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
case intro
α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
rw [nsmul_eq_mul'] at hn
case h
α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ b ≤ r * f x
case intro
α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
⊢ ∀ᶠ (a : α) in l, b ≤ r * f a
filter_upwards [tendsto_atTop.1 hf (n * max b 0)]with x hx
no goals
case h
α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ b ≤ r * f x
calc
  b ≤ 1 * max b 0 := by
  { rw [one_mul]
    exact le_max_left _ _ }
  _ ≤ r * n * max b 0 := by gcongr
  _ = r * (n * max b 0) := by rw [mul_assoc]
  _ ≤ r * f x := by gcongr
no goals
α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ 1 * max b 0 ≤ r * ↑n * max b 0
gcongr
no goals
α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ r * ↑n * max b 0 = r * (↑n * max b 0)
rw [mul_assoc]
no goals
α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedSemiring R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ r * (↑n * max b 0) ≤ r * f x
gcongr