no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.214045
ι : Sort x
inst✝ : OrderedSemiring β
l : Filter α
f g : α → β
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
⊢ 0 ≤ᶠ[l] f * g
filter_upwards [hf, hg] with x using _root_.mul_nonneg