awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ
hf : ¬IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f u
⊢ liminf u f = 0

Tactic:
limsInf_of_not_isBounded hf

Premises used: Filter.liminf, Real.limsInf_of_not_isBounded
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
simp : (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b) ↔ ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ x
⊢ (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (i : ι) ↦ (↑(u i) : ℝ)) ↔
    IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u

Tactic:
simp only [IsBoundedUnder, IsBounded, eventually_map, ← coe_le_coe, NNReal.exists, coe_mk]

Premises used: NNReal.coe_mk, Filter.IsBounded, Filter.eventually_map, NNReal.exists, Filter.IsBoundedUnder, NNReal.coe_le_coe
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
mp : (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b) → ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ x
mpr : (∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ x) → ∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b
⊢ (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b) ↔ ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ x

Tactic:
constructor
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b
⊢ 0 ≤ (↑b.toNNReal : ℝ)

Tactic:
simp
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b
h : ∀ (a : ι), (↑(u a) : ℝ) ≤ b → (↑(u a) : ℝ) ≤ (↑b.toNNReal : ℝ)
⊢ ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑b.toNNReal : ℝ)

Tactic:
filter_upwards [hb]
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b
⊢ ∀ (a : ι), (↑(u a) : ℝ) ≤ b → (↑(u a) : ℝ) ≤ (↑b.toNNReal : ℝ)

Tactic:
simp +contextual
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b
⊢ ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ x

Tactic:
exact ⟨b.toNNReal, by simp, by filter_upwards [hb]; simp +contextual⟩
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b
⊢ ∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b

Tactic:
⟨b, hb⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b
⊢ ∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ b

Tactic:
exact ⟨b, hb⟩
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
simp : (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b) ↔ ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ (↑(u a) : ℝ)
⊢ (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (i : ι) ↦ (↑(u i) : ℝ)) ↔
    IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u

Tactic:
simp only [IsBoundedUnder, IsBounded, eventually_map, ← coe_le_coe, NNReal.exists, coe_mk]

Premises used: NNReal.coe_mk, Filter.IsBounded, Filter.eventually_map, NNReal.exists, Filter.IsBoundedUnder, NNReal.coe_le_coe
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
mp : (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b) → ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ (↑(u a) : ℝ)
mpr : (∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ (↑(u a) : ℝ)) → ∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b
⊢ (∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b) ↔ ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ (↑(u a) : ℝ)

Tactic:
constructor
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b
⊢ 0 ≤ (↑b.toNNReal : ℝ)

Tactic:
simp
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b
⊢ ∀ᶠ (a : ι) in f, (↑b.toNNReal : ℝ) ≤ (↑(u a) : ℝ)

Tactic:
simpa
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b
⊢ ∃ (x : ℝ) (_ : 0 ≤ x), ∀ᶠ (a : ι) in f, x ≤ (↑(u a) : ℝ)

Tactic:
exact ⟨b.toNNReal, by simp, by simpa⟩
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, b ≤ (↑(u a) : ℝ)
⊢ ∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b

Tactic:
⟨b, hb⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, b ≤ (↑(u a) : ℝ)
⊢ ∃ (b : ℝ), ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ b

Tactic:
exact ⟨b, hb⟩
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst : f.NeBot
simp :
  (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a) ↔
    ∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
          (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)
⊢ (IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (i : ι) ↦ (↑(u i) : ℝ)) ↔
    IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u

Tactic:
simp only [IsCoboundedUnder, IsCobounded, eventually_map, ← coe_le_coe, NNReal.forall,
    NNReal.exists]

Premises used: Filter.IsCoboundedUnder, Filter.eventually_map, Filter.IsCobounded, NNReal.forall, NNReal.exists, NNReal.coe_le_coe
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst : f.NeBot
mp :
  (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a) →
    ∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
          (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)
