-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
lemma le_limsup_mul (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 f) * liminf v f ≤ limsup (u * 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)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
x✝ : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
⊢ ∃ᶠ (a : ι) in f, c < u a * v a

Tactic:
refine ((frequently_lt_of_lt_limsup
  (isBoundedUnder_of_eventually_ge h₁).isCoboundedUnder_le au).and_eventually
  ((eventually_lt_of_lt_liminf bv (isBoundedUnder_of_eventually_ge h₃)).and
  (h₁.and h₃))).mono fun x ⟨xa, ⟨xb, u0, _⟩⟩ ↦ ?_

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)
u0✝ : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
x✝¹ : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
x : ι
x✝ : a < u x ∧ b < v x ∧ 0 x ≤ u x ∧ 0 x ≤ v x
xa : a < u x
xb : b < v x
u0 : 0 x ≤ u x
right✝ : 0 x ≤ v x
⊢ c < u x * v x

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)
u0 : 0 ≤ limsup u f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
have uv : 0 ≤ limsup (u * v) f :=
  le_limsup_of_frequently_le ((h₁.and h₃).mono fun _ ⟨hu, hv⟩ ↦ mul_nonneg hu hv).frequently 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)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
⊢ limsup u f * liminf v f ≤ limsup (u * 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)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
refine mul_le_of_forall_lt_of_nonneg u0 uv fun a _ au b b0 bv ↦ (le_limsup_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)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
x✝ : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
⊢ ∃ᶠ (a : ι) in f, c < u a * v a

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)
u0✝ : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
x✝¹ : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
x : ι
x✝ : a < u x ∧ b < v x ∧ 0 x ≤ u x ∧ 0 x ≤ v x
xa : a < u x
xb : b < v x
u0 : 0 x ≤ u x
right✝ : 0 x ≤ v x
⊢ c < u x * v x

Tactic:
exact c_ab.trans_le (mul_le_mul xa.le xb.le b0 u0)

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
⊢ limsup u f * liminf v f ≤ limsup (u * 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 f * liminf v f ≤ limsup (u * 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
⊢ limsup u f * liminf v f ≤ limsup (u * 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 f * liminf v f ≤ limsup (u * 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)
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le h₁.frequently 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)
u0 : 0 ≤ limsup u f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f