awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
u_bdd_ge : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f u
v_bdd_ge : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f v
⊢ IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
have obtain : ∀ (U : R) (hU : ∀ᶠ (x : R) in map u f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x U),
  IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
Tactic: obtain ⟨U, hU⟩ := u_bdd_ge
Cleared hypotheses: u_bdd_ge
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
v_bdd_ge : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f v
U : R
hU : ∀ᶠ (x : R) in map u f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x U
⊢ IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
have obtain : ∀ (V : R) (hV : ∀ᶠ (x : R) in map v f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x V),
  IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
Tactic: obtain ⟨V, hV⟩ := v_bdd_ge
Cleared hypotheses: v_bdd_ge
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
U : R
hU : ∀ᶠ (x : R) in map u f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x U
V : R
hV : ∀ᶠ (x : R) in map v f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x V
⊢ IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
have h : ∀ᶠ (x : R) in map (u + v) f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x (U + V)
Tactic: use U + V
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
U : R
hU : ∀ᶠ (x : R) in map u f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x U
V : R
hV : ∀ᶠ (x : R) in map v f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x V
⊢ ∀ᶠ (x : R) in map (u + v) f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x (U + V)
have h : ∀ (hU : ∀ᶠ (a : α) in f, u a ≥ U) (hV : ∀ᶠ (a : α) in f, v a ≥ V), ∀ᶠ (a : α) in f, u a + v a ≥ U + V
Tactic: simp only [eventually_map, Pi.add_apply] at hU hV ⊢
Cleared hypotheses: hU, hV
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
U V : R
hU : ∀ᶠ (a : α) in f, u a ≥ U
hV : ∀ᶠ (a : α) in f, v a ≥ V
⊢ ∀ᶠ (a : α) in f, u a + v a ≥ U + V
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ u a ≥ U) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ v a ≥ V) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ u a + v a ≥ U + V) x} x}
          x}
    a
Tactic: filter_upwards [hU, hV] with a hu hv using add_le_add hu hv
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
U V : R
hU : ∀ᶠ (a : α) in f, u a ≥ U
hV : ∀ᶠ (a : α) in f, v a ≥ V
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ u a ≥ U) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ v a ≥ V) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ u a + v a ≥ U + V) x} x}
            x}
      a
⊢ ∀ᶠ (a : α) in f, u a + v a ≥ U + V
have h₁ : ∀ (a : α), u a ≥ U → v a ≥ V → u a + v a ≥ U + V
Tactic: filter_upwards [hU, hV] with a hu hv using add_le_add hu hv
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
u_bdd_le : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f u
v_bdd_le : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f v
⊢ IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)
have obtain : ∀ (U : R) (hU : ∀ᶠ (x : R) in map u f, (fun (x1 x2 : R) ↦ x1 ≤ x2) x U),
  IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)
Tactic: obtain ⟨U, hU⟩ := u_bdd_le
Cleared hypotheses: u_bdd_le
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
v_bdd_le : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : R) in map u f, (fun (x1 x2 : R) ↦ x1 ≤ x2) x U
⊢ IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)
have obtain : ∀ (V : R) (hV : ∀ᶠ (x : R) in map v f, (fun (x1 x2 : R) ↦ x1 ≤ x2) x V),
  IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)
Tactic: obtain ⟨V, hV⟩ := v_bdd_le
Cleared hypotheses: v_bdd_le
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
U : R
hU : ∀ᶠ (x : R) in map u f, (fun (x1 x2 : R) ↦ x1 ≤ x2) x U
V : R
hV : ∀ᶠ (x : R) in map v f, (fun (x1 x2 : R) ↦ x1 ≤ x2) x V
⊢ IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)
have h : ∀ᶠ (x : R) in map (u + v) f, (fun (x1 x2 : R) ↦ x1 ≤ x2) x (U + V)
Tactic: use U + V
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
U : R
hU : ∀ᶠ (x : R) in map u f, (fun (x1 x2 : R) ↦ x1 ≤ x2) x U
V : R
hV : ∀ᶠ (x : R) in map v f, (fun (x1 x2 : R) ↦ x1 ≤ x2) x V
⊢ ∀ᶠ (x : R) in map (u + v) f, (fun (x1 x2 : R) ↦ x1 ≤ x2) x (U + V)
have h : ∀ (hU : ∀ᶠ (a : α) in f, u a ≤ U) (hV : ∀ᶠ (a : α) in f, v a ≤ V), ∀ᶠ (a : α) in f, u a + v a ≤ U + V
Tactic: simp only [eventually_map, Pi.add_apply] at hU hV ⊢
Cleared hypotheses: hU, hV
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
U V : R
hU : ∀ᶠ (a : α) in f, u a ≤ U
hV : ∀ᶠ (a : α) in f, v a ≤ V
⊢ ∀ᶠ (a : α) in f, u a + v a ≤ U + V
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ u a ≤ U) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ v a ≤ V) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ u a + v a ≤ U + V) x} x}
          x}
    a