mpr :
  (∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
          (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
    ∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a
⊢ (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a) ↔
    ∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
          (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)

Tactic:
constructor
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst : f.NeBot
b : ℝ
hb : ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a
⊢ 0 ≤ (↑b.toNNReal : ℝ)

Tactic:
simp
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst : f.NeBot
b : ℝ
hb : ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a
x : ℝ
h : 0 ≤ x
⊢ (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x h) : ℝ)) →
    (↑(NNReal.mk (↑b.toNNReal : ℝ) ⋯) : ℝ) ≤ (↑(NNReal.mk x h) : ℝ)

Tactic:
simpa [*] using hb _
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst : f.NeBot
b : ℝ
hb : ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a
⊢ ∃ (x : ℝ) (hx : 0 ≤ x),
    ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
      (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)) →
        (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk x_1 hx_1) : ℝ)

Tactic:
exact ⟨b.toNNReal, by simp, fun x _ ↦ by simpa [*] using hb _⟩
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst : f.NeBot
b : ℝ
hb₀ : 0 ≤ b
hb :
  ∀ (x : ℝ) (hx : 0 ≤ x),
    (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)) → (↑(NNReal.mk b hb₀) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)
x : ℝ
hx : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ x
⊢ 0 ≤ (↑(u (⋯.choose (p := fun (x_1 : ι) ↦ (↑(u x_1) : ℝ) ≤ x))) : ℝ)

Tactic:
simp
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst : f.NeBot
b : ℝ
hb₀ : 0 ≤ b
hb :
  ∀ (x : ℝ) (hx : 0 ≤ x),
    (∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)) → (↑(NNReal.mk b hb₀) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)
⊢ ∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≤ a) → b ≤ a

Tactic:
exact ⟨b, fun x hx ↦ hb _ (hx.exists.choose_spec.trans' (by simp)) hx⟩
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
simp :
  (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a) ↔
    ∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(u a) : ℝ)) →
          (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)
⊢ (IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (i : ι) ↦ (↑(u i) : ℝ)) ↔
    IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u

Tactic:
simp only [IsCoboundedUnder, IsCobounded, eventually_map, ← coe_le_coe, NNReal.forall,
    NNReal.exists]

Premises used: Filter.IsCoboundedUnder, Filter.eventually_map, Filter.IsCobounded, NNReal.forall, NNReal.exists, NNReal.coe_le_coe
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
mp :
  (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a) →
    ∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(u a) : ℝ)) →
          (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)
mpr :
  (∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(u a) : ℝ)) →
          (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)) →
    ∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a
⊢ (∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a) ↔
    ∃ (x : ℝ) (hx : 0 ≤ x),
      ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
        (∀ᶠ (a : ι) in f, (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(u a) : ℝ)) →
          (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)

Tactic:
constructor
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a
⊢ ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ 0

Tactic:
simp
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a
⊢ ∃ (x : ℝ) (hx : 0 ≤ x),
    ∀ (x_1 : ℝ) (hx_1 : 0 ≤ x_1),
      (∀ᶠ (a : ι) in f, (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(u a) : ℝ)) →
        (↑(NNReal.mk x_1 hx_1) : ℝ) ≤ (↑(NNReal.mk x hx) : ℝ)

Tactic:
exact ⟨b, hb _ (by simp), fun x _ ↦ hb _⟩
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb :
  ∀ (x : ℝ) (hx : 0 ≤ x),
    (∀ᶠ (a : ι) in f, (↑(NNReal.mk x hx) : ℝ) ≤ (↑(u a) : ℝ)) → (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk b hb₀) : ℝ)
⊢ ∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a

Tactic:
⟨b, fun x hx ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb :
  ∀ (x : ℝ) (hx : 0 ≤ x),
    (∀ᶠ (a : ι) in f, (↑(NNReal.mk x hx) : ℝ) ≤ (↑(u a) : ℝ)) → (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk b hb₀) : ℝ)
mpr : ∀ (x : ℝ) (hx : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ x), b ≥ x
⊢ ∃ (b : ℝ), ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, (↑(u a_1) : ℝ) ≥ a) → b ≥ a

Tactic:
refine ⟨b, fun x hx ↦ ?_⟩
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb :
  ∀ (x : ℝ) (hx : 0 ≤ x),
    (∀ᶠ (a : ι) in f, (↑(NNReal.mk x hx) : ℝ) ≤ (↑(u a) : ℝ)) → (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk b hb₀) : ℝ)
