awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
a0 : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
⊢ ∃ᶠ (x : ι) in f, a < u x

Tactic:
have h₅ := frequently_lt_of_lt_limsup h₁ au
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
a0 : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₅ : ∃ᶠ (x : ι) in f, a < u x
⊢ ∀ᶠ (a : ι) in f, b < v a

Tactic:
have h₆ := eventually_lt_of_lt_liminf bv (isBoundedUnder_of_eventually_ge h₃)
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
a0 : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₅ : ∃ᶠ (x : ι) in f, a < u x
h₆ : ∀ᶠ (a : ι) in f, b < v a
apply : ∀ (x : ι), a < u x ∧ b < v x ∧ 0 x ≤ v x → c < u x * v x
⊢ ∃ᶠ (a : ι) in f, c < u a * v a

Tactic:
apply (h₅.and_eventually (h₆.and h₃)).mono

Premises used: Filter.Eventually.and, Filter.Frequently.mono, Filter.Frequently.and_eventually
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
a0 : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₅ : ∃ᶠ (x : ι) in f, a < u x
h₆ : ∀ᶠ (a : ι) in f, b < v a
⊢ ∀ (x : ι), a < u x ∧ b < v x ∧ 0 x ≤ v x → c < u x * v x

Tactic:
fun x ⟨xa, ⟨xb, _⟩⟩ ↦ c_ab.trans_le <| mul_le_mul xa.le xb.le b0 (a0.trans xa.le)

Premises used: HMul.hMul, LT.lt.le, _private.0.le_limsup_mul.match_2, mul_le_mul, LT.lt.trans_le, LT.lt, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
a0 : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₅ : ∃ᶠ (x : ι) in f, a < u x
h₆ : ∀ᶠ (a : ι) in f, b < v a
⊢ ∀ (x : ι), a < u x ∧ b < v x ∧ 0 x ≤ v x → c < u x * v x

