ι : Type ?u.217364
ι' : Type ?u.217367
α : Type u_2
β : Type u_1
γ : Type ?u.217376
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
inst✝ : NeBot l
h : Tendsto f l atTop
hrf : Tendsto (fun x => r * f x) l atTop
hr : r ≤ 0
⊢ False
ι : Type ?u.217364
ι' : Type ?u.217367
α : Type u_2
β : Type u_1
γ : Type ?u.217376
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
inst✝ : NeBot l
h : Tendsto f l atTop
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r
refine' ⟨fun hrf => not_le.mp fun hr => _, fun hr => (tendsto_const_mul_atTop_of_pos hr).mpr h⟩
case intro.intro
ι : Type ?u.217364
ι' : Type ?u.217367
α : Type u_2
β : Type u_1
γ : Type ?u.217376
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
inst✝ : NeBot l
h : Tendsto f l atTop
hrf : Tendsto (fun x => r * f x) l atTop
hr : r ≤ 0
x : β
hx : 0 ≤ f x
hrx : 0 < r * f x
⊢ False
ι : Type ?u.217364
ι' : Type ?u.217367
α : Type u_2
β : Type u_1
γ : Type ?u.217376
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
inst✝ : NeBot l
h : Tendsto f l atTop
hrf : Tendsto (fun x => r * f x) l atTop
hr : r ≤ 0
⊢ False
rcases ((h.eventually_ge_atTop 0).and (hrf.eventually_gt_atTop 0)).exists with ⟨x, hx, hrx⟩
no goals
case intro.intro
ι : Type ?u.217364
ι' : Type ?u.217367
α : Type u_2
β : Type u_1
γ : Type ?u.217376
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
inst✝ : NeBot l
h : Tendsto f l atTop
hrf : Tendsto (fun x => r * f x) l atTop
hr : r ≤ 0
x : β
hx : 0 ≤ f x
hrx : 0 < r * f x
⊢ False
exact (mul_nonpos_of_nonpos_of_nonneg hr hx).not_lt hrx