awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
a : EReal
ha : a ∈ Ioo 0 (limsup u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
inr : ∀ (x : α), a < u x ∧ b < v x ∧ 0 x ≤ v x → ∀ (xa : a < u x) (xb : b < v x) (vx : 0 x ≤ v x), c < (u * v) x
⊢ ∃ᶠ (a : α) in f, c < (u * v) a

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

Premises used: Filter.eventually_lt_of_lt_liminf, Set.mem_Ioo, Filter.Eventually.and, Filter.Frequently.mono, Filter.Frequently.and_eventually, And.right, Iff.mp, Filter.frequently_lt_of_lt_limsup
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
a : EReal
ha : a ∈ Ioo 0 (limsup u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
x : α
h_1 : a < u x ∧ b < v x ∧ 0 x ≤ v x
xa : a < u x
xb : b < v x
vx : 0 x ≤ v x
⊢ c < (u * v) x

Tactic:
c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ioo.1 hb).1.le ((mem_Ioo.1 ha).1.le.trans xa.le))

Premises used: Set.mem_Ioo, LT.lt.le, And.left, mul_le_mul, LT.lt.trans_le, Iff.mp, LE.le.trans
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
a : EReal
ha : a ∈ Ioo 0 (limsup u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
x : α
h_1 : a < u x ∧ b < v x ∧ 0 x ≤ v x
xa : a < u x
xb : b < v x
vx : 0 x ≤ v x
⊢ c < (u * v) x

Tactic:
exact c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ioo.1 hb).1.le ((mem_Ioo.1 ha).1.le.trans xa.le))

Premises used: Set.mem_Ioo, LT.lt.le, And.left, mul_le_mul, LT.lt.trans_le, Iff.mp, LE.le.trans
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
inl :
  ∀ (hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x) (hv : 0 ≤ᶠ[⊥] v) (h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤)
    (h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0), limsup (u * v) ⊥ ≤ limsup u ⊥ * limsup v ⊥
inr : f.NeBot → limsup (u * v) f ≤ limsup u f * limsup v f
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
rcases f.eq_or_neBot with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤
h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0
inl : ⊥ ≤ limsup u ⊥ * limsup v ⊥
⊢ limsup (u * v) ⊥ ≤ limsup u ⊥ * limsup v ⊥

Tactic:
rw [limsup_bot]

Premises used: Filter.limsup_bot
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤
h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0
⊢ ⊥ ≤ limsup u ⊥ * limsup v ⊥

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
h₁ : limsup u ⊥ ≠ 0 ∨ limsup v ⊥ ≠ ⊤
h₂ : limsup u ⊥ ≠ ⊤ ∨ limsup v ⊥ ≠ 0
⊢ ⊥ ≤ limsup u ⊥ * limsup v ⊥

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
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

Tactic:
have u_0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h : f.NeBot
u_0 : 0 ≤ limsup u f
⊢ 0 < limsup u f ∨ limsup v f ≠ ⊤

Tactic:
replace h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤ := h₁.imp_left fun h ↦ lt_of_le_of_ne u_0 h.symm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h₂ : limsup u f ≠ ⊤ ∨ limsup v f ≠ 0
h : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
⊢ limsup u f ≠ ⊤ ∨ 0 < limsup v f