Tactic:
exact fun x ⟨xa, ⟨xb, _⟩⟩ ↦ c_ab.trans_le <| mul_le_mul xa.le xb.le b0 (a0.trans xa.le)
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (limsup_le_iff h h').2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.limsup_le_iff, le_mul_of_forall_lt₀
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
refine :
  ∀ (a : ℝ) (a_u : a > limsup u f) (b : ℝ) (b_v : b > limsup v f) (c : ℝ) (c_ab : c > a * b),
    ∀ᶠ (a : ι) in f, u a * v a < c
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

Tactic:
refine le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (limsup_le_iff h h').2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.limsup_le_iff, le_mul_of_forall_lt₀
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
h₅ : ∀ (x : ι) (x_a : u x < a) (x_b : v x < b) (v_0 : 0 x ≤ v x), u x * v x < c
⊢ ∀ᶠ (a : ι) in f, u a * v a < c

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

Premises used: Filter.eventually_lt_of_limsup_lt
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
x : ι
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
apply : u x * v x ≤ a * b
⊢ u x * v x < c

Tactic:
apply lt_of_le_of_lt _ c_ab

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
x : ι
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
inl : ∀ (u_0 : u x < 0), u x * v x ≤ a * b
inr : ∀ (u_0 : 0 ≤ u x), u x * v x ≤ a * b
⊢ u x * v x ≤ a * b

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

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
x : ι
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
u_0 : u x < 0
inl : 0 ≤ a * b
⊢ u x * v x ≤ a * b

Tactic:
apply (mul_nonpos_of_nonpos_of_nonneg u_0.le v_0).trans

Premises used: mul_nonpos_of_nonpos_of_nonneg, LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
x : ι
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
u_0 : u x < 0
⊢ 0 ≤ a * b

Tactic:
mul_nonneg ((le_limsup_of_frequently_le h₁ h₂).trans a_u.le) (v_0.trans x_b.le)

Premises used: mul_nonneg, Filter.le_limsup_of_frequently_le, LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
x : ι
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
u_0 : u x < 0
⊢ 0 ≤ a * b

Tactic:
exact mul_nonneg ((le_limsup_of_frequently_le h₁ h₂).trans a_u.le) (v_0.trans x_b.le)

Premises used: mul_nonneg, Filter.le_limsup_of_frequently_le, LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
x : ι
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
u_0 : 0 ≤ u x
⊢ u x * v x ≤ a * b

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

Premises used: LT.lt.le, mul_le_mul, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
x : ι
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
u_0 : 0 ≤ u x
⊢ u x * v x ≤ a * b

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

Premises used: LT.lt.le, mul_le_mul, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)

Tactic:
have h := isCoboundedUnder_ge_mul_of_nonneg h₁ h₂ h₃ h₄
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x

Tactic:
have h' := isBoundedUnder_of_eventually_ge (a := 0)
    <| (h₁.and h₃).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
apply : ∀ a' ≥ 0, a' < liminf u f → ∀ b' ≥ 0, b' < liminf v f → a' * b' ≤ liminf (u * v) f
⊢ liminf u f * liminf v f ≤ liminf (u * v) f

Tactic:
apply mul_le_of_forall_lt_of_nonneg (le_liminf_of_le h₂.isCoboundedUnder_ge h₁)
    (le_liminf_of_le h ((h₁.and h₃).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0))

Premises used: mul_nonneg, HMul.hMul, Filter.Eventually.and, LE.le, Filter.Eventually.mono, Filter.IsBoundedUnder.isCoboundedUnder_ge, mul_le_of_forall_lt_of_nonneg, OfNat.ofNat, _private.0.le_liminf_mul.match_1, Filter.le_liminf_of_le
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
a : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
⊢ a * b ≤ liminf (u * v) f

Tactic:
(le_liminf_iff h h').2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.le_liminf_iff
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
a : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
refine : ∀ (c : ℝ) (c_ab : c < a * b), ∀ᶠ (a : ι) in f, c < (u * v) a
⊢ a * b ≤ liminf (u * v) f

Tactic:
refine (le_liminf_iff h h').2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.le_liminf_iff
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
a : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
h₅ : ∀ (x : ι) (xa : a < u x) (xb : b < v x), c < (u * v) x
⊢ ∀ᶠ (a : ι) in f, c < (u * v) a

Tactic:
filter_upwards [eventually_lt_of_lt_liminf au (isBoundedUnder_of_eventually_ge h₁),
    eventually_lt_of_lt_liminf bv (isBoundedUnder_of_eventually_ge h₃)] with x xa xb

Premises used: Filter.eventually_lt_of_lt_liminf, Filter.isBoundedUnder_of_eventually_ge
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
a : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
x : ι
xa : a < u x
xb : b < v x
⊢ c < (u * v) x

Tactic:
c_ab.trans_le (mul_le_mul xa.le xb.le b0 (a0.trans xa.le))

Premises used: LT.lt.le, mul_le_mul, LT.lt.trans_le, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
a : ℝ
a0 : a ≥ 0
au : a < liminf u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
x : ι
xa : a < u x
xb : b < v x
⊢ c < (u * v) x

Tactic:
exact c_ab.trans_le (mul_le_mul xa.le xb.le b0 (a0.trans xa.le))

Premises used: LT.lt.le, mul_le_mul, LT.lt.trans_le, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x

Tactic:
have h' := isBoundedUnder_of_eventually_ge (a := 0)
    <| (h₁.and h₃).mono fun x ⟨u_0, v_0⟩ ↦ mul_nonneg u_0 v_0
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Tactic:
le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (liminf_le_iff h h').2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.liminf_le_iff, le_mul_of_forall_lt₀
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
refine :
  ∀ (a : ℝ) (a_u : a > limsup u f) (b : ℝ) (b_v : b > liminf v f) (c : ℝ) (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₀ fun a a_u b b_v ↦ (liminf_le_iff h h').2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.liminf_le_iff, le_mul_of_forall_lt₀
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > liminf v f
c : ℝ
c_ab : c > a * b
⊢ ∃ᶠ (a : ι) in f, (u * v) a < c

Tactic:
((frequently_lt_of_liminf_lt h₄ b_v).and_eventually ((eventually_lt_of_limsup_lt a_u).and
    (h₁.and h₃))).mono fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_

Premises used: HMul.hMul, _private.0.liminf_mul_le.match_1, Filter.Eventually.and, Filter.eventually_lt_of_limsup_lt, Filter.Frequently.mono, Filter.Frequently.and_eventually, Filter.frequently_lt_of_liminf_lt, LT.lt
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > liminf v f
c : ℝ
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 h₄ b_v).and_eventually ((eventually_lt_of_limsup_lt a_u).and
    (h₁.and h₃))).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.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > liminf v f
c : ℝ
c_ab : c > a * b
x : ι
h_1 : 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.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
f : Filter ι
u v : ι → ℝ
inst : f.NeBot
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (x : ι) ↦ u x * v x
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > liminf v f
c : ℝ
c_ab : c > a * b
x : ι
h_1 : 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.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : F.NeBot
inst_4 : Add R
inst_5 : ContinuousAdd R
inst_6 : AddLeftMono R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
x x_1 : R
h : x ≤ x_1
dsimp : c + x ≤ c + x_1
⊢ LE.le.{u_4} (α := R) ((fun (x : R) ↦ c + x) x) ((fun (x : R) ↦ c + x) x_1)

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : F.NeBot
inst_4 : Add R
inst_5 : ContinuousAdd R
inst_6 : AddLeftMono R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
x x_1 : R
h : x ≤ x_1
⊢ c + x ≤ c + x_1

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : F.NeBot
inst_4 : Add R
inst_5 : ContinuousAdd R
inst_6 : AddRightMono R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
x x_1 : R
h : x ≤ x_1
dsimp : x + c ≤ x_1 + c
⊢ LE.le.{u_4} (α := R) ((fun (x : R) ↦ x + c) x) ((fun (x : R) ↦ x + c) x_1)

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : F.NeBot
inst_4 : Add R
inst_5 : ContinuousAdd R
inst_6 : AddRightMono R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) F f
x x_1 : R
h : x ≤ x_1
⊢ x + c ≤ x_1 + c

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : F.NeBot
inst_4 : Add R
inst_5 : ContinuousAdd R
inst_6 : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
x x_1 : R
h : x ≤ x_1
dsimp : c + x ≤ c + x_1
⊢ LE.le.{u_4} (α := R) ((fun (x : R) ↦ c + x) x) ((fun (x : R) ↦ c + x) x_1)

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
R : Type u_4
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
F : Filter ι
inst_3 : F.NeBot
inst_4 : Add R
inst_5 : ContinuousAdd R
inst_6 : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) F f
x x_1 : R
h : x ≤ x_1
⊢ c + x ≤ c + x_1

Tactic:
gcongr