Tactic: filter_upwards [hU, hV] with a hu hv using add_le_add hu hv
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
U V : R
hU : ∀ᶠ (a : α) in f, u a ≤ U
hV : ∀ᶠ (a : α) in f, v a ≤ V
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ u a ≤ U) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ v a ≤ V) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ u a + v a ≤ U + V) x} x}
            x}
      a
⊢ ∀ᶠ (a : α) in f, u a + v a ≤ U + V
have h₁ : ∀ (a : α), u a ≤ U → v a ≤ V → u a + v a ≤ U + V
Tactic: filter_upwards [hU, hV] with a hu hv using add_le_add hu hv
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f v
⊢ IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
have obtain : ∀ (U : R) (hU : ∀ᶠ (x : α) in f, u x ≤ U), IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
Tactic: obtain ⟨U, hU⟩ := hu.eventually_le
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, u x ≤ U
⊢ IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
have obtain : ∀ (V : R) (hV : ∃ᶠ (x : α) in f, v x ≤ V), IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
Tactic: obtain ⟨V, hV⟩ := hv.frequently_le
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, u x ≤ U
V : R
hV : ∃ᶠ (x : α) in f, v x ≤ V
⊢ IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
have apply : ∃ᶠ (x : α) in f, (u + v) x ≤ U + V
Tactic: apply IsCoboundedUnder.of_frequently_le (a := U + V)
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)
have obtain : ∀ (U : R) (hU : ∀ᶠ (x : α) in f, U ≤ u x), IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)
Tactic: obtain ⟨U, hU⟩ := hu.eventually_ge
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, U ≤ u x
⊢ IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)
have obtain : ∀ (V : R) (hV : ∃ᶠ (x : α) in f, V ≤ v x), IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)
Tactic: obtain ⟨V, hV⟩ := hv.frequently_ge
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, U ≤ u x
V : R
hV : ∃ᶠ (x : α) in f, V ≤ v x
⊢ IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)
have apply : ∃ᶠ (x : α) in f, U + V ≤ (u + v) x
Tactic: apply IsCoboundedUnder.of_frequently_ge (a := U + V)
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
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
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u * v)
have obtain : ∀ (U : α) (hU : ∀ᶠ (x : ι) in f, u x ≤ U), IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u * v)
Tactic: obtain ⟨U, hU⟩ := h₂.eventually_le
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u * v)
have obtain : ∀ (V : α) (hV : ∀ᶠ (x : ι) in f, v x ≤ V), IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u * v)
Tactic: obtain ⟨V, hV⟩ := h₄.eventually_le
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u * v)
have refine : ∀ᶠ (x : ι) in f, (u * v) x ≤ U * V
Tactic: refine isBoundedUnder_of_eventually_le (a := U * V) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
⊢ ∀ᶠ (x : ι) in f, (u * v) x ≤ U * V
have h : ∀ (x : ι) (x_U : u x ≤ U) (x_V : v x ≤ V) (v_0 : 0 x ≤ v x), (u * v) x ≤ U * V
Tactic: filter_upwards [hU, hV, h₃] with x x_U x_V v_0
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
⊢ 0 ≤ U
have obtain : ∀ (y : ι) (y_0 : 0 ≤ u y) (y_U : u y ≤ U), 0 ≤ U
Tactic: obtain ⟨y, y_0, y_U⟩ := (h₁.and_eventually hU).exists
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (hypothesis)
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
⊢ (u * v) x ≤ U * V
have U_0 : 0 ≤ U
Tactic: have U_0 : 0 ≤ U := by
    obtain ⟨y, y_0, y_U⟩ := (h₁.and_eventually hU).exists
    exact y_0.trans y_U
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
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)
have obtain : ∀ (U : α) (hU : ∀ᶠ (x : ι) in f, u x ≤ U), IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u * v)
Tactic: obtain ⟨U, hU⟩ := h₂.eventually_le
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u * v)
have obtain : ∀ (V : α) (hV : ∃ᶠ (x : ι) in f, v x ≤ V), IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u * v)
Tactic: obtain ⟨V, hV⟩ := h₄.frequently_le
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u * v)
have refine : ∃ᶠ (x : ι) in f, (u * v) x ≤ U * V
Tactic: refine IsCoboundedUnder.of_frequently_le (a := U * V) ?_
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
⊢ ∃ᶠ (x : ι) in f, (u * v) x ≤ U * V
have apply : ∀ (x : ι), v x ≤ V ∧ u x ≤ U ∧ 0 x ≤ u x ∧ 0 x ≤ v x → (u * v) x ≤ U * V
Tactic: apply (hV.and_eventually (hU.and (h₁.and h₃))).mono
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
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
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
x : ι
⊢ v x ≤ V ∧ u x ≤ U ∧ 0 x ≤ u x ∧ 0 x ≤ v x → (u * v) x ≤ U * V
have this : ∀ (x_V : v x ≤ V) (x_U : u x ≤ U) (u_0 : 0 x ≤ u x) (v_0 : 0 x ≤ v x), (u * v) x ≤ U * V
Tactic: ⟨x_V, x_U, u_0, v_0⟩
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
f : Filter β
u v : β → α
bu : α
hu : ∀ᶠ (x : β) in f, u x ≤ bu
bv : α
hv : ∀ᶠ (x : β) in f, v x ≤ bv
⊢ ∀ᶠ (x : β) in f, u x ⊔ v x ≤ bu ⊔ bv
have h : ∀ (a : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ u x ≤ bu) x} x →
        Membership.mem (γ := Set β)
          {x : β |
            Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ v x ≤ bv) x} x →
              Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ u x ⊔ v x ≤ bu ⊔ bv) x} x}
          x}
    a
