-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
lemma limsup_mul_le (h₁ : 0 ≤ᶠ[f] u) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u)
    (h₃ : 0 ≤ᶠ[f] v) (h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v) :
    limsup (u * v) f ≤ (limsup u f) * limsup v f

Proof state:
ι : Type u_1
f : Filter ι
inst✝ : f.NeBot
u v : ι → ℝ
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => u x * v x
h' : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
⊢ ∀ᶠ (a : ι) in f, u a * v a < c

Tactic:
filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v, h₁, h₃]
  with x x_a x_b u_0 v_0

Result:
case h
ι : Type u_1
f : Filter ι
inst✝ : f.NeBot
u v : ι → ℝ
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => u x * v x
h' : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
x : ι
x_a : u x < a
x_b : v x < b
u_0 : 0 x ≤ u x
v_0 : 0 x ≤ v x
⊢ u x * v x < c

Proof state:
ι : Type u_1
f : Filter ι
inst✝ : f.NeBot
u v : ι → ℝ
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => u x * v x
h' : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
refine le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (limsup_le_iff h h').2 fun c c_ab ↦ ?_

Result:
ι : Type u_1
f : Filter ι
inst✝ : f.NeBot
u v : ι → ℝ
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => u x * v x
h' : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
⊢ ∀ᶠ (a : ι) in f, u a * v a < c

Proof state:
ι : Type u_1
f : Filter ι
inst✝ : f.NeBot
u v : ι → ℝ
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
have h := (isBoundedUnder_of_eventually_ge (a := 0)
  <| (h₁.and h₃).mono fun x ⟨u_0, v_0⟩ ↦ mul_nonneg u_0 v_0).isCoboundedUnder_le

Result:
ι : Type u_1
f : Filter ι
inst✝ : f.NeBot
u v : ι → ℝ
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => u x * v x
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Proof state:
case h
ι : Type u_1
f : Filter ι
inst✝ : f.NeBot
u v : ι → ℝ
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => u x * v x
h' : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
x : ι
x_a : u x < a
x_b : v x < b
u_0 : 0 x ≤ u x
v_0 : 0 x ≤ v x
⊢ u x * v x < c

Tactic:
exact (mul_le_mul x_a.le x_b.le v_0 (u_0.trans x_a.le)).trans_lt c_ab

Result:
no goals

Proof state:
ι : Type u_1
f : Filter ι
inst✝ : f.NeBot
u v : ι → ℝ
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => u x * v x
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
have h' := isBoundedUnder_le_mul_of_nonneg h₁ h₂ h₃ h₄

Result:
ι : Type u_1
f : Filter ι
inst✝ : f.NeBot
u v : ι → ℝ
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => u x * v x
h' : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)
⊢ limsup (u * v) f ≤ limsup u f * limsup v f