-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma le_limsup_mul (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) :
    limsup u f * liminf v f ≤ limsup (u * v) f

Proof state:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
a : EReal
ha : a ∈ Ico 0 (limsup u f)
b : EReal
hb : b ∈ Ico 0 (liminf v f)
c : EReal
c_ab : c < a * b
⊢ ∃ᶠ (a : α) in f, c < (u * v) a

Tactic:
refine (((frequently_lt_of_lt_limsup) (mem_Ico.1 ha).2).and_eventually
  <| (eventually_lt_of_lt_liminf (mem_Ico.1 hb).2).and
  <| hu.and hv).mono fun x ⟨xa, ⟨xb, u0, _⟩⟩ ↦ ?_

Result:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u0✝ : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
a : EReal
ha : a ∈ Ico 0 (limsup u f)
b : EReal
hb : b ∈ Ico 0 (liminf v f)
c : EReal
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 * v) x

Proof state:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 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 uv0 fun a ha b hb ↦ (le_limsup_iff).2 fun c c_ab ↦ ?_

Result:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
a : EReal
ha : a ∈ Ico 0 (limsup u f)
b : EReal
hb : b ∈ Ico 0 (liminf v f)
c : EReal
c_ab : c < a * b
⊢ ∃ᶠ (a : α) in f, c < (u * v) a

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
rcases f.eq_or_neBot with rfl | _

Result:
case inl
α : Type u_3
u v : α → EReal
hu : 0 ≤ᶠ[⊥] u
hv : 0 ≤ᶠ[⊥] v
⊢ limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥

case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Proof state:
case inl
α : Type u_3
u v : α → EReal
hu : 0 ≤ᶠ[⊥] u
hv : 0 ≤ᶠ[⊥] v
⊢ limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥

Tactic:
rw [limsup_bot, limsup_bot, liminf_bot, bot_mul_top]

Result:
no goals

Proof state:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu.frequently

Result:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u0 : 0 ≤ limsup u f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Proof state:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u0 : 0 ≤ limsup u f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
have uv0 : 0 ≤ limsup (u * v) f :=
  le_limsup_of_frequently_le ((hu.and hv).mono fun _ ⟨hu, hv⟩ ↦ mul_nonneg hu hv).frequently

Result:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Proof state:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u0✝ : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
a : EReal
ha : a ∈ Ico 0 (limsup u f)
b : EReal
hb : b ∈ Ico 0 (liminf v f)
c : EReal
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 * v) x

Tactic:
exact c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ico.1 hb).1 u0)

Result:
no goals