x : ℝ
hx : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ x
mpr : ∀ (hx₀ : x ≤ 0), b ≥ x
mpr₁ : ∀ (hx₀ : 0 ≤ x), b ≥ x
⊢ b ≥ x

Tactic:
obtain hx₀ | hx₀ := le_total x 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb :
  ∀ (x : ℝ) (hx : 0 ≤ x),
    (∀ᶠ (a : ι) in f, (↑(NNReal.mk x hx) : ℝ) ≤ (↑(u a) : ℝ)) → (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk b hb₀) : ℝ)
x : ℝ
hx : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ x
hx₀ : x ≤ 0
⊢ b ≥ x

Tactic:
hx₀.trans hb₀

Premises used: LE.le.trans
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb :
  ∀ (x : ℝ) (hx : 0 ≤ x),
    (∀ᶠ (a : ι) in f, (↑(NNReal.mk x hx) : ℝ) ≤ (↑(u a) : ℝ)) → (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk b hb₀) : ℝ)
x : ℝ
hx : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ x
hx₀ : x ≤ 0
⊢ b ≥ x

Tactic:
exact hx₀.trans hb₀

Premises used: LE.le.trans
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb :
  ∀ (x : ℝ) (hx : 0 ≤ x),
    (∀ᶠ (a : ι) in f, (↑(NNReal.mk x hx) : ℝ) ≤ (↑(u a) : ℝ)) → (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk b hb₀) : ℝ)
x : ℝ
hx : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ x
hx₀ : 0 ≤ x
⊢ b ≥ x

Tactic:
hb _ hx₀ hx

Premises used: NNReal.toReal
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb :
  ∀ (x : ℝ) (hx : 0 ≤ x),
    (∀ᶠ (a : ι) in f, (↑(NNReal.mk x hx) : ℝ) ≤ (↑(u a) : ℝ)) → (↑(NNReal.mk x hx) : ℝ) ≤ (↑(NNReal.mk b hb₀) : ℝ)
x : ℝ
hx : ∀ᶠ (a : ι) in f, (↑(u a) : ℝ) ≥ x
hx₀ : 0 ≤ x
⊢ b ≥ x

Tactic:
exact hb _ hx₀ hx
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
f : Filter ℝ≥0
hf : ¬IsBounded (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f
⊢ Eq (α := ℝ≥0) (sInf ∅) 0

Tactic:
sInf_empty

Premises used: NNReal.sInf_empty
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
f : Filter ℝ≥0
hf : ¬IsBounded (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f
h : Eq (α := Set ℝ≥0) {a : ℝ≥0 | ∀ᶠ (n : ℝ≥0) in f, n ≤ a} ∅
⊢ Eq (α := ℝ≥0) (sInf {a : ℝ≥0 | ∀ᶠ (n : ℝ≥0) in f, n ≤ a}) ⊥

Tactic:
convert! sInf_empty

Premises used: NNReal.sInf_empty
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
f : Filter ℝ≥0
hf : ¬IsBounded (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f
⊢ Eq (α := Set ℝ≥0) {a : ℝ≥0 | ∀ᶠ (n : ℝ≥0) in f, n ≤ a} ∅

Tactic:
simpa [Set.eq_empty_iff_forall_notMem, IsBounded] using hf

Premises used: Filter.IsBounded, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
f : Filter ℝ≥0
hf : ¬IsCobounded (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f
rwa : Eq (α := ℝ≥0) (sSup {a : ℝ≥0 | ∀ᶠ (n : ℝ≥0) in f, a ≤ n}) 0
rwa₁ : Eq (α := ℝ≥0) 0 0
rwa₂ : ¬BddAbove (α := ℝ≥0) {a : ℝ≥0 | ∀ᶠ (n : ℝ≥0) in f, a ≤ n}
rwa₃ : Eq (α := ℝ≥0) 0 0
rwa₄ rwa₅ rwa₆ : ¬BddAbove (α := ℝ≥0) {a : ℝ≥0 | ∀ᶠ (n : ℝ≥0) in f, a ≤ n}
⊢ f.limsInf = 0

Tactic:
rwa [limsInf, sSup_of_not_bddAbove]

Premises used: Filter.limsInf, NNReal.sSup_of_not_bddAbove
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : ¬IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
⊢ limsup u f = 0

Tactic:
limsSup_of_not_isBounded hf

Premises used: Filter.limsup, NNReal.limsSup_of_not_isBounded
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : ¬IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
⊢ liminf u f = 0

Tactic:
limsInf_of_not_isCobounded hf

Premises used: NNReal.limsInf_of_not_isCobounded, Filter.liminf
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
pos :
  ∀ (hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u),
    liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(liminf u f) : ℝ)
neg :
  ∀ (hf : ¬IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u),
    liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(liminf u f) : ℝ)
⊢ liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(liminf u f) : ℝ)

Tactic:
by_cases hf : f.IsCoboundedUnder (· ≥ ·) u

Premises used: Filter.IsCoboundedUnder, GE.ge
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : ¬IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
⊢ liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(liminf u f) : ℝ)

