-- Mathlib/Order/LiminfLimsup.lean
lemma isBoundedUnder_le_mul_of_nonneg [Mul α] [Zero α] [Preorder α] [PosMulMono α]
    [MulPosMono α] {f : Filter ι} {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) :
    IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)

Proof state:
case intro
α : Type u_1
ι : Type u_4
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)

Tactic:
obtain ⟨V, hV⟩ := h₄.eventually_le

Result:
case intro.intro
α : Type u_1
ι : Type u_4
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)

Proof state:
α : Type u_1
ι : Type u_4
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
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
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)

Tactic:
obtain ⟨U, hU⟩ := h₂.eventually_le

Result:
case intro
α : Type u_1
ι : Type u_4
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)

Proof state:
case intro.intro
α : Type u_1
ι : Type u_4
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
⊢ ∀ᶠ (x : ι) in f, (u * v) x ≤ U * V

Tactic:
filter_upwards [hU, hV, h₁, h₃] with x x_U x_V u_0 v_0

Result:
case h
α : Type u_1
ι : Type u_4
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
u_0 : 0 x ≤ u x
v_0 : 0 x ≤ v x
⊢ (u * v) x ≤ U * V

Proof state:
case intro.intro
α : Type u_1
ι : Type u_4
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)

Tactic:
refine isBoundedUnder_of_eventually_le (a := U * V) ?_

Result:
case intro.intro
α : Type u_1
ι : Type u_4
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
⊢ ∀ᶠ (x : ι) in f, (u * v) x ≤ U * V

Proof state:
case h
α : Type u_1
ι : Type u_4
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
f : Filter ι
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
u_0 : 0 x ≤ u x
v_0 : 0 x ≤ v x
⊢ (u * v) x ≤ U * V

Tactic:
exact mul_le_mul x_U x_V v_0 (u_0.trans x_U)

Result:
no goals