awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∀ (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_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : 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_1 : f.NeBot
hf : IsBoundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≤ x2) f u
this : 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 α
inst : CountableInterFilter f
u : α → ℝ≥0∞
⊢ ∀ᶠ (y : α) in f, u y ≤ limsup u f

Tactic:
_root_.eventually_le_limsup

Premises used: eventually_le_limsup
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
⊢ limsup u f = 0 ↔ u =ᶠ[f] 0

Tactic:
limsup_eq_bot

Premises used: limsup_eq_bot
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
pos : ∀ (ha₀ : a = 0), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
neg : ∀ (ha₀ : ¬a = 0), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f

Tactic:
by_cases ha₀ : a = 0
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
pos : Eq (α := ℝ≥0∞) (limsup (fun (x : α) ↦ ⊥) f) ⊥
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f

Tactic:
simp_rw [ha₀, zero_mul, ← ENNReal.bot_eq_zero]

Premises used: MulZeroClass.zero_mul, ENNReal.bot_eq_zero
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ Eq (α := ℝ≥0∞) (limsup (fun (x : α) ↦ ⊥) f) ⊥

Tactic:
limsup_const_bot

Premises used: Filter.limsup_const_bot
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ Eq (α := ℝ≥0∞) (limsup (fun (x : α) ↦ ⊥) f) ⊥

Tactic:
exact limsup_const_bot

Premises used: Filter.limsup_const_bot
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : ¬a = 0
g_iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ a * x) ⋯ ⋯
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f

Tactic:
g_iso.limsup_apply.symm

Premises used: OrderIso.limsup_apply, Eq.symm
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : ¬a = 0
g_iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ a * x) ⋯ ⋯
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f

Tactic:
exact g_iso.limsup_apply.symm

Premises used: OrderIso.limsup_apply, Eq.symm
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
⊢ limsup (fun (x : α) ↦ u x * a) f = a * limsup u f

Tactic:
simpa [mul_comm] using limsup_const_mul_of_ne_top ha_top

Premises used: ENNReal.limsup_const_mul_of_ne_top, mul_comm
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha_top : a ≠ ∞
g_iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ a * x) ⋯ ⋯
⊢ liminf (fun (x : α) ↦ a * u x) f = a * liminf u f

Tactic:
g_iso.liminf_apply.symm

Premises used: OrderIso.liminf_apply, Eq.symm
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha_top : a ≠ ∞
g_iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective (fun (x : ℝ≥0∞) ↦ a * x) ⋯ ⋯
⊢ liminf (fun (x : α) ↦ a * u x) f = a * liminf u f

Tactic:
exact g_iso.liminf_apply.symm

Premises used: OrderIso.liminf_apply, Eq.symm
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha_top : a ≠ ∞
⊢ liminf (fun (x : α) ↦ u x * a) f = a * liminf u f

Tactic:
simpa [mul_comm] using liminf_const_mul_of_ne_zero_of_ne_top ha₀ ha_top

Premises used: mul_comm, ENNReal.liminf_const_mul_of_ne_zero_of_ne_top
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
pos : ∀ (ha₀ : a = 0), liminf (fun (x : α) ↦ a * u x) f = a * liminf u f
neg : ∀ (ha₀ : ¬a = 0), liminf (fun (x : α) ↦ a * u x) f = a * liminf u f
⊢ liminf (fun (x : α) ↦ a * u x) f = a * liminf u f

Tactic:
by_cases ha₀ : a = 0
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
pos : Eq (α := ℝ≥0∞) (liminf (fun (x : α) ↦ ⊥) f) ⊥
⊢ liminf (fun (x : α) ↦ a * u x) f = a * liminf u f

Tactic:
simp_rw [ha₀, zero_mul, ← ENNReal.bot_eq_zero]

Premises used: MulZeroClass.zero_mul, ENNReal.bot_eq_zero
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ Eq (α := ℝ≥0∞) (liminf (fun (x : α) ↦ ⊥) f) ⊥

Tactic:
apply liminf_const

Premises used: Filter.liminf_const
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : ¬a = 0
⊢ liminf (fun (x : α) ↦ a * u x) f = a * liminf u f

Tactic:
liminf_const_mul_of_ne_zero_of_ne_top ha₀ ha_top

Premises used: ENNReal.liminf_const_mul_of_ne_zero_of_ne_top
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : ¬a = 0
⊢ liminf (fun (x : α) ↦ a * u x) f = a * liminf u f

Tactic:
exact liminf_const_mul_of_ne_zero_of_ne_top ha₀ ha_top

Premises used: ENNReal.liminf_const_mul_of_ne_zero_of_ne_top
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
⊢ liminf (fun (x : α) ↦ u x * a) f = a * liminf u f