Tactic:
simp [*]
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
⊢ liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(liminf u f) : ℝ)

Tactic:
eq_of_forall_le_iff fun c ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
pos : ∀ (c : ℝ), c ≤ liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f ↔ c ≤ (↑(liminf u f) : ℝ)
⊢ liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(liminf u f) : ℝ)

Tactic:
refine eq_of_forall_le_iff fun c ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
c : ℝ
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) f fun (i : ι) ↦ (↑(u i) : ℝ)

Tactic:
simpa
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
c : ℝ
⊢ ∀ᶠ (x : ℝ) in map (fun (i : ι) ↦ (↑(u i) : ℝ)) f, (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) x 0

Tactic:
simp
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
c : ℝ
pos : (∀ y < c, ∀ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ y < c.toNNReal, ∀ᶠ (a : ι) in f, y < u a
⊢ c ≤ liminf (fun (i : ι) ↦ (↑(u i) : ℝ)) f ↔ c ≤ (↑(liminf u f) : ℝ)

Tactic:
rw [← Real.toNNReal_le_iff_le_coe, le_liminf_iff (by simpa) ⟨0, by simp⟩, le_liminf_iff]

Premises used: Exists.intro, Real.toNNReal_le_iff_le_coe, OfNat.ofNat, Filter.le_liminf_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
c : ℝ
pos :
  (∀ y < c, ∀ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ (x : ℝ) (b : x < c) (a : 0 ≤ x), ∀ᶠ (a : ι) in f, x < (↑(u a) : ℝ)
⊢ (∀ y < c, ∀ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ y < c.toNNReal, ∀ᶠ (a : ι) in f, y < u a

Tactic:
simp only [← coe_lt_coe, Real.coe_toNNReal', lt_sup_iff, or_imp, isEmpty_Prop, not_lt,
    zero_le_coe, IsEmpty.forall_iff, and_true, NNReal.forall, coe_mk, forall_comm (α := _ ≤ _)]

Premises used: and_true, Real.coe_toNNReal', forall_comm, NNReal.coe_mk, or_imp, lt_sup_iff, not_lt, NNReal.forall, NNReal.coe_lt_coe, NNReal.zero_le_coe, isEmpty_Prop, IsEmpty.forall_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
c : ℝ
⊢ (∀ y < c, ∀ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ (x : ℝ) (b : x < c) (a : 0 ≤ x), ∀ᶠ (a : ι) in f, x < (↑(u a) : ℝ)

Tactic:
forall₂_congr fun r hr ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
c : ℝ
pos : ∀ (r : ℝ) (hr : r < c), (∀ᶠ (a : ι) in f, r < (↑(u a) : ℝ)) ↔ ∀ (a : 0 ≤ r), ∀ᶠ (a : ι) in f, r < (↑(u a) : ℝ)
⊢ (∀ y < c, ∀ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ (x : ℝ) (b : x < c) (a : 0 ≤ x), ∀ᶠ (a : ι) in f, x < (↑(u a) : ℝ)

Tactic:
refine forall₂_congr fun r hr ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
c r : ℝ
hr_1 : r < c
hr : r < 0
i : ι
⊢ 0 ≤ (↑(u i) : ℝ)

Tactic:
simp
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) f u
c r : ℝ
hr : r < c
⊢ (∀ᶠ (a : ι) in f, r < (↑(u a) : ℝ)) ↔ ∀ (a : 0 ≤ r), ∀ᶠ (a : ι) in f, r < (↑(u a) : ℝ)

Tactic:
simpa using (le_or_gt 0 r).imp_right fun hr ↦ .of_forall fun i ↦ hr.trans_le (by simp)

Premises used: le_or_gt, OfNat.ofNat, Or.imp_right
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inl : limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) ⊥ = (↑(limsup u ⊥) : ℝ)
inr : ∀ (hf : f.NeBot), limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
⊢ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)

Tactic:
obtain rfl | hf := f.eq_or_neBot

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
u : ι → ℝ≥0
⊢ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) ⊥ = (↑(limsup u ⊥) : ℝ)

Tactic:
simp [limsup, limsSup]

Premises used: Filter.limsSup, Filter.limsup
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : f.NeBot
pos :
  ∀ (hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u), limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
neg :
  ∀ (hf : ¬IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u),
    limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)
