awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (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 (u + v)
a : α
a_u : a < limsup u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
⊢ ∃ᶠ (a : ι) in f, c < (u + v) a
have refine : ∀ (x : ι) (ab_x : a < u x ∧ b < v x), c < (u + v) x
Tactic: refine ((frequently_lt_of_lt_limsup h₂ a_u).and_eventually
    (eventually_lt_of_lt_liminf b_v h₄)).mono fun _ ab_x ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
⊢ limsup (u + v) f ≤ limsup u f + limsup v f
have h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
Tactic: have h := isCoboundedUnder_le_add h₁ h₃
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
⊢ limsup (u + v) f ≤ limsup u f + limsup v f
have h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
Tactic: have h' := isBoundedUnder_le_add h₂ h₄
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (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 (u + v)
⊢ limsup (u + v) f ≤ limsup u f + limsup v f
have refine : ∀ (a : α) (a_u : a > limsup u f) (b : α) (b_v : b > limsup v f), limsup (u + v) f ≤ a + b
Tactic: refine le_add_of_forall_lt fun a a_u b b_v ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (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 (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > limsup v f
⊢ limsup (u + v) f ≤ a + b
have rw : ∀ y > a + b, ∀ᶠ (a : ι) in f, (u + v) a < y
Tactic: rw [limsup_le_iff h h']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (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 (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > limsup v f
c : α
c_ab : c > a + b
⊢ ∀ᶠ (a : ι) in f, (u + v) a < c
have h₅ : ∀ (x : ι) (a_x : u x < a) (b_x : v x < b), (u + v) x < c
Tactic: filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v] with x a_x b_x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
⊢ liminf u f + liminf v f ≤ liminf (u + v) f
have h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
Tactic: have h := isCoboundedUnder_ge_add h₂ h₄
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
⊢ liminf u f + liminf v f ≤ liminf (u + v) f
have h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
Tactic: have h' := isBoundedUnder_ge_add h₁ h₃
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) 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 (u + v)
⊢ liminf u f + liminf v f ≤ liminf (u + v) f
have refine : ∀ (a : α) (a_u : a < liminf u f) (b : α) (b_v : b < liminf v f), a + b ≤ liminf (u + v) f
Tactic: refine add_le_of_forall_lt fun a a_u b b_v ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) 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 (u + v)
a : α
a_u : a < liminf u f
b : α
b_v : b < liminf v f
⊢ a + b ≤ liminf (u + v) f
have rw : ∀ y < a + b, ∀ᶠ (a : ι) in f, y < (u + v) a
Tactic: rw [le_liminf_iff h h']
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) 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 (u + v)
a : α
a_u : a < liminf u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
⊢ ∀ᶠ (a : ι) in f, c < (u + v) a
have h₅ : ∀ (x : ι) (a_x : a < u x) (b_x : b < v x), c < (u + v) x
Tactic: filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
⊢ liminf (u + v) f ≤ limsup u f + liminf v f
have h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
Tactic: have h := isCoboundedUnder_ge_add h₂ h₄
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
⊢ liminf (u + v) f ≤ limsup u f + liminf v f
have h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
Tactic: have h' := isBoundedUnder_ge_add h₁ h₃
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) 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 (u + v)
⊢ liminf (u + v) f ≤ limsup u f + liminf v f
have refine : ∀ (a : α) (a_u : a > limsup u f) (b : α) (b_v : b > liminf v f) (x : α) (c_ab : x > a + b),
  ∃ᶠ (a : ι) in f, (u + v) a < x
Tactic: refine le_add_of_forall_lt fun a a_u b b_v ↦ (liminf_le_iff h h').2 fun _ c_ab ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) 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 (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > liminf v f
x : α
c_ab : x > a + b
⊢ ∃ᶠ (a : ι) in f, (u + v) a < x
have refine : ∀ (x_1 : ι) (ab_x : v x_1 < b ∧ u x_1 < a), (u + v) x_1 < x
Tactic: refine ((frequently_lt_of_liminf_lt h₄ b_v).and_eventually
    (eventually_lt_of_limsup_lt a_u h₂)).mono fun _ ab_x ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
have h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
Tactic: have h := IsCoboundedUnder.of_frequently_ge (a := 0)
    <| (h₁.and_eventually h₃).mono fun x ⟨ux_0, vx_0⟩ ↦ mul_nonneg ux_0 vx_0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
have h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
Tactic: have h' := isBoundedUnder_le_mul_of_nonneg h₁ h₂ h₃ h₄
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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 f * liminf v f ≤ limsup (u * v) f
have u0 : 0 ≤ limsup u f
Tactic: have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le h₁ h₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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)
u0 : 0 ≤ limsup u f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
have uv : 0 ≤ limsup (u * v) f
Tactic: have uv : 0 ≤ limsup (u * v) f :=
    le_limsup_of_frequently_le ((h₁.and_eventually h₃).mono fun _ ⟨hu, hv⟩ ↦ mul_nonneg hu hv) h'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f
have refine : ∀ (a : ℝ) (a0 : a ≥ 0) (au : a < limsup u f) (b : ℝ) (b0 : b ≥ 0) (bv : b < liminf v f), a * b ≤ limsup (u * v) f
Tactic: refine mul_le_of_forall_lt_of_nonneg u0 uv fun a a0 au b b0 bv ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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)
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
⊢ a * b ≤ limsup (u * v) f
have refine : ∀ (c : ℝ) (c_ab : c < a * b), ∃ᶠ (a : ι) in f, c < u a * v a
Tactic: refine (le_limsup_iff h h').2 fun c c_ab ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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)
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
⊢ ∃ᶠ (a : ι) in f, c < u a * v a
have h₅ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
Tactic: replace h₁ := IsCoboundedUnder.of_frequently_ge h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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
⊢ ∃ᶠ (a : ι) in f, c < u a * v a
have h₅ : ∃ᶠ (x : ι) in f, a < u x
Tactic: have h₅ := frequently_lt_of_lt_limsup h₁ au
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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, c < u a * v a
have h₆ : ∀ᶠ (a : ι) in f, b < v a
Tactic: have h₆ := eventually_lt_of_lt_liminf bv (isBoundedUnder_of_eventually_ge h₃)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ ∃ᶠ (a : ι) in f, c < u a * v a
have apply : ∀ (x : ι), a < u x ∧ b < v x ∧ 0 x ≤ v x → c < u x * v x
Tactic: apply (h₅.and_eventually (h₆.and h₃)).mono
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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
⊢ limsup (u * v) f ≤ limsup u f * limsup v f
have h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
Tactic: have h := IsCoboundedUnder.of_frequently_ge (a := 0)
    <| (h₁.and_eventually h₃).mono fun x ⟨ux_0, vx_0⟩ ↦ mul_nonneg ux_0 vx_0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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
⊢ limsup (u * v) f ≤ limsup u f * limsup v f
have h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
Tactic: have h' := isBoundedUnder_le_mul_of_nonneg h₁ h₂ h₃ h₄
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
have 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
Tactic: refine le_mul_of_forall_lt₀ fun a a_u b b_v ↦ (limsup_le_iff h h').2 fun c c_ab ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ ∀ᶠ (a : ι) in f, u a * v a < c
have h₅ : ∀ (x : ι) (x_a : u x < a) (x_b : v x < b) (v_0 : 0 x ≤ v x), u x * v x < 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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 x * v x < c
have apply : u x * v x ≤ a * b
Tactic: apply lt_of_le_of_lt _ c_ab
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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 x * v x ≤ a * b
have inl : ∀ (u_0 : u x < 0), u x * v x ≤ a * b
Tactic: rcases lt_or_ge (u x) 0 with u_0 | u_0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ u x * v x ≤ a * b
have inr : ∀ (u_0 : 0 ≤ u x), u x * v x ≤ a * b
Tactic: rcases lt_or_ge (u x) 0 with u_0 | u_0
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (goal)
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
⊢ u x * v x ≤ a * b
have inl : 0 ≤ a * b
Tactic: apply (mul_nonpos_of_nonpos_of_nonneg u_0.le v_0).trans
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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
⊢ liminf u f * liminf v f ≤ liminf (u * v) f
have h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f (u * v)
Tactic: have h := isCoboundedUnder_ge_mul_of_nonneg h₁ h₂ h₃ h₄
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.LiminfLimsup (hypothesis)
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)
⊢ liminf u f * liminf v f ≤ liminf (u * v) f
have h' : 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