Tactic:
simpa [mul_comm] using liminf_const_mul_of_ne_top ha_top

Premises used: ENNReal.liminf_const_mul_of_ne_top, mul_comm
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
pos : ∀ (ha_top : a ≠ ∞), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
neg : ∀ (ha_top : a = ∞), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f

Tactic:
by_cases! ha_top : a ≠ ⊤
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f

Tactic:
limsup_const_mul_of_ne_top ha_top

Premises used: ENNReal.limsup_const_mul_of_ne_top
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f

Tactic:
exact limsup_const_mul_of_ne_top ha_top

Premises used: ENNReal.limsup_const_mul_of_ne_top
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
pos : ∀ (hu : u =ᶠ[f] 0), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
neg : ∀ (hu : ¬u =ᶠ[f] 0), limsup (fun (x : α) ↦ a * u x) f = a * limsup u f
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f

Tactic:
by_cases hu : u =ᶠ[f] 0
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : u =ᶠ[f] 0
x : α
hx : u x = 0 x
⊢ Eq (α := ℝ≥0∞) ((fun (x : α) ↦ a * u x) x) (0 x)

Tactic:
simp [hx]
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : u =ᶠ[f] 0
⊢ f.EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ a * u x) 0

Tactic:
have hau : (a * u ·) =ᶠ[f] 0 := hu.mono fun x hx => by simp [hx]
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : u =ᶠ[f] 0
hau : f.EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ a * u x) 0
pos : ⊥ = a * ⊥
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f

Tactic:
simp only [limsup_congr hu, limsup_congr hau, Pi.zero_def, ← ENNReal.bot_eq_zero,
      limsup_const_bot]

Premises used: ENNReal.bot_eq_zero, Pi.zero_def, Filter.limsup_const_bot, Filter.limsup_congr
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : u =ᶠ[f] 0
hau : f.EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ a * u x) 0
⊢ ⊥ = a * ⊥

Tactic:
simp
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
⊢ ∃ᶠ (x : α) in f, ¬u x = 0 x

Tactic:
rw [EventuallyEq, not_eventually] at hu

Premises used: Filter.EventuallyEq, Filter.not_eventually
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ∃ᶠ (x : α) in f, ¬u x = 0 x
x : α
hx : ¬u x = 0 x
⊢ LE.le (α := ℝ≥0∞) ∞ (if u x = 0 then 0 else ∞)

Tactic:
simpa
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ∃ᶠ (x : α) in f, ¬u x = 0 x
⊢ ∃ᶠ (x : α) in f, LE.le (α := ℝ≥0∞) ∞ (if u x = 0 then 0 else ∞)

Tactic:
exact hu.mono fun x hx => by simpa

Premises used: Filter.Frequently.mono
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
⊢ ∃ᶠ (x : α) in f, LE.le (α := ℝ≥0∞) ∞ (if u x = 0 then 0 else ∞)

Tactic:
have hu_mul : ∃ᶠ x : α in f, ⊤ ≤ ite (u x = 0) (0 : ℝ≥0∞) ⊤ := by
      rw [EventuallyEq, not_eventually] at hu
      exact hu.mono fun x hx => by simpa
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, LE.le (α := ℝ≥0∞) ∞ (if u x = 0 then 0 else ∞)
⊢ Eq (α := ℝ≥0∞) (limsup (fun (x : α) ↦ if u x = 0 then 0 else ∞) f) ∞

Tactic:
have h_top_le : (f.limsup fun x : α => ite (u x = 0) (0 : ℝ≥0∞) ⊤) = ⊤ :=
      eq_top_iff.mpr (le_limsup_of_frequently_le hu_mul)
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, LE.le (α := ℝ≥0∞) ∞ (if u x = 0 then 0 else ∞)
h_top_le : Eq (α := ℝ≥0∞) (limsup (fun (x : α) ↦ if u x = 0 then 0 else ∞) f) ∞
⊢ limsup u f ≠ 0

Tactic:
have hfu : f.limsup u ≠ 0 := mt limsup_eq_bot.1 hu
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, LE.le (α := ℝ≥0∞) ∞ (if u x = 0 then 0 else ∞)
h_top_le : Eq (α := ℝ≥0∞) (limsup (fun (x : α) ↦ if u x = 0 then 0 else ∞) f) ∞
hfu : limsup u f ≠ 0
⊢ limsup (fun (x : α) ↦ a * u x) f = a * limsup u f

