awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
pos : ∀ (h_bot : x = ⊥), ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
neg : ∀ (h_bot : ¬x = ⊥), ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x

Tactic:
by_cases h_bot : x = ⊥
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
h_bot : x = ⊥
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x

Tactic:
tendsto_nhds_of_eventually_eq ?_

Premises used: ContinuousAt, tendsto_nhds_of_eventually_eq
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
h_bot : x = ⊥
pos : ∀ᶠ (x' : EReal) in 𝓝 x, ENNReal.ofReal x'.toReal = (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x

Tactic:
refine tendsto_nhds_of_eventually_eq ?_

Premises used: tendsto_nhds_of_eventually_eq
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
h_bot : x = ⊥
pos :
  ∃ (i : ℝ),
    True ∧ ∀ ⦃x : EReal⦄, x ∈ Iio (↑i : EReal) → ENNReal.ofReal x.toReal = (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) ⊥
⊢ ∀ᶠ (x' : EReal) in 𝓝 x, ENNReal.ofReal x'.toReal = (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x

Tactic:
rw [h_bot, nhds_bot_basis.eventually_iff]

Premises used: EReal.nhds_bot_basis, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
h_bot : x = ⊥
⊢ ∃ (i : ℝ),
    True ∧ ∀ ⦃x : EReal⦄, x ∈ Iio (↑i : EReal) → ENNReal.ofReal x.toReal = (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) ⊥

Tactic:
simpa [toReal_bot, ENNReal.ofReal_zero, ENNReal.ofReal_eq_zero, true_and] using
      ⟨0, fun _ hx ↦ toReal_nonpos hx.le⟩

Premises used: ENNReal.ofReal_eq_zero, EReal.toReal_bot, ENNReal.ofReal_zero, true_and
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
h_bot : ¬x = ⊥
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x

Tactic:
ENNReal.continuous_ofReal.continuousAt.comp' <| continuousOn_toReal.continuousAt
    <| (toFinite _).isClosed.compl_mem_nhds ?_

Premises used: ENNReal.continuous_ofReal, EReal.continuousOn_toReal, ContinuousAt.comp', IsClosed.compl_mem_nhds, Continuous.continuousAt, Set.toFinite, ContinuousOn.continuousAt, Set.Finite.isClosed
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
h_bot : ¬x = ⊥
neg : x ∉ {⊥, ⊤}
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : EReal) ↦ ENNReal.ofReal x.toReal) x

Tactic:
refine ENNReal.continuous_ofReal.continuousAt.comp' <| continuousOn_toReal.continuousAt
    <| (toFinite _).isClosed.compl_mem_nhds ?_

Premises used: ENNReal.continuous_ofReal, EReal.continuousOn_toReal, ContinuousAt.comp', IsClosed.compl_mem_nhds, Continuous.continuousAt, Set.toFinite, ContinuousOn.continuousAt, Set.Finite.isClosed
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
x_1 : EReal
h_top : ¬x_1 = ⊤
x : EReal
hx : Membership.mem (γ := Set EReal) {⊤}ᶜ x
h_bot : ¬x = ⊥
⊢ x ∉ {⊥, ⊤}

Tactic:
simp_all only [mem_compl_iff, mem_singleton_iff, mem_insert_iff, or_self, not_false_eq_true]

Premises used: Set.mem_singleton_iff, or_self, Set.mem_insert_iff, not_false_eq_true, Set.mem_compl_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α → EReal
hf : Continuous[inst, _] f
⊢ Continuous[inst, _] fun (x : α) ↦ (f x).toENNReal

Tactic:
continuous_toENNReal.comp hf

Premises used: EReal.toENNReal, Continuous.comp, EReal.continuous_toENNReal, ite
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Set α
f : α → EReal
hf : ContinuousOn f s
⊢ ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ (f x).toENNReal) s

Tactic:
continuous_toENNReal.comp_continuousOn hf

Premises used: Continuous.comp_continuousOn, EReal.toENNReal, EReal.continuous_toENNReal, ite
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α → EReal
s : Set α
x : α
hf : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (Y := ℝ≥0∞) (fun (x : α) ↦ (f x).toENNReal) s x

Tactic:
continuous_toENNReal.continuousAt.comp_continuousWithinAt hf

Premises used: EReal.toENNReal, Continuous.continuousAt, EReal.continuous_toENNReal, ContinuousAt.comp_continuousWithinAt, ite
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
inst : TopologicalSpace α
f : α → EReal
x : α
hf : ContinuousAt f x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : α) ↦ (f x).toENNReal) x