Tactic:
replace h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f :=
    h₂.imp_right fun h ↦ lt_of_le_of_ne (le_limsup_of_frequently_le hv.frequently) h.symm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
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:
le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.limsup_le_iff, EReal.le_mul_of_forall_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
inr :
  ∀ (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
⊢ 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 ↦ ?_

Premises used: Iff.mpr, Filter.limsup_le_iff, EReal.le_mul_of_forall_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h_1 : f.NeBot
u_0 : 0 ≤ limsup u f
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
h : ∀ (x : α) (x_a : u x < a) (x_b : v x < b) (v_0 : 0 x ≤ v x), (u * v) x < c
⊢ ∀ᶠ (a : α) in f, (u * v) a < c

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

Premises used: Filter.eventually_lt_of_limsup_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
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
v_0 : 0 x ≤ v x
apply : (u * v) x ≤ a * b
⊢ (u * v) x < c

Tactic:
apply lt_of_le_of_lt _ c_ab

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
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
v_0 : 0 x ≤ v x
inl : ∀ (hux : u x < 0), (u * v) x ≤ a * b
inr : ∀ (hux : 0 ≤ u x), (u * v) x ≤ a * b
⊢ (u * v) x ≤ a * b

Tactic:
rcases lt_or_ge (u x) 0 with hux | hux

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
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
v_0 : 0 x ≤ v x
hux : u x < 0
inl : 0 ≤ a * b
⊢ (u * v) x ≤ a * b

Tactic:
apply (mul_nonpos_iff.2 (.inr ⟨hux.le, v_0⟩)).trans

Premises used: Iff.mpr, EReal.mul_nonpos_iff, LT.lt.le, And.intro, LE.le.trans, Or.inr
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
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
v_0 : 0 x ≤ v x
hux : u x < 0
⊢ 0 ≤ a * b

Tactic:
mul_nonneg (u_0.trans a_u.le) (v_0.trans x_b.le)

Premises used: mul_nonneg, LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
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
v_0 : 0 x ≤ v x
hux : u x < 0
⊢ 0 ≤ a * b

Tactic:
exact mul_nonneg (u_0.trans a_u.le) (v_0.trans x_b.le)

Premises used: mul_nonneg, LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
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
v_0 : 0 x ≤ v x
hux : 0 ≤ u x
⊢ (u * v) x ≤ a * b

Tactic:
mul_le_mul x_a.le x_b.le v_0 (hux.trans x_a.le)

Premises used: LT.lt.le, mul_le_mul, LE.le.trans
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u_0 : 0 ≤ limsup u f
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
v_0 : 0 x ≤ v x
hux : 0 ≤ u x
⊢ (u * v) x ≤ a * b

Tactic:
exact mul_le_mul x_a.le x_b.le v_0 (hux.trans x_a.le)

Premises used: LT.lt.le, mul_le_mul, LE.le.trans
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
apply : ∀ a' ∈ Ioo 0 (liminf u f), ∀ b' ∈ Ioo 0 (liminf v f), a' * b' ≤ liminf (fun (x : α) ↦ u x * v x) f
⊢ liminf u f * liminf v f ≤ liminf (u * v) f

Tactic:
apply mul_le_of_forall_lt_of_nonneg ((le_liminf_of_le) hu)
    <| (le_liminf_of_le) ((hu.and hv).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0)

Premises used: mul_nonneg, HMul.hMul, EReal.mul_le_of_forall_lt_of_nonneg, Filter.Eventually.and, LE.le, Filter.Eventually.mono, OfNat.ofNat, _private.0.EReal.le_liminf_mul.match_1, Filter.le_liminf_of_le
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
⊢ ∀ a' ∈ Ioo 0 (liminf u f), ∀ b' ∈ Ioo 0 (liminf v f), a' * b' ≤ liminf (fun (x : α) ↦ u x * v x) f

Tactic:
fun a ha b hb ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.le_liminf_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
refine :
  ∀ (a : EReal) (ha : a ∈ Ioo 0 (liminf u f)) (b : EReal) (hb : b ∈ Ioo 0 (liminf v f)) (c : EReal) (c_ab : c < a * b),
    ∀ᶠ (a : α) in f, c < u a * v a
⊢ ∀ a' ∈ Ioo 0 (liminf u f), ∀ b' ∈ Ioo 0 (liminf v f), a' * b' ≤ liminf (fun (x : α) ↦ u x * v x) f

Tactic:
refine fun a ha b hb ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.le_liminf_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ioo 0 (liminf u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
h : ∀ (x : α) (xa : a < u x) (xb : b < v x), c < u x * v x
⊢ ∀ᶠ (a : α) in f, c < u a * v a

Tactic:
filter_upwards [eventually_lt_of_lt_liminf (mem_Ioo.1 ha).2,
    eventually_lt_of_lt_liminf (mem_Ioo.1 hb).2] with x xa xb

Premises used: Filter.eventually_lt_of_lt_liminf, Set.mem_Ioo, And.right, Iff.mp
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ioo 0 (liminf u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
x : α
xa : a < u x
xb : b < v x
⊢ c < u x * v x

Tactic:
c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ioo.1 hb).1.le ((mem_Ioo.1 ha).1.le.trans xa.le))

Premises used: Set.mem_Ioo, LT.lt.le, And.left, mul_le_mul, LT.lt.trans_le, Iff.mp, LE.le.trans
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ioo 0 (liminf u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
x : α
xa : a < u x
xb : b < v x
⊢ c < u x * v x

Tactic:
exact c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ioo.1 hb).1.le ((mem_Ioo.1 ha).1.le.trans xa.le))

Premises used: Set.mem_Ioo, LT.lt.le, And.left, mul_le_mul, LT.lt.trans_le, Iff.mp, LE.le.trans
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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:
h₁.imp_left fun h ↦ lt_of_le_of_ne ?_ h.symm

Premises used: Or.imp_left, lt_of_le_of_ne
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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
refine : ∀ (h : limsup u f ≠ 0), 0 ≤ limsup u f
⊢ 0 < limsup u f ∨ liminf v f ≠ ⊤

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

Premises used: Or.imp_left, lt_of_le_of_ne
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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:
le_of_eq_of_le (limsup_const 0).symm (limsup_le_limsup hu)

Premises used: Filter.limsup_const, le_of_eq_of_le, Filter.limsup_le_limsup, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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)

Premises used: Filter.limsup_const, le_of_eq_of_le, Filter.limsup_le_limsup, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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:
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)
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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:
h₂.imp_right fun h ↦ lt_of_le_of_ne ?_ h.symm

Premises used: Or.imp_right, lt_of_le_of_ne
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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 ≠ ⊤
refine : ∀ (h : liminf v f ≠ 0), 0 ≤ liminf v f
⊢ limsup u f ≠ ⊤ ∨ 0 < liminf v f

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

Premises used: Or.imp_right, lt_of_le_of_ne
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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:
le_of_eq_of_le (liminf_const 0).symm (liminf_le_liminf hv)