⊢ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)

Tactic:
by_cases hf : f.IsBoundedUnder (· ≤ ·) u

Premises used: LE.le, Filter.IsBoundedUnder
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : ¬IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
⊢ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)

Tactic:
simp [*]
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u

Tactic:
isBoundedDefault
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u

Tactic:
have : f.IsCoboundedUnder (· ≤ ·) u := by isBoundedDefault
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
⊢ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)

Tactic:
eq_of_forall_le_iff fun c ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
pos : ∀ (c : ℝ), c ≤ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f ↔ c ≤ (↑(limsup u f) : ℝ)
⊢ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f = (↑(limsup u f) : ℝ)

Tactic:
refine eq_of_forall_le_iff fun c ↦ ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
c : ℝ
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (i : ι) ↦ (↑(u i) : ℝ)

Tactic:
simpa
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
c : ℝ
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (i : ι) ↦ (↑(u i) : ℝ)

Tactic:
simpa
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
c : ℝ
pos : (∀ y < c, ∃ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ y < c.toNNReal, ∃ᶠ (a : ι) in f, y < u a
⊢ c ≤ limsup (fun (i : ι) ↦ (↑(u i) : ℝ)) f ↔ c ≤ (↑(limsup u f) : ℝ)

Tactic:
rw [← Real.toNNReal_le_iff_le_coe, le_limsup_iff (by simpa) (by simpa), le_limsup_iff ‹_›]

Premises used: Filter.le_limsup_iff, Real.toNNReal_le_iff_le_coe
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
c : ℝ
pos :
  (∀ y < c, ∃ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ (x : ℝ) (b : x < c) (a : 0 ≤ x), ∃ᶠ (a : ι) in f, x < (↑(u a) : ℝ)
⊢ (∀ y < c, ∃ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ y < c.toNNReal, ∃ᶠ (a : ι) in f, y < u a

Tactic:
simp only [← coe_lt_coe, Real.coe_toNNReal', lt_sup_iff, or_imp, isEmpty_Prop, not_lt,
    zero_le_coe, IsEmpty.forall_iff, and_true, NNReal.forall, coe_mk, forall_comm (α := _ ≤ _)]

Premises used: and_true, Real.coe_toNNReal', forall_comm, NNReal.coe_mk, or_imp, lt_sup_iff, not_lt, NNReal.forall, NNReal.coe_lt_coe, NNReal.zero_le_coe, isEmpty_Prop, IsEmpty.forall_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
c : ℝ
⊢ (∀ y < c, ∃ᶠ (a : ι) in f, y < (↑(u a) : ℝ)) ↔ ∀ (x : ℝ) (b : x < c) (a : 0 ≤ x), ∃ᶠ (a : ι) in f, x < (↑(u a) : ℝ)

Tactic:
forall₂_congr fun r hr ↦ ?_

Premises used: forall₂_congr