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

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
⊢ limsup (u * v) f ≤ limsup u f * limsup 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
h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤
h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0
⊢ limsup (u * v) ⊥ ≤ limsup u ⊥ * limsup v ⊥

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

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

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

Result:
no goals

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

Tactic:
replace h₁ : 0 < limsup u f ∨ limsup 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:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h✝ : f.NeBot
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Proof state:
case inl
α : Type u_3
u v : α → EReal
hu : 0 ≤ᶠ[⊥] u
hv : 0 ≤ᶠ[⊥] v
h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤
h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0
⊢ limsup (u * v) ⊥ ≤ limsup u ⊥ * limsup v ⊥

Tactic:
rw [limsup_bot]

Result:
case inl
α : Type u_3
u v : α → EReal
hu : 0 ≤ᶠ[⊥] u
hv : 0 ≤ᶠ[⊥] v
h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤
h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0
⊢ ⊥ ≤ limsup u ⊥ * limsup v ⊥

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

Proof state:
case h
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
x : α
x_a : u x < a
x_b : v x < b
u_0 : 0 x ≤ u x
v_0 : 0 x ≤ v x
⊢ (u * v) x < c

Tactic:
exact (mul_le_mul x_a.le x_b.le v_0 (u_0.trans x_a.le)).trans_lt c_ab

Result:
no goals

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

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

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

Result:
case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
⊢ limsup (u * v) f ≤ limsup u f * limsup 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
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
⊢ ∀ᶠ (a : α) in f, (u * v) a < c

Tactic:
filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v, hu, hv]
  with x x_a x_b u_0 v_0

Result:
case h
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
x : α
x_a : u x < a
x_b : v x < b
u_0 : 0 x ≤ u x
v_0 : 0 x ≤ v x
⊢ (u * v) x < c

Proof state:
case inl
α : Type u_3
u v : α → EReal
hu : 0 ≤ᶠ[⊥] u
hv : 0 ≤ᶠ[⊥] v
h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤
h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0
⊢ ⊥ ≤ limsup u ⊥ * limsup v ⊥

Tactic:
exact bot_le

Result:
no goals

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h✝ : f.NeBot
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
⊢ limsup u f ≠ ⊤ ∨ 0 < limsup 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
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h✝ : f.NeBot
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h : limsup v f ≠ 0
⊢ 0 ≤ limsup 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
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
refine le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (limsup_le_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
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
⊢ ∀ᶠ (a : α) in f, (u * v) a < c