awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a : α
ha : u a ≤ (↑C : ℝ≥0∞)
⊢ (u a).toReal ≤ (↑C : ℝ)

Tactic:
ENNReal.toReal_le_coe_of_le_coe ha

Premises used: ENNReal.toReal_le_coe_of_le_coe
-- 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
a : α
ha : u a ≤ (↑C : ℝ≥0∞)
⊢ (u a).toReal ≤ (↑C : ℝ)

Tactic:
exact ENNReal.toReal_le_coe_of_le_coe ha

Premises used: ENNReal.toReal_le_coe_of_le_coe
-- 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:
have h₂ : IsBoundedUnder (· ≤ ·) f (fun a ↦ (u a).toReal) := by
    refine isBoundedUnder_of_eventually_le (a := C) ?_
    filter_upwards [hf] with a ha
    exact ENNReal.toReal_le_coe_of_le_coe ha
-- 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₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
⊢ ENNReal.ofReal (limsup (fun (a : α) ↦ (u a).toReal) f) = limsup u f

Tactic:
(ENNReal.ofReal_limsup h₁ h₂).trans (limsup_congr ?_)

Premises used: ENNReal.ofReal_limsup, Filter.limsup_congr, Eq.trans
-- 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₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
refine : ∀ᶠ (a : α) in f, ENNReal.ofReal (u a).toReal = u a
⊢ ENNReal.ofReal (limsup (fun (a : α) ↦ (u a).toReal) f) = limsup u f

Tactic:
refine (ENNReal.ofReal_limsup h₁ h₂).trans (limsup_congr ?_)

Premises used: ENNReal.ofReal_limsup, Filter.limsup_congr, Eq.trans
-- 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₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
h : ∀ (x : α) (hx : u x ≤ (↑C : ℝ≥0∞)), ENNReal.ofReal (u x).toReal = u x
⊢ ∀ᶠ (a : α) in f, ENNReal.ofReal (u a).toReal = u a

Tactic:
filter_upwards [hf] with x hx
-- 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₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
x : α
hx : u x ≤ (↑C : ℝ≥0∞)
⊢ (↑C : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- 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₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
x : α
hx : u x ≤ (↑C : ℝ≥0∞)
⊢ ENNReal.ofReal (u x).toReal = u x

Tactic:
exact ENNReal.ofReal_toReal (ne_top_of_le_ne_top (by simp : C ≠ ∞) hx)

Premises used: ENNReal.ofReal_toReal, ne_top_of_le_ne_top
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
inl :
  ∀ (h₁ : ∀ᶠ (a : α) in ⊥, u a ≠ ∞) (h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ⊥ fun (a : α) ↦ (u a).toReal),
    (limsup u ⊥).toReal = limsup (fun (a : α) ↦ (u a).toReal) ⊥
inr : ∀ (hf : f.NeBot), (limsup u f).toReal = limsup (fun (a : α) ↦ (u a).toReal) f
⊢ (limsup u f).toReal = limsup (fun (a : α) ↦ (u a).toReal) 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∞
h₁ : ∀ᶠ (a : α) in ⊥, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) ⊥ fun (a : α) ↦ (u a).toReal
⊢ (limsup u ⊥).toReal = limsup (fun (a : α) ↦ (u a).toReal) ⊥

Tactic:
simp [limsup, limsSup]

Premises used: Filter.limsSup, Filter.limsup
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
⊢ ∃ᶠ (x : α) in f, 0 ≤ (u x).toReal

Tactic:
simpa
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal

Tactic:
have : IsCoboundedUnder (· ≤ ·) f fun a ↦ (u a).toReal := .of_frequently_ge (a := 0) (by simpa)
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
⊢ (limsup u f).toReal = limsup (fun (a : α) ↦ (u a).toReal) f