Tactic:
continuous_toENNReal.continuousAt.comp hf

Premises used: EReal.toENNReal, Continuous.continuousAt, EReal.continuous_toENNReal, ContinuousAt.comp, ite
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
u v : α → EReal
⊢ HAdd.hAdd (α := EReal) (⨅ (x : α), u x) (⨅ (x : α), v x) ≤ ⨅ (x : α), (u + v) x

Tactic:
le_iInf fun i ↦ add_le_add (iInf_le u i) (iInf_le v i)

Premises used: add_le_add, le_iInf, iInf_le
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_2
u v : α → EReal
⊢ ⨆ (x : α), (u + v) x ≤ HAdd.hAdd (α := EReal) (⨆ (x : α), u x) (⨆ (x : α), v x)

Tactic:
iSup_le fun i ↦ add_le_add (le_iSup u i) (le_iSup v i)

Premises used: add_le_add, le_iSup, iSup_le
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
v : α → EReal
⊢ liminf (-v) f = -limsup v f

Tactic:
EReal.negOrderIso.limsup_apply.symm

Premises used: Filter.limsInf, WithBot, OrderIso.limsup_apply, Filter.liminf, setOf, EReal, EReal.neg, Eq.symm, EReal.negOrderIso
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
v : α → EReal
⊢ limsup (-v) f = -liminf v f

Tactic:
EReal.negOrderIso.liminf_apply.symm

Premises used: Filter.limsSup, WithBot, setOf, EReal, OrderIso.liminf_apply, Filter.limsup, EReal.neg, Eq.symm, EReal.negOrderIso
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
⊢ liminf u f + liminf v f ≤ liminf (u + v) f

Tactic:
add_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, EReal.add_le_of_forall_lt, Filter.le_liminf_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
refine :
  ∀ (a : EReal) (a_u : a < liminf u f) (b : EReal) (b_v : b < liminf v f) (c : EReal) (c_ab : c < a + b),
    ∀ᶠ (a : α) in f, c < (u + v) a
⊢ liminf u f + liminf v f ≤ liminf (u + v) f

Tactic:
refine add_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, EReal.add_le_of_forall_lt, Filter.le_liminf_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
a_u : a < liminf u f
b : EReal
b_v : b < liminf v f
c : EReal
c_ab : c < a + b
h : ∀ (x : α) (a_x : a < u x) (b_x : b < v x), c < (u + v) x
⊢ ∀ᶠ (a : α) in f, c < (u + v) a

Tactic:
filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x

Premises used: Filter.eventually_lt_of_lt_liminf
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
a_u : a < liminf u f
b : EReal
b_v : b < liminf v f
c : EReal
c_ab : c < a + b
x : α
a_x : a < u x
b_x : b < v x
⊢ c < (u + v) x

Tactic:
c_ab.trans (add_lt_add a_x b_x)

Premises used: LT.lt.trans, EReal.add_lt_add
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
a_u : a < liminf u f
b : EReal
b_v : b < liminf v f
c : EReal
c_ab : c < a + b
x : α
a_x : a < u x
b_x : b < v x
⊢ c < (u + v) x

Tactic:
exact c_ab.trans (add_lt_add a_x b_x)

Premises used: LT.lt.trans, EReal.add_lt_add
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
⊢ limsup (u + v) f ≤ limsup u f + limsup v f

Tactic:
le_add_of_forall_gt h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.limsup_le_iff, EReal.le_add_of_forall_gt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
refine :
  ∀ (a : EReal) (a_u : a > limsup u f) (b : EReal) (b_v : b > limsup v f) (c : EReal) (c_ab : c > a + b),
    ∀ᶠ (a : α) in f, (u + v) a < c
⊢ limsup (u + v) f ≤ limsup u f + limsup v f

Tactic:
refine le_add_of_forall_gt h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.limsup_le_iff, EReal.le_add_of_forall_gt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a + b
h₁ : ∀ (x : α) (a_x : u x < a) (b_x : v x < b), (u + v) x < c
⊢ ∀ᶠ (a : α) in f, (u + v) a < c

Tactic:
filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v] with x a_x b_x

Premises used: Filter.eventually_lt_of_limsup_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a + b
x : α
a_x : u x < a
b_x : v x < b
⊢ (u + v) x < c

Tactic:
(add_lt_add a_x b_x).trans c_ab

Premises used: LT.lt.trans, EReal.add_lt_add
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a + b
x : α
a_x : u x < a
b_x : v x < b
⊢ (u + v) x < c

Tactic:
exact (add_lt_add a_x b_x).trans c_ab

