-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
lemma le_liminf_mul (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 f) * liminf v f ≤ liminf (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₄ : 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 f * liminf v f ≤ liminf (u * v) f

Tactic:
apply mul_le_of_forall_lt_of_nonneg (le_liminf_of_le h₂.isCoboundedUnder_ge h₁)
  (le_liminf_of_le h ((h₁.and h₃).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0))

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' ≥ 0, a' < liminf u f → ∀ b' ≥ 0, b' < liminf v f → a' * b' ≤ liminf (u * 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₄ : 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 : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
x : ι
xa : a < u x
xb : b < v x
⊢ c < (u * v) x

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

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

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

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 f * liminf v f ≤ liminf (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₄ : 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 : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
⊢ ∀ᶠ (a : ι) in f, c < (u * v) a

Tactic:
filter_upwards [eventually_lt_of_lt_liminf au (isBoundedUnder_of_eventually_ge h₁),
  eventually_lt_of_lt_liminf bv (isBoundedUnder_of_eventually_ge h₃)] with x xa xb

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₄ : 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 : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
x : ι
xa : a < u x
xb : b < v x
⊢ c < (u * 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₄ : 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' ≥ 0, a' < liminf u f → ∀ b' ≥ 0, b' < liminf v f → a' * b' ≤ liminf (u * v) f

Tactic:
intro a a0 au b b0 bv

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 : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
⊢ a * b ≤ liminf (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₄ : 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 : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
⊢ a * b ≤ liminf (u * v) f

Tactic:
refine (le_liminf_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 : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
⊢ ∀ᶠ (a : ι) in f, c < (u * 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₄ : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v
⊢ liminf u f * liminf v f ≤ liminf (u * 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 f * liminf v f ≤ liminf (u * v) f