Premises used: Filter.liminf_const, le_of_eq_of_le, Filter.liminf_le_liminf, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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)

Premises used: Filter.liminf_const, le_of_eq_of_le, Filter.liminf_le_liminf, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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:
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)
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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:
le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (liminf_le_iff).2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.liminf_le_iff, EReal.le_mul_of_forall_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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
refine :
  ∀ (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
⊢ 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 ↦ ?_

Premises used: Iff.mpr, Filter.liminf_le_iff, EReal.le_mul_of_forall_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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:
(((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⟩ ↦ ?_

Premises used: HMul.hMul, Filter.Eventually.and, Filter.eventually_lt_of_limsup_lt, Filter.Frequently.mono, Filter.Frequently.and_eventually, _private.0.EReal.liminf_mul_le.match_1, Filter.frequently_lt_of_liminf_lt, LT.lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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
refine :
  ∀ (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
⊢ ∃ᶠ (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⟩ ↦ ?_

Premises used: Filter.Eventually.and, Filter.eventually_lt_of_limsup_lt, Filter.Frequently.mono, Filter.Frequently.and_eventually, Filter.frequently_lt_of_liminf_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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 : α
h : 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:
(mul_le_mul x_u.le x_v.le v_0 (u_0.trans x_u.le)).trans_lt c_ab

Premises used: LT.lt.le, mul_le_mul, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : 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 : α
h : 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

Premises used: LT.lt.le, mul_le_mul, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a b : ℝ
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), (↑b : EReal))

Tactic:
simp only [ContinuousAt, nhds_coe_coe, ← coe_add, tendsto_map'_iff, Function.comp_def,
    tendsto_coe, tendsto_add]

Premises used: ContinuousAt, Filter.tendsto_map'_iff, EReal.tendsto_coe, Function.comp_def, tendsto_add, EReal.coe_add, EReal.nhds_coe_coe
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
simp : ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, (↑a : EReal)), (↑x : EReal) < a.1 + a.2
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, (↑a : EReal))

Tactic:
simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_coe]

Premises used: ContinuousAt, EReal.top_add_coe, EReal.tendsto_nhds_top_iff_real
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, (↑a : EReal)), (↑x : EReal) < a.1 + a.2

Tactic:
fun r ↦ ((lt_mem_nhds (coe_lt_top (r - (a - 1)))).prod_nhds
    (lt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| sub_one_lt _)).mono fun _ h ↦ ?_

Premises used: Iff.mpr, HSub.hSub, sub_one_lt, Filter.Eventually.mono, Filter.Eventually.prod_nhds, OfNat.ofNat, lt_mem_nhds, EReal.coe_lt_coe_iff, EReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
refine :
  ∀ (r : ℝ) (x : EReal × EReal) (h : (↑(r - (a - 1)) : EReal) < x.1 ∧ (↑(a - 1) : EReal) < x.2),
    (↑r : EReal) < x.1 + x.2
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, (↑a : EReal)), (↑x : EReal) < a.1 + a.2

Tactic:
refine fun r ↦ ((lt_mem_nhds (coe_lt_top (r - (a - 1)))).prod_nhds
    (lt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| sub_one_lt _)).mono fun _ h ↦ ?_

Premises used: Iff.mpr, HSub.hSub, sub_one_lt, Filter.Eventually.mono, Filter.Eventually.prod_nhds, OfNat.ofNat, lt_mem_nhds, EReal.coe_lt_coe_iff, EReal.coe_lt_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a r : ℝ
x : EReal × EReal
h : (↑(r - (a - 1)) : EReal) < x.1 ∧ (↑(a - 1) : EReal) < x.2
⊢ (↑r : EReal) < x.1 + x.2

Tactic:
simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2

Premises used: And.right, And.left, EReal.coe_add, EReal.add_lt_add, sub_add_cancel
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
a : ℝ
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑a : EReal), ⊤)

Tactic:
simpa only [add_comm, Function.comp_def, ContinuousAt, Prod.swap]
    using Tendsto.comp (continuousAt_add_top_coe a) (continuous_swap.tendsto ((a : EReal), ⊤))

Premises used: ContinuousAt, continuous_swap, Prod.mk, add_comm, Continuous.tendsto, Function.comp_def, EReal.continuousAt_add_top_coe, Prod.swap, Filter.Tendsto.comp, Top.top, Real.toEReal
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
simp : ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), (↑x : EReal) < a.1 + a.2
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) (⊤, ⊤)

Tactic:
simp only [ContinuousAt, tendsto_nhds_top_iff_real, top_add_top]

Premises used: ContinuousAt, EReal.tendsto_nhds_top_iff_real, EReal.top_add_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
⊢ ∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), (↑x : EReal) < a.1 + a.2

Tactic:
fun r ↦ ((lt_mem_nhds (coe_lt_top 0)).prod_nhds
    (lt_mem_nhds <| coe_lt_top r)).mono fun _ h ↦ ?_

Premises used: Filter.Eventually.mono, Filter.Eventually.prod_nhds, OfNat.ofNat, lt_mem_nhds, EReal.coe_lt_top