Premises used: LT.lt.trans, EReal.add_lt_add
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
⊢ limsup u f + liminf v f ≤ limsup (u + v) f

Tactic:
add_le_of_forall_lt fun _ a_u _ b_v ↦ (le_limsup_iff).2 fun _ c_ab ↦
    (((frequently_lt_of_lt_limsup) a_u).and_eventually ((eventually_lt_of_lt_liminf) b_v)).mono
    fun _ ab_x ↦ c_ab.trans (add_lt_add ab_x.1 ab_x.2)

Premises used: Iff.mpr, Filter.eventually_lt_of_lt_liminf, Filter.le_limsup_iff, Filter.Frequently.mono, Filter.Frequently.and_eventually, And.right, And.left, EReal.add_le_of_forall_lt, Filter.frequently_lt_of_lt_limsup, LT.lt.trans, EReal.add_lt_add
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ liminf v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ liminf v f ≠ ⊥
⊢ liminf (u + v) f ≤ limsup u f + liminf v f

Tactic:
le_add_of_forall_gt h h' fun _ a_u _ b_v ↦ (liminf_le_iff).2 fun _ c_ab ↦
    (((frequently_lt_of_liminf_lt) b_v).and_eventually ((eventually_lt_of_limsup_lt) a_u)).mono
    fun _ ab_x ↦ (add_lt_add ab_x.2 ab_x.1).trans c_ab

Premises used: Iff.mpr, Filter.eventually_lt_of_limsup_lt, Filter.Frequently.mono, EReal.le_add_of_forall_gt, Filter.Frequently.and_eventually, And.right, And.left, Filter.frequently_lt_of_liminf_lt, Filter.liminf_le_iff, LT.lt.trans, EReal.add_lt_add
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
apply : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
apply₁ : limsup u f + limsup v f ≤ ⊥
⊢ limsup (u + v) f = ⊥

Tactic:
apply le_bot_iff.1 ((limsup_add_le (.inr h') _).trans _)

Premises used: le_bot_iff, Iff.mp, LE.le.trans, Or.inr, EReal.limsup_add_le
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
rw : Ne (α := EReal) ⊥ ⊤ ∨ limsup v f ≠ ⊥
⊢ limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥

Tactic:
rw [h]
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ Ne (α := EReal) ⊥ ⊤ ∨ limsup v f ≠ ⊥

Tactic:
.inl bot_ne_top

Premises used: Or.inl, bot_ne_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
⊢ Ne (α := EReal) ⊥ ⊤ ∨ limsup v f ≠ ⊥

Tactic:
exact .inl bot_ne_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f = ⊥
h' : limsup v f ≠ ⊤
rw : ⊥ + limsup v f ≤ ⊥
rw₁ rw₂ : LE.le (α := EReal) ⊥ ⊥
⊢ limsup u f + limsup v f ≤ ⊥

Tactic:
rw [h, bot_add]

Premises used: EReal.bot_add
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
inl : ∀ (hb : limsup v f ≤ ⊤), limsup (u + v) f ≤ a + ⊤
inr : ∀ (h : b < ⊤), limsup (u + v) f ≤ a + b
⊢ limsup (u + v) f ≤ a + b

Tactic:
rcases eq_top_or_lt_top b with rfl | h

Premises used: eq_top_or_lt_top, rfl
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
ha : limsup u f < a
hb : limsup v f ≤ ⊤
inl : limsup (u + v) f ≤ ⊤
⊢ limsup (u + v) f ≤ a + ⊤

Tactic:
rw [add_top_of_ne_bot ha.ne_bot]

Premises used: EReal.add_top_of_ne_bot, LT.lt.ne_bot
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
ha : limsup u f < a
hb : limsup v f ≤ ⊤
⊢ limsup (u + v) f ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
ha : limsup u f < a
hb : limsup v f ≤ ⊤
⊢ limsup (u + v) f ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
h : b < ⊤
⊢ limsup (u + v) f ≤ a + b

Tactic:
(limsup_add_le (.inr (hb.trans_lt h).ne) (.inl ha.ne_top)).trans (add_le_add ha.le hb)

Premises used: LT.lt.ne_top, add_le_add, LT.lt.le, Or.inl, LE.le.trans, LE.le.trans_lt, Or.inr, LT.lt.ne, EReal.limsup_add_le
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : limsup u f < a
hb : limsup v f ≤ b
h : b < ⊤
⊢ limsup (u + v) f ≤ a + b

Tactic:
exact (limsup_add_le (.inr (hb.trans_lt h).ne) (.inl ha.ne_top)).trans (add_le_add ha.le hb)

Premises used: LT.lt.ne_top, add_le_add, LT.lt.le, Or.inl, LE.le.trans, LE.le.trans_lt, Or.inr, LT.lt.ne, EReal.limsup_add_le
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
a b : EReal
ha : a < liminf u f
hb : b < liminf v f
⊢ a + b < liminf (u + v) f

Tactic:
(add_lt_add ha hb).trans_le le_liminf_add

Premises used: EReal.le_liminf_add, LT.lt.trans_le, EReal.add_lt_add
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
apply : ⊤ ≤ liminf u f + liminf v f
⊢ liminf (u + v) f = ⊤

Tactic:
apply top_le_iff.1 (le_trans _ le_liminf_add)

Premises used: EReal.le_liminf_add, top_le_iff, Iff.mp, le_trans
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
rw : ⊤ ≤ ⊤ + liminf v f
rw₁ rw₂ : LE.le (α := EReal) ⊤ ⊤
⊢ ⊤ ≤ liminf u f + liminf v f

Tactic:
rw [h, top_add_of_ne_bot h']

Premises used: EReal.top_add_of_ne_bot
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
inl : ∀ (h₁ : LE.le (α := EReal) 0 0) (h₂ : Ne (α := EReal) 0 ⊤), limsup (fun (x : α) ↦ 0 * u x) f = 0 * limsup u f
inr : ∀ (h₃ : 0 < c), limsup (fun (x : α) ↦ c * u x) f = c * limsup u f
⊢ limsup (fun (x : α) ↦ c * u x) f = c * limsup u f

Tactic:
obtain rfl | h₃ := h₁.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
h₁ : LE.le (α := EReal) 0 0
h₂ : Ne (α := EReal) 0 ⊤
⊢ limsup (fun (x : α) ↦ 0 * u x) f = 0 * limsup u f

Tactic:
simp
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
inr : limsup (fun (x : α) ↦ u x * c) f = limsup u f * c
⊢ limsup (fun (x : α) ↦ c * u x) f = c * limsup u f

Tactic:
simp_rw [EReal.mul_comm (x := c)]

Premises used: EReal.mul_comm
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
inr : limsup (fun (x : α) ↦ u x * c) f ≤ limsup u f * c
inr₁ : limsup u f * c ≤ limsup (fun (x : α) ↦ u x * c) f
⊢ limsup (fun (x : α) ↦ u x * c) f = limsup u f * c

Tactic:
apply eq_of_le_of_ge

Premises used: eq_of_le_of_ge
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
inr : ∀ y > limsup u f * c, ∀ᶠ (a : α) in f, u a * c < y
⊢ limsup (fun (x : α) ↦ u x * c) f ≤ limsup u f * c

Tactic:
rw [limsup_le_iff]

Premises used: Filter.limsup_le_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ 0 < c

Tactic:
aesop
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ c ≠ ⊤

Tactic:
aesop
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ ∀ y > limsup u f * c, ∀ᶠ (a : α) in f, u a * c < y

Tactic:
simpa [← EReal.lt_div_iff (by aesop) (by aesop)]
      using fun _ ↦ eventually_lt_of_limsup_lt

Premises used: EReal.lt_div_iff, Filter.eventually_lt_of_limsup_lt
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
inr : ∀ y < limsup u f * c, ∃ᶠ (a : α) in f, y < u a * c
⊢ limsup u f * c ≤ limsup (fun (x : α) ↦ u x * c) f

Tactic:
rw [le_limsup_iff]

Premises used: Filter.le_limsup_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
h₃ : 0 < c
⊢ ∀ y < limsup u f * c, ∃ᶠ (a : α) in f, y < u a * c

Tactic:
simpa [← EReal.div_lt_iff (by aesop) (by aesop)]
      using fun _ ↦ frequently_lt_of_lt_limsup

Premises used: EReal.div_lt_iff, Filter.frequently_lt_of_lt_limsup
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : c ≤ 0
h₂ : c ≠ ⊥
⊢ 0 ≤ -c

Tactic:
aesop
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : c ≤ 0
h₂ : c ≠ ⊥
⊢ -c ≠ ⊤

Tactic:
aesop
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : c ≤ 0
h₂ : c ≠ ⊥
⊢ limsup (fun (x : α) ↦ c * u x) f = c * liminf u f

Tactic:
simpa [limsup_neg] using
    limsup_const_mul_of_nonneg_of_ne_top (u := -u) (c := -c) (by aesop) (by aesop)

Premises used: EReal.limsup_neg, EReal.limsup_const_mul_of_nonneg_of_ne_top
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
⊢ 0 ≤ c

Tactic:
aesop
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
⊢ c ≠ ⊤

Tactic:
aesop
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : 0 ≤ c
h₂ : c ≠ ⊤
⊢ liminf (fun (x : α) ↦ c * u x) f = c * liminf u f

Tactic:
simpa [mul_neg, ← Pi.neg_def, limsup_neg] using
    limsup_const_mul_of_nonneg_of_ne_top (u := -u) (by aesop) (by aesop)

Premises used: EReal.limsup_neg, EReal.limsup_const_mul_of_nonneg_of_ne_top, Pi.neg_def, mul_neg
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u : α → EReal
inst : f.NeBot
c : EReal
h₁ : c ≤ 0
h₂ : c ≠ ⊥
⊢ liminf (fun (x : α) ↦ c * u x) f = c * limsup u f

Tactic:
simpa [neg_mul, ← Pi.neg_def, limsup_neg] using
    limsup_const_mul_of_nonneg_of_ne_top (c := -c) (by aesop) (by aesop)

Premises used: EReal.limsup_neg, EReal.limsup_const_mul_of_nonneg_of_ne_top, neg_mul, Pi.neg_def
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
inl : ∀ (hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x) (hv : 0 ≤ᶠ[⊥] v), limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
inr : f.NeBot → limsup u f * liminf v f ≤ limsup (u * v) f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
rcases f.eq_or_neBot with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
u v : α → EReal
hu : ∃ᶠ (x : α) in ⊥, 0 ≤ u x
hv : 0 ≤ᶠ[⊥] v
inl : ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥
inl₁ : ⊥ * liminf v ⊥ ≤ ⊥
inl₂ : HMul.hMul (α := EReal) ⊥ ⊤ ≤ ⊥
inl₃ inl₄ : LE.le (α := EReal) ⊥ ⊥
⊢ limsup u ⊥ * liminf v ⊥ ≤ limsup (u * v) ⊥

Tactic:
rw [limsup_bot, limsup_bot, liminf_bot, bot_mul_top]

Premises used: Filter.limsup_bot, EReal.bot_mul_top, Filter.liminf_bot
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
⊢ 0 ≤ limsup u f

Tactic:
have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le hu
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u0 : 0 ≤ limsup u f
⊢ 0 ≤ limsup (u * v) f

Tactic:
have uv0 : 0 ≤ limsup (u * v) f :=
    le_limsup_of_frequently_le <| (hu.and_eventually hv).mono fun _ ⟨hu, hv⟩ ↦ mul_nonneg hu hv
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
mul_le_of_forall_lt_of_nonneg u0 uv0 fun a ha b hb ↦ (le_limsup_iff).2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, EReal.mul_le_of_forall_lt_of_nonneg, Filter.le_limsup_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
inr :
  ∀ (a : EReal) (ha : a ∈ Ioo 0 (limsup u f)) (b : EReal) (hb : b ∈ Ioo 0 (liminf v f)) (c : EReal) (c_ab : c < a * b),
    ∃ᶠ (a : α) in f, c < (u * v) a
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
refine mul_le_of_forall_lt_of_nonneg u0 uv0 fun a ha b hb ↦ (le_limsup_iff).2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, EReal.mul_le_of_forall_lt_of_nonneg, Filter.le_limsup_iff
-- Module: Mathlib.Topology.Instances.EReal.Lemmas
Goal:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h : f.NeBot
u0 : 0 ≤ limsup u f
uv0 : 0 ≤ limsup (u * v) f
a : EReal
ha : a ∈ Ioo 0 (limsup u f)
b : EReal
hb : b ∈ Ioo 0 (liminf v f)
c : EReal
c_ab : c < a * b
⊢ ∃ᶠ (a : α) in f, c < (u * v) a

Tactic:
(((frequently_lt_of_lt_limsup) (mem_Ioo.1 ha).2).and_eventually
    <| (eventually_lt_of_lt_liminf (mem_Ioo.1 hb).2).and
    <| hv).mono fun x ⟨xa, ⟨xb, vx⟩⟩ ↦ ?_

Premises used: Filter.eventually_lt_of_lt_liminf, Set.mem_Ioo, HMul.hMul, _private.0.EReal.le_limsup_mul.match_2, Filter.Eventually.and, Filter.Frequently.mono, Filter.Frequently.and_eventually, And.right, LT.lt, Iff.mp, Filter.frequently_lt_of_lt_limsup