Tactic: filter_upwards [hu, hv] with _ using sup_le_sup
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
f : Filter β
u v : β → α
bu : α
hu : ∀ᶠ (x : β) in f, u x ≤ bu
bv : α
hv : ∀ᶠ (x : β) in f, v x ≤ bv
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ u x ≤ bu) x} x →
          Membership.mem (γ := Set β)
            {x : β |
              Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ v x ≤ bv) x} x →
                Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ u x ⊔ v x ≤ bu ⊔ bv) x} x}
            x}
      a
⊢ ∀ᶠ (x : β) in f, u x ⊔ v x ≤ bu ⊔ bv
have h₁ : ∀ (a : β), u a ≤ bu → v a ≤ bv → u a ⊔ v a ≤ bu ⊔ bv
Tactic: filter_upwards [hu, hv] with _ using sup_le_sup
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) l (g ∘ f) ↔ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f
have refine : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) l (g ∘ f) → IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f
Tactic: refine ⟨?_, fun h => h.isBoundedUnder (α := β) hg⟩
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (x : γ) in map (g ∘ f) l, (fun (x1 x2 : γ) ↦ x1 ≤ x2) x c
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f
have hc₁ : ∀ᶠ (a : α) in l, (fun (x1 x2 : γ) ↦ x1 ≤ x2) ((g ∘ f) a) c
Tactic: rw [eventually_map] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun (x1 x2 : γ) ↦ x1 ≤ x2) ((g ∘ f) a) c
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f
have obtain : ∀ (b : β) (hb : ∀ a ≥ b, c < g a), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f
Tactic: obtain ⟨b, hb⟩ : ∃ b, ∀ a ≥ b, c < g a := eventually_atTop.1 (hg'.eventually_gt_atTop c)
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
h : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u ∨ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
have inl : ∀ (h' : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u),
  IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
Tactic: rcases h with (h' | h')
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
h : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u ∨ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
inl :
  ∀ (h' : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u),
    IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
have inr : ∀ (h' : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v),
  IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
Tactic: rcases h with (h' | h')
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
have inl : ∀ (b : β) (hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a),
  IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
Tactic: rcases h' with ⟨b, hb⟩
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
have h : ∀ (a : β),
  (∀ᶠ (x : β) in map (fun (a : α) ↦ max (u a) (v a)) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) →
    (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
Tactic: use b
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun (a : α) ↦ max (u a) (v a)) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
⊢ b ≤ c
have h : ∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
Tactic: apply hb c
-- Lean 4 proof step from Mathlib.Order.Filter.IsBounded (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun (a : α) ↦ max (u a) (v a)) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
⊢ ∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
have h : ∀ (hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u a) (v a)) c),
  ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (u a) c
Tactic: rw [eventually_map] at hc ⊢
Cleared hypotheses: hc