Tactic:
simp [ha_top, top_mul', h_top_le, hfu]

Premises used: ENNReal.top_mul'
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
⊢ limsup (fun (x : α) ↦ u x * a) f = a * limsup u f

Tactic:
simpa [mul_comm] using limsup_const_mul

Premises used: ENNReal.limsup_const_mul, mul_comm
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u v : α → ℝ≥0∞
⊢ limsup (u * v) f ≤ limsup (fun (x : α) ↦ limsup u f * v x) f

Tactic:
limsup_le_limsup ?_

Premises used: Filter.limsup_le_limsup
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u v : α → ℝ≥0∞
refine : u * v ≤ᶠ[f] fun (x : α) ↦ limsup u f * v x
⊢ limsup (u * v) f ≤ limsup (fun (x : α) ↦ limsup u f * v x) f

Tactic:
refine limsup_le_limsup ?_

Premises used: Filter.limsup_le_limsup
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u v : α → ℝ≥0∞
x : α
hx : u x ≤ limsup u f
⊢ (u * v) x ≤ limsup u f * v x

Tactic:
mul_le_mul' hx le_rfl

Premises used: le_rfl, mul_le_mul'
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u v : α → ℝ≥0∞
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (y : α) ↦ u y ≤ limsup u f) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (u * v) x ≤ (fun (x : α) ↦ limsup u f * v x) x) x} x}
      a
h₁ h₂ : ∀ (x : α) (hx : u x ≤ limsup u f), (u * v) x ≤ limsup u f * v x
⊢ u * v ≤ᶠ[f] fun (x : α) ↦ limsup u f * v x

Tactic:
filter_upwards [@eventually_le_limsup _ f _ u] with x hx using mul_le_mul' hx le_rfl

Premises used: ENNReal.eventually_le_limsup
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : CountableInterFilter f
u v : α → ℝ≥0∞
⊢ limsup (u + v) f ≤ limsup u f + limsup v f

Tactic:
sInf_le ((eventually_le_limsup u).mp
    ((eventually_le_limsup v).mono fun _ hxg hxf => add_le_add hxf hxg))

Premises used: Filter.limsSup, add_le_add, Filter.limsup, Filter.Eventually.mono, Filter.Eventually.mp, sInf_le, ENNReal.eventually_le_limsup
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
β : Type u_2
inst : Countable β
f : Filter α
inst_1 : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
rw : ∀ (i : β), ∀ᶠ (x : α) in f, u x i ≤ limsup (fun (a' : α) ↦ u a' i) f
⊢ ∀ᶠ (a : α) in f, ∀ (b : β), u a b ≤ limsup (fun (a' : α) ↦ u a' b) f

Tactic:
rw [eventually_countable_forall]

Premises used: eventually_countable_forall
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
β : Type u_2
inst : Countable β
f : Filter α
inst_1 : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ (i : β), ∀ᶠ (x : α) in f, u x i ≤ limsup (fun (a' : α) ↦ u a' i) f

Tactic:
fun b => ENNReal.eventually_le_limsup fun a => u a b

Premises used: ENNReal.eventually_le_limsup
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
β : Type u_2
inst : Countable β
f : Filter α
inst_1 : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ (i : β), ∀ᶠ (x : α) in f, u x i ≤ limsup (fun (a' : α) ↦ u a' i) f

Tactic:
exact fun b => ENNReal.eventually_le_limsup fun a => u a b

Premises used: ENNReal.eventually_le_limsup
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
⊢ ENNReal.ofReal (limsup u f) = limsup (fun (a : α) ↦ ENNReal.ofReal (u a)) f

Tactic:
ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_

Premises used: ENNReal.eq_of_forall_le_nnreal_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
refine :
  ∀ (r : ℝ≥0), ENNReal.ofReal (limsup u f) ≤ (↑r : ℝ≥0∞) ↔ limsup (fun (a : α) ↦ ENNReal.ofReal (u a)) f ≤ (↑r : ℝ≥0∞)
⊢ ENNReal.ofReal (limsup u f) = limsup (fun (a : α) ↦ ENNReal.ofReal (u a)) f

Tactic:
refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_

Premises used: ENNReal.eq_of_forall_le_nnreal_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
simp : limsup u f ≤ (↑r : ℝ) ↔ limsup (fun (a : α) ↦ ENNReal.ofReal (u a)) f ≤ (↑r : ℝ≥0∞)
⊢ ENNReal.ofReal (limsup u f) ≤ (↑r : ℝ≥0∞) ↔ limsup (fun (a : α) ↦ ENNReal.ofReal (u a)) f ≤ (↑r : ℝ≥0∞)

Tactic:
simp only [ofReal_le_coe]

Premises used: ENNReal.ofReal_le_coe
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
rw : (∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y) ↔ ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
⊢ limsup u f ≤ (↑r : ℝ) ↔ limsup (fun (a : α) ↦ ENNReal.ofReal (u a)) f ≤ (↑r : ℝ≥0∞)

Tactic:
rw [limsup_le_iff, limsup_le_iff]

Premises used: Filter.limsup_le_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
mp : (∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y) → ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
mpr : (∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y) → ∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y
⊢ (∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y) ↔ ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y

Tactic:
constructor
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y
hx : none > (↑r : ℝ≥0∞)
⊢ ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < none

Tactic:
simp
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > (↑r : ℝ≥0∞)
⊢ (↑x : ℝ) > (↑r : ℝ)

Tactic:
simpa using hx
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > (↑r : ℝ≥0∞)
h₃ : ∀ (a : α) (ha : u a < (↑x : ℝ)), ENNReal.ofReal (u a) < some x
⊢ ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < some x

Tactic:
filter_upwards [h x (by simpa using hx)] with a ha

Premises used: NNReal.toReal
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > (↑r : ℝ≥0∞)
a : α
ha : u a < (↑x : ℝ)
h₃ : ∀ (ha₀ : u a ≤ 0), ENNReal.ofReal (u a) < some x
h₄ : ∀ (ha₀ : 0 ≤ u a), ENNReal.ofReal (u a) < some x
⊢ ENNReal.ofReal (u a) < some x

Tactic:
obtain ha₀ | ha₀ := le_total (u a) 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > (↑r : ℝ≥0∞)
a : α
ha : u a < (↑x : ℝ)
ha₀ : u a ≤ 0
⊢ ENNReal.ofReal (u a) < some x

Tactic:
simpa [ofReal_of_nonpos, *] using hx.bot_lt

Premises used: LT.lt.bot_lt, ENNReal.ofReal_of_nonpos
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > (↑r : ℝ), ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > (↑r : ℝ≥0∞)
a : α
ha : u a < (↑x : ℝ)
ha₀ : 0 ≤ u a
⊢ ENNReal.ofReal (u a) < some x

Tactic:
simp [ofReal_lt_coe_iff, *]

Premises used: ENNReal.ofReal_lt_coe_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > (↑r : ℝ)
⊢ 0 ≤ (↑r : ℝ)

Tactic:
simp
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > (↑r : ℝ)
⊢ 0 < x

Tactic:
have : 0 < x := hx.trans_le' (by simp)
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > (↑r : ℝ)
this : 0 < x
⊢ ENNReal.ofReal x > (↑r : ℝ≥0∞)

Tactic:
simpa [this] using hx
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > (↑r : ℝ)
this : 0 < x
h₃ : ∀ (a : α) (ha : ENNReal.ofReal (u a) < ENNReal.ofReal x), u a < x
⊢ ∀ᶠ (a : α) in f, u a < x

Tactic:
filter_upwards [h (.ofReal x) (by simpa [this] using hx)] with a ha

Premises used: ENNReal.ofReal
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > (↑r : ℝ)
this : 0 < x
a : α
ha : ENNReal.ofReal (u a) < ENNReal.ofReal x
⊢ u a ≤ (ENNReal.ofReal (u a)).toReal

Tactic:
simp [toReal_ofReal']

Premises used: ENNReal.toReal_ofReal'
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > (↑r : ℝ≥0∞), ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > (↑r : ℝ)
this : 0 < x
a : α
ha : ENNReal.ofReal (u a) < ENNReal.ofReal x
⊢ u a < x

Tactic:
exact (toReal_lt_of_lt_ofReal ha).trans_le' (by simp [toReal_ofReal'])

Premises used: ENNReal.toReal_lt_of_lt_ofReal, LT.lt.trans_le'
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ (↑C : ℝ≥0∞)
x : α
⊢ 0 ≤ (u x).toReal

Tactic:
positivity
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ (↑C : ℝ≥0∞)
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal

Tactic:
have h₁ : IsCoboundedUnder (· ≤ ·) f (fun a ↦ (u a).toReal) :=
    IsCoboundedUnder.of_frequently_ge <| .of_forall fun _ ↦ by positivity
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ (↑C : ℝ≥0∞)
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal

Tactic:
isBoundedUnder_of_eventually_le (a := C) ?_

Premises used: Filter.isBoundedUnder_of_eventually_le
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ (↑C : ℝ≥0∞)
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
refine : ∀ᶠ (x : α) in f, (u x).toReal ≤ (↑C : ℝ)
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal

Tactic:
refine isBoundedUnder_of_eventually_le (a := C) ?_

Premises used: Filter.isBoundedUnder_of_eventually_le
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
inst : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ (↑C : ℝ≥0∞)
h₁ : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
h : ∀ (a : α) (ha : u a ≤ (↑C : ℝ≥0∞)), (u a).toReal ≤ (↑C : ℝ)
⊢ ∀ᶠ (x : α) in f, (u x).toReal ≤ (↑C : ℝ)

Tactic:
filter_upwards [hf] with a ha