-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
lemma liminf_mul_le (h₁ : 0 ≤ᶠ[f] u) (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u)
    (h₃ : 0 ≤ᶠ[f] v) (h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v) :
    liminf (u * v) f ≤ (limsup u f) * liminf 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₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f fun x => u x * v x
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > liminf v f
c : ℝ
c_ab : c > a * b
x : ι
x✝ : v x < b ∧ u x < a ∧ 0 x ≤ u x ∧ 0 x ≤ v x
x_v : v x < b
x_u : u x < a
u_0 : 0 x ≤ u x
v_0 : 0 x ≤ v x
⊢ (u * v) x < c

Tactic:
exact (mul_le_mul x_u.le x_v.le v_0 (u_0.trans x_u.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₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f fun x => u x * v x
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Tactic:
refine le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (liminf_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₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f fun x => u x * v x
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > liminf v f
c : ℝ
c_ab : c > a * b
⊢ ∃ᶠ (a : ι) in f, (u * 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₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)
⊢ liminf (u * v) f ≤ limsup u f * liminf 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

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₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f fun x => u x * v x
⊢ liminf (u * v) f ≤ limsup u f * liminf 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₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Tactic:
have h := isCoboundedUnder_ge_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₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)
⊢ liminf (u * v) f ≤ limsup u f * liminf 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₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f fun x => u x * v x
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > liminf v f
c : ℝ
c_ab : c > a * b
⊢ ∃ᶠ (a : ι) in f, (u * v) a < c

Tactic:
refine ((frequently_lt_of_liminf_lt h₄ b_v).and_eventually ((eventually_lt_of_limsup_lt a_u).and
  (h₁.and h₃))).mono fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_

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₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f fun x => u x * v x
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > liminf v f
c : ℝ
c_ab : c > a * b
x : ι
x✝ : v x < b ∧ u x < a ∧ 0 x ≤ u x ∧ 0 x ≤ v x
x_v : v x < b
x_u : u x < a
u_0 : 0 x ≤ u x
v_0 : 0 x ≤ v x
⊢ (u * v) x < c