Tactic:
eq_of_forall_ge_iff fun r ↦ ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
inr : ∀ (r : ℝ), (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r
⊢ (limsup u f).toReal = limsup (fun (a : α) ↦ (u a).toReal) f

Tactic:
refine eq_of_forall_ge_iff fun r ↦ ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
inr : ∀ (hr : r < 0), (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r
inr₁ : ∀ (hr : 0 ≤ r), (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r
⊢ (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r

Tactic:
obtain hr | hr := lt_or_ge r 0

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : r < 0
⊢ ∃ᶠ (i : α) in f, 0 ≤ (u i).toReal

Tactic:
simpa
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : r < 0
⊢ (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r

Tactic:
exact iff_of_false (hr.trans_le toReal_nonneg).not_ge
      (hr.trans_le <| le_limsup_of_frequently_le (by simpa)).not_ge

Premises used: Filter.le_limsup_of_frequently_le, ENNReal.toReal_nonneg, iff_of_false, LT.lt.trans_le, LT.lt.not_ge
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
inr : (∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y) ↔ ∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y
rw : limsup u f ≠ ∞
⊢ (limsup u f).toReal ≤ r ↔ limsup (fun (a : α) ↦ (u a).toReal) f ≤ r

Tactic:
rw [← le_ofReal_iff_toReal_le _ hr, limsup_le_iff, limsup_le_iff]

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

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

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

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

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

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

Tactic:
toReal_lt_of_lt_ofReal hi

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

Tactic:
exact toReal_lt_of_lt_ofReal hi

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

Tactic:
simpa [lt_top_iff_ne_top]

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

Tactic:
simpa [ofReal_lt_coe_iff hr] using hx

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

Tactic:
filter_upwards [h₁, h x (by simpa [ofReal_lt_coe_iff hr] using hx)] with i hi

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

Tactic:
simp [← lt_ofReal_iff_toReal_lt hi]

Premises used: ENNReal.lt_ofReal_iff_toReal_lt
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
obtain :
  ∀ (x : ℝ) (hx : ∀ᶠ (x_1 : ℝ) in map (fun (a : α) ↦ (u a).toReal) f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x_1 x), limsup u f ≠ ∞
⊢ limsup u f ≠ ∞

Tactic:
obtain ⟨x, hx⟩ := h₂
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (x_1 : ℝ) in map (fun (a : α) ↦ (u a).toReal) f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x_1 x
⊢ ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x

Tactic:
rw [eventually_map] at hx

Premises used: Filter.eventually_map
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
obtain : ∀ (i : α) (hi : (u i).toReal ≤ x), 0 ≤ x
⊢ 0 ≤ x

Tactic:
obtain ⟨i, hi⟩ := hx.exists

Premises used: Filter.Eventually.exists
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
i : α
hi : (u i).toReal ≤ x
⊢ 0 ≤ x

Tactic:
toReal_nonneg.trans hi

Premises used: ENNReal.toReal_nonneg, LE.le.trans
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
i : α
hi : (u i).toReal ≤ x
⊢ 0 ≤ x

Tactic:
exact toReal_nonneg.trans hi

Premises used: ENNReal.toReal_nonneg, LE.le.trans
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
⊢ 0 ≤ x

Tactic:
have hx₀ : 0 ≤ x := by obtain ⟨i, hi⟩ := hx.exists; exact toReal_nonneg.trans hi
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
hx₀ : 0 ≤ x
simp : ∃ (x : ℝ≥0∞) (_ : ∀ᶠ (a : α) in f, u a ≤ x), ¬x = ∞
⊢ limsup u f ≠ ∞

Tactic:
simp only [limsup, limsSup, eventually_map, ne_eq, sInf_eq_top, Set.mem_setOf_eq, not_forall]

Premises used: Filter.limsSup, Set.mem_setOf_eq, Filter.eventually_map, ne_eq, Filter.limsup, sInf_eq_top, Classical.not_forall
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
hx₀ : 0 ≤ x
⊢ ¬ENNReal.ofReal x = ∞

Tactic:
simp
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
hx₀ : 0 ≤ x
refine : ∀ᶠ (a : α) in f, u a ≤ ENNReal.ofReal x
⊢ ∃ (x : ℝ≥0∞) (_ : ∀ᶠ (a : α) in f, u a ≤ x), ¬x = ∞

Tactic:
refine ⟨.ofReal x, ?_, by simp⟩
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
hx₀ : 0 ≤ x
h : ∀ (i : α) (hi : u i ≠ ∞), (u i).toReal ≤ x → u i ≤ ENNReal.ofReal x
⊢ ∀ᶠ (a : α) in f, u a ≤ ENNReal.ofReal x

Tactic:
filter_upwards [h₁, hx] with i hi
-- Module: Mathlib.Order.Filter.ENNReal
Goal:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (a : α) ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (u a).toReal x
hx₀ : 0 ≤ x
i : α
hi : u i ≠ ∞
⊢ (u i).toReal ≤ x → u i ≤ ENNReal.ofReal x

Tactic:
simp [le_ofReal_iff_toReal_le, *]

Premises used: ENNReal.le_ofReal_iff_toReal_le
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
ι : Sort u_5
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (∃ (i : ι), p i ∧ (f '' s i).Subsingleton) ↔ ∃ (i : ι), p i ∧ ∀ x ∈ s i, ∀ y ∈ s i, f x = f y

Tactic:
simp only [Set.Subsingleton, forall_mem_image]

Premises used: Set.Subsingleton, Set.forall_mem_image
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
ι : Sort u_5
p : ι → Prop
s : ι → Set α
x : ι → α
h : l.HasBasis p s
hx : ∀ (i : ι), p i → x i ∈ s i
⊢ EventuallyConst f l ↔ ∃ (i : ι), p i ∧ ∀ y ∈ s i, f y = f (x i)

Tactic:
h.eventuallyConst_iff.trans <| exists_congr fun i ↦ and_congr_right fun hi ↦
    ⟨fun h ↦ (h · · (x i) (hx i hi)), fun h a ha b hb ↦ h a ha ▸ (h b hb).symm⟩

Premises used: Eq.rec, Filter.HasBasis.eventuallyConst_iff, and_congr_right, exists_congr, Iff.intro, Iff.trans, Eq.symm
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst : Nonempty β
⊢ EventuallyConst f l ↔ ∃ (x : β), Tendsto f l (pure x)

Tactic:
subsingleton_iff_exists_le_pure

Premises used: Filter.subsingleton_iff_exists_le_pure, Filter.EventuallyConst, Filter.Tendsto
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
x : β
h : Tendsto f l (pure x)
⊢ EventuallyConst f l

Tactic:
have : Nonempty β := ⟨x⟩; eventuallyConst_iff_tendsto.2 ⟨x, h⟩

Premises used: Iff.mpr, Filter.eventuallyConst_iff_tendsto, Nonempty.intro, Exists.intro
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst : Nonempty β
⊢ EventuallyConst f l ↔ ∃ (c : β), f =ᶠ[l] fun (x : α) ↦ c

Tactic:
subsingleton_iff_exists_singleton_mem

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyConst, Filter.EventuallyEq, Set.preimage, Set.singleton, Filter.subsingleton_iff_exists_singleton_mem
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
l : Filter α
p : α → Prop
⊢ EventuallyConst p l ↔ (p =ᶠ[l] fun (x : α) ↦ False) ∨ p =ᶠ[l] fun (x : α) ↦ True

Tactic:
simp only [eventuallyConst_iff_exists_eventuallyEq, Prop.exists_iff]

Premises used: Prop.exists_iff, Filter.eventuallyConst_iff_exists_eventuallyEq
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
l : Filter α
p : α → Prop
⊢ EventuallyConst p l ↔ (∀ᶠ (x : α) in l, p x) ∨ ∀ᶠ (x : α) in l, ¬p x

Tactic:
simp [eventuallyConst_pred', or_comm, EventuallyEq]

Premises used: Filter.EventuallyEq, or_comm, Filter.eventuallyConst_pred'
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
l : Filter α
s : Set α
⊢ EventuallyConst s l ↔ s =ᶠ[l] ∅ ∨ s =ᶠ[l] univ

Tactic:
eventuallyConst_pred'

Premises used: Set.univ, setOf, Filter.eventuallyConst_pred'
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
l : Filter α
s : Set α
⊢ EventuallyConst s l ↔ (∀ᶠ (x : α) in l, x ∈ s) ∨ ∀ᶠ (x : α) in l, x ∉ s

Tactic:
eventuallyConst_pred

Premises used: Set.Mem, Filter.eventuallyConst_pred
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
s : Set β
f : α → β
⊢ EventuallyConst (f ⁻¹' s) l ↔ EventuallyConst s (map f l)

Tactic:
.rfl

Premises used: Set.Mem, Filter.map, Iff.rfl, setOf, Filter.EventuallyConst, Set.preimage
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f g : α → β
h : f =ᶠ[l] g
⊢ EventuallyConst f l ↔ EventuallyConst g l

Tactic:
simp only [EventuallyConst, map_congr h]

Premises used: Filter.map_congr, Filter.EventuallyConst
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
l : Filter α
⊢ EventuallyConst id l ↔ l.Subsingleton

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.map, Iff.rfl, setOf, Filter.EventuallyConst, Set.preimage
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ EventuallyConst f ⊥

Tactic:
subsingleton_bot

Premises used: Set.Mem, Filter.map, Set.univ, setOf, Filter.EventuallyConst, Filter.subsingleton_bot, Set.preimage, Filter.copy
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
c : β
⊢ EventuallyConst.{u_1, u_2} (β := β) (fun (x : α) ↦ c) l

Tactic:
.of_tendsto tendsto_const_pure

Premises used: Filter.tendsto_const_pure, Filter.EventuallyConst.of_tendsto
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f g : α → β
h : EventuallyConst f l
hg : f =ᶠ[l] g
⊢ EventuallyConst g l

Tactic:
hg.eventuallyConst_iff.1 h

Premises used: Filter.EventuallyEq.eventuallyConst_iff, Iff.mp
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst : Subsingleton β
⊢ EventuallyConst f l

Tactic:
.of_subsingleton

Premises used: Filter.Subsingleton.of_subsingleton, Filter.EventuallyConst
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
l' : Filter α
h : EventuallyConst f l
hl' : l' ≤ l
⊢ EventuallyConst f l'

Tactic:
h.anti (map_mono hl')

Premises used: Filter.map_mono, Filter.EventuallyConst, Filter.Subsingleton.anti
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
l : Filter α
f : α → β
inst : Subsingleton α
⊢ EventuallyConst f l

Tactic:
.map .of_subsingleton f

Premises used: Filter.Subsingleton.of_subsingleton, Filter.EventuallyConst, Filter.Subsingleton.map
-- Module: Mathlib.Order.Filter.EventuallyConst
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
h : EventuallyConst f l
g : β → γ
⊢ EventuallyConst (g ∘ f) l

Tactic:
h.map g

Premises used: Set.Mem, Filter.map, setOf, Filter.EventuallyConst, Filter.Subsingleton.map, Set.preimage