-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma liminf_mul_le [NeBot f] (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v)
    (h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤) (h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0) :
    liminf (u * v) f ≤ limsup u f * liminf v f

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > liminf v f
c : EReal
c_ab : c > a * b
⊢ ∃ᶠ (a : α) in f, (u * v) a < c

Tactic:
refine (((frequently_lt_of_liminf_lt) b_v).and_eventually <| (eventually_lt_of_limsup_lt a_u).and
  <| hu.and hv).mono fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_

Result:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > liminf v f
c : EReal
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

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h : liminf v f ≠ 0
⊢ 0 ≤ liminf v f

Tactic:
exact le_of_eq_of_le (liminf_const 0).symm (liminf_le_liminf hv)

Result:
no goals

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Tactic:
refine le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (liminf_le_iff).2 fun c c_ab ↦ ?_

Result:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > liminf v f
c : EReal
c_ab : c > a * b
⊢ ∃ᶠ (a : α) in f, (u * v) a < c

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
⊢ 0 < limsup u f ∨ liminf v f ≠ ⊤

Tactic:
refine h₁.imp_left fun h ↦ lt_of_le_of_ne ?_ h.symm

Result:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
h : limsup u f ≠ 0
⊢ 0 ≤ limsup u f

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Tactic:
replace h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤ := by
  refine h₁.imp_left fun h ↦ lt_of_le_of_ne ?_ h.symm
  exact le_of_eq_of_le (limsup_const 0).symm (limsup_le_limsup hu)

Result:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > liminf v f
c : EReal
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_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
⊢ limsup u f ≠ ⊤ ∨ 0 < liminf v f

Tactic:
refine h₂.imp_right fun h ↦ lt_of_le_of_ne ?_ h.symm

Result:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h : liminf v f ≠ 0
⊢ 0 ≤ liminf v f

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Tactic:
replace h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f := by
  refine h₂.imp_right fun h ↦ lt_of_le_of_ne ?_ h.symm
  exact le_of_eq_of_le (liminf_const 0).symm (liminf_le_liminf hv)

Result:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
h : limsup u f ≠ 0
⊢ 0 ≤ limsup u f

Tactic:
exact le_of_eq_of_le (limsup_const 0).symm (limsup_le_limsup hu)

Result:
no goals