α : 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 ≤ f a * r
α : 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 => f x * r) 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 ≤ f a * r
α : 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 ≤ f a * r
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 ≤ n • r
hn' : 1 ≤ ↑n * r
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r
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 ≤ f a * r
have hn' : 1 ≤ (n : R) * r := by rwa [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 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ f x * r
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
hn' : 1 ≤ ↑n * r
⊢ ∀ᶠ (a : α) in l, b ≤ f a * r
filter_upwards [tendsto_atTop.1 hf (max b 0 * n)]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 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ f x * r
calc
  b ≤ max b 0 * 1 := by
  { rw [mul_one]
    exact le_max_left _ _ }
  _ ≤ max b 0 * (n * r) := by gcongr
  _ = max b 0 * n * r := by rw [mul_assoc]
  _ ≤ f x * r := 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 ≤ n • r
⊢ 1 ≤ ↑n * r
rwa [nsmul_eq_mul] at hn
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 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * 1 ≤ max b 0 * (↑n * r)
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 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * (↑n * r) = max b 0 * ↑n * r
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 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * ↑n * r ≤ f x * r
gcongr