case inl
ι : Type ?u.233433
ι' : Type ?u.233436
α : Type u_2
β : Type u_1
γ : Type ?u.233445
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
hr : r < 0
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

case inr.inl
ι : Type ?u.233433
ι' : Type ?u.233436
α : Type u_2
β : Type u_1
γ : Type ?u.233445
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
inst✝ : NeBot l
⊢ Tendsto (fun x => 0 * f x) l atTop ↔ 0 < 0 ∧ Tendsto f l atTop ∨ 0 < 0 ∧ Tendsto f l atBot

case inr.inr
ι : Type ?u.233433
ι' : Type ?u.233436
α : Type u_2
β : Type u_1
γ : Type ?u.233445
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
hr : 0 < r
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
ι : Type ?u.233433
ι' : Type ?u.233436
α : Type u_2
β : Type u_1
γ : Type ?u.233445
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
rcases lt_trichotomy r 0 with (hr | rfl | hr)
no goals
case inl
ι : Type ?u.233433
ι' : Type ?u.233436
α : Type u_2
β : Type u_1
γ : Type ?u.233445
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
hr : r < 0
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
simp [hr, hr.not_lt, tendsto_const_mul_atTop_of_neg]
no goals
case inr.inl
ι : Type ?u.233433
ι' : Type ?u.233436
α : Type u_2
β : Type u_1
γ : Type ?u.233445
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
inst✝ : NeBot l
⊢ Tendsto (fun x => 0 * f x) l atTop ↔ 0 < 0 ∧ Tendsto f l atTop ∨ 0 < 0 ∧ Tendsto f l atBot
simp [not_tendsto_const_atTop]
no goals
case inr.inr
ι : Type ?u.233433
ι' : Type ?u.233436
α : Type u_2
β : Type u_1
γ : Type ?u.233445
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
hr : 0 < r
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
simp [hr, hr.not_lt, tendsto_const_mul_atTop_of_pos]