awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
y : α
hy : y ∈ s
⊢ ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ edist (f x) (f y))
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
y : α
hy : y ∈ s
funProp : (↑K : ℝ≥0∞) ≠ ∞
⊢ ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ (↑K : ℝ≥0∞) * edist x y)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContinuousOn (Y := ℝ≥0∞) (fun (y : α) ↦ edist (f x) (f y))
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
funProp : (↑K : ℝ≥0∞) ≠ ∞
⊢ ContinuousOn (Y := ℝ≥0∞) (fun (y : α) ↦ (↑K : ℝ≥0∞) * edist x y)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ LipschitzOnWith K f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) ↔ LipschitzOnWith K f s

Tactic:
⟨fun hf ↦ hf.mono subset_closure, LipschitzOnWith.closure hcont⟩

Premises used: LipschitzOnWith.mono, subset_closure, LipschitzOnWith.closure, Iff.intro
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
inl : ∀ (h : Bornology.IsBounded (α := ℝ) ∅), ediam (X := ℝ) ∅ = ENNReal.ofReal (HSub.hSub (α := ℝ) (sSup ∅) (sInf ∅))
inr : ∀ (hne : s.Nonempty), ediam s = ENNReal.ofReal (sSup s - sInf s)
⊢ ediam s = ENNReal.ofReal (sSup s - sInf s)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hne)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
h : Bornology.IsBounded (α := ℝ) ∅
⊢ ediam (X := ℝ) ∅ = ENNReal.ofReal (HSub.hSub (α := ℝ) (sSup ∅) (sInf ∅))

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ ediam s = ENNReal.ofReal (sSup s - sInf s)

Tactic:
le_antisymm (Metric.ediam_le_of_forall_dist_le fun x hx y hy => ?_) ?_

Premises used: le_antisymm, Metric.ediam_le_of_forall_dist_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
inr : ∀ (x : ℝ) (hx : x ∈ s) (y : ℝ) (hy : y ∈ s), dist x y ≤ sSup s - sInf s
inr₁ : ENNReal.ofReal (sSup s - sInf s) ≤ ediam s
⊢ ediam s = ENNReal.ofReal (sSup s - sInf s)

Tactic:
refine le_antisymm (Metric.ediam_le_of_forall_dist_le fun x hx y hy => ?_) ?_

Premises used: le_antisymm, Metric.ediam_le_of_forall_dist_le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ dist x y ≤ sSup s - sInf s

Tactic:
Real.dist_le_of_mem_Icc (h.subset_Icc_sInf_sSup hx) (h.subset_Icc_sInf_sSup hy)

Premises used: Bornology.IsBounded.subset_Icc_sInf_sSup, Real.dist_le_of_mem_Icc
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ dist x y ≤ sSup s - sInf s

Tactic:
exact Real.dist_le_of_mem_Icc (h.subset_Icc_sInf_sSup hx) (h.subset_Icc_sInf_sSup hy)

Premises used: Bornology.IsBounded.subset_Icc_sInf_sSup, Real.dist_le_of_mem_Icc
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
inr : sSup s - sInf s ≤ (ediam s).toReal
⊢ ENNReal.ofReal (sSup s - sInf s) ≤ ediam s

Tactic:
apply ENNReal.ofReal_le_of_le_toReal

Premises used: ENNReal.ofReal_le_of_le_toReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
inr : sSup s - sInf s ≤ Metric.diam (closure s)
⊢ sSup s - sInf s ≤ (ediam s).toReal

Tactic:
rw [← Metric.diam, ← Metric.diam_closure]

Premises used: Metric.diam_closure, Metric.diam
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ sSup s - sInf s ≤ dist (sSup s) (sInf s)

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ dist (sSup s) (sInf s) ≤ Metric.diam (closure s)

Tactic:
dist_le_diam_of_mem h.closure (csSup_mem_closure hne h.bddAbove)
        (csInf_mem_closure hne h.bddBelow)

Premises used: Bornology.IsBounded.bddBelow, Metric.dist_le_diam_of_mem, csSup_mem_closure, Bornology.IsBounded.bddAbove, csInf_mem_closure, Bornology.IsBounded.closure
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ sSup s - sInf s ≤ Metric.diam (closure s)

Tactic:
calc sSup s - sInf s ≤ dist (sSup s) (sInf s) := le_abs_self _
    _ ≤ Metric.diam (closure s) := dist_le_diam_of_mem h.closure (csSup_mem_closure hne h.bddAbove)
        (csInf_mem_closure hne h.bddBelow)

Premises used: le_abs_self, Bornology.IsBounded.bddBelow, Metric.dist_le_diam_of_mem, closure, Metric.diam, Dist.dist, csSup_mem_closure, Bornology.IsBounded.bddAbove, csInf_mem_closure, InfSet.sInf, SupSet.sSup, Bornology.IsBounded.closure
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
rw : 0 ≤ sSup s - sInf s
⊢ Metric.diam s = sSup s - sInf s

Tactic:
rw [Metric.diam, Real.ediam_eq h, ENNReal.toReal_ofReal]

Premises used: Real.ediam_eq, ENNReal.toReal_ofReal, Metric.diam
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
⊢ 0 ≤ sSup s - sInf s

Tactic:
sub_nonneg.2 (Real.sInf_le_sSup s h.bddBelow h.bddAbove)

Premises used: Iff.mpr, Bornology.IsBounded.bddBelow, Real.sInf_le_sSup, sub_nonneg, Bornology.IsBounded.bddAbove
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
s : Set ℝ
h : Bornology.IsBounded s
⊢ 0 ≤ sSup s - sInf s

Tactic:
exact sub_nonneg.2 (Real.sInf_le_sSup s h.bddBelow h.bddAbove)

Premises used: Iff.mpr, Bornology.IsBounded.bddBelow, Real.sInf_le_sSup, sub_nonneg, Bornology.IsBounded.bddAbove
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ
inl : ∀ (h : b ≤ a), ediam (Ioo a b) = ENNReal.ofReal (b - a)
inr : ∀ (h : a < b), ediam (Ioo a b) = ENNReal.ofReal (b - a)
⊢ ediam (Ioo a b) = ENNReal.ofReal (b - a)

Tactic:
rcases le_or_gt b a with (h | h)

Premises used: le_or_gt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ
h : b ≤ a
⊢ ediam (Ioo a b) = ENNReal.ofReal (b - a)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ
h : a < b
inr : ENNReal.ofReal (sSup (Ioo a b) - sInf (Ioo a b)) = ENNReal.ofReal (b - a)
inr₁ : ENNReal.ofReal (b - sInf (Ioo a b)) = ENNReal.ofReal (b - a)
inr₂ inr₃ : ENNReal.ofReal (b - a) = ENNReal.ofReal (b - a)
⊢ ediam (Ioo a b) = ENNReal.ofReal (b - a)

Tactic:
rw [Real.ediam_eq (isBounded_Ioo _ _), csSup_Ioo h, csInf_Ioo h]

Premises used: Real.ediam_eq, Metric.isBounded_Ioo, csSup_Ioo, csInf_Ioo
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ
inl : ∀ (h : a ≤ b), ediam (Icc a b) = ENNReal.ofReal (b - a)
inr : ∀ (h : b < a), ediam (Icc a b) = ENNReal.ofReal (b - a)
⊢ ediam (Icc a b) = ENNReal.ofReal (b - a)

Tactic:
rcases le_or_gt a b with (h | h)

Premises used: le_or_gt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ
h : a ≤ b
inl : ENNReal.ofReal (sSup (Icc a b) - sInf (Icc a b)) = ENNReal.ofReal (b - a)
inl₁ : ENNReal.ofReal (b - sInf (Icc a b)) = ENNReal.ofReal (b - a)
inl₂ inl₃ : ENNReal.ofReal (b - a) = ENNReal.ofReal (b - a)
⊢ ediam (Icc a b) = ENNReal.ofReal (b - a)

Tactic:
rw [Real.ediam_eq (isBounded_Icc _ _), csSup_Icc h, csInf_Icc h]

Premises used: Real.ediam_eq, csSup_Icc, csInf_Icc, Metric.isBounded_Icc
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ
h : b < a
⊢ ediam (Icc a b) = ENNReal.ofReal (b - a)

Tactic:
simp [h, h.le]

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ
⊢ ediam (Ico a b) = ENNReal.ofReal (b - a)

Tactic:
le_antisymm (ediam_Icc a b ▸ ediam_mono Ico_subset_Icc_self)
    (ediam_Ioo a b ▸ ediam_mono Ioo_subset_Ico_self)

Premises used: le_antisymm
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ
⊢ ediam (Ioc a b) = ENNReal.ofReal (b - a)

Tactic:
le_antisymm (ediam_Icc a b ▸ ediam_mono Ioc_subset_Icc_self)
    (ediam_Ioo a b ▸ ediam_mono Ioo_subset_Ioc_self)

Premises used: le_antisymm
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ
h : a ≤ b
⊢ Metric.diam (Icc a b) = b - a

Tactic:
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]

Premises used: Iff.mpr, ENNReal.toReal_ofReal, Metric.diam, sub_nonneg
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ
h : a ≤ b
⊢ Metric.diam (Ico a b) = b - a

Tactic:
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]

Premises used: Iff.mpr, ENNReal.toReal_ofReal, Metric.diam, sub_nonneg
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ
h : a ≤ b
⊢ Metric.diam (Ioc a b) = b - a

Tactic:
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]

Premises used: Iff.mpr, ENNReal.toReal_ofReal, Metric.diam, sub_nonneg
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
a b : ℝ
h : a ≤ b
⊢ Metric.diam (Ioo a b) = b - a

Tactic:
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]

Premises used: Iff.mpr, ENNReal.toReal_ofReal, Metric.diam, sub_nonneg
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t x : ℝ≥0∞
t_ne_top : t ≠ ∞
x_le : x ≤ t
⊢ x < ∞

Tactic:
have x_lt_top : x < ∞ := lt_of_le_of_lt x_le t_ne_top.lt_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t x : ℝ≥0∞
t_ne_top : t ≠ ∞
x_le : x ≤ t
x_lt_top : x < ∞
⊢ min t x ≠ ∞

Tactic:
simp_all only [ne_eq, min_eq_top, false_and, not_false_eq_true]

Premises used: false_and, ne_eq, not_false_eq_true, min_eq_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t x : ℝ≥0∞
t_ne_top : t ≠ ∞
x_le : x ≤ t
x_lt_top : x < ∞
⊢ min t x ≠ ∞

Tactic:
have obs : min t x ≠ ∞ := by
    simp_all only [ne_eq, min_eq_top, false_and, not_false_eq_true]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t x : ℝ≥0∞
t_ne_top : t ≠ ∞
x_le : x ≤ t
x_lt_top : x < ∞
obs : min t x ≠ ∞
⊢ t.truncateToReal x = x.toReal

Tactic:
(ENNReal.toReal_eq_toReal_iff' obs x_lt_top.ne).mpr (min_eq_right x_le)

Premises used: Iff.mpr, ENNReal.toReal_eq_toReal_iff', min_eq_right, LT.lt.ne, ENNReal.truncateToReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t x : ℝ≥0∞
t_ne_top : t ≠ ∞
x_le : x ≤ t
x_lt_top : x < ∞
obs : min t x ≠ ∞
⊢ t.truncateToReal x = x.toReal

Tactic:
exact (ENNReal.toReal_eq_toReal_iff' obs x_lt_top.ne).mpr (min_eq_right x_le)

Premises used: Iff.mpr, ENNReal.toReal_eq_toReal_iff', min_eq_right, LT.lt.ne
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
x : ℝ≥0∞
h : min t x ≤ t
⊢ (min t x).toReal ≤ t.toReal

Tactic:
gcongr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
x : ℝ≥0∞
⊢ min t x ≤ t

Tactic:
min_le_left t x

Premises used: min_le_left
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
x : ℝ≥0∞
⊢ min t x ≤ t

Tactic:
exact min_le_left t x

Premises used: min_le_left
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t x : ℝ≥0∞
⊢ 0 ≤ t.truncateToReal x

Tactic:
toReal_nonneg

Premises used: ENNReal.toReal_nonneg, ENNReal.truncateToReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
x y : ℝ≥0∞
x_le_y : x ≤ y
hb : min t y ≠ ∞
⊢ (min t x).toReal ≤ (min t y).toReal

Tactic:
gcongr
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
x y : ℝ≥0∞
x_le_y : x ≤ y
⊢ min t y ≠ ∞

Tactic:
ne_top_of_le_ne_top t_ne_top (min_le_left _ _)

Premises used: min_le_left, ne_top_of_le_ne_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
x y : ℝ≥0∞
x_le_y : x ≤ y
⊢ min t y ≠ ∞

Tactic:
exact ne_top_of_le_ne_top t_ne_top (min_le_left _ _)

Premises used: min_le_left, ne_top_of_le_ne_top
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
⊢ Continuous (min t)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
apply : ∀ (x : ℝ≥0∞), Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | a ≠ ∞} (min t x)
⊢ Continuous t.truncateToReal

Tactic:
apply continuousOn_toReal.comp_continuous (by fun_prop)

Premises used: ContinuousOn.comp_continuous, ENNReal.continuousOn_toReal
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
t : ℝ≥0∞
t_ne_top : t ≠ ∞
⊢ ∀ (x : ℝ≥0∞), Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | a ≠ ∞} (min t x)

Tactic:
simp [t_ne_top]
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
inl : limsup (fun (i : ι) ↦ f i - c) ⊥ = limsup f ⊥ - c
inr : F.NeBot → limsup (fun (i : ι) ↦ f i - c) F = limsup f F - c
⊢ limsup (fun (i : ι) ↦ f i - c) F = limsup f F - c

Tactic:
rcases F.eq_or_neBot with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ limsup (fun (i : ι) ↦ f i - c) ⊥ = limsup f ⊥ - c

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
h : F.NeBot
⊢ limsup (fun (i : ι) ↦ f i - c) F = limsup f F - c

Tactic:
(Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ x - c)
    (fun _ _ h ↦ tsub_le_tsub_right h c) (continuous_sub_right c).continuousAt).symm

Premises used: Set.Mem, Filter.map, ENNReal.continuous_sub_right, setOf, Filter.limsup, Continuous.continuousAt, Monotone.map_limsSup_of_continuousAt, Set.preimage, WithTop.sub, ENNReal, tsub_le_tsub_right, Eq.symm, WithTop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
h : F.NeBot
⊢ limsup (fun (i : ι) ↦ f i - c) F = limsup f F - c

Tactic:
exact (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ x - c)
    (fun _ _ h ↦ tsub_le_tsub_right h c) (continuous_sub_right c).continuousAt).symm

Premises used: ENNReal.continuous_sub_right, Continuous.continuousAt, Monotone.map_limsSup_of_continuousAt, tsub_le_tsub_right, Eq.symm
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
F : Filter ι
inst : F.NeBot
f : ι → ℝ≥0∞
c : ℝ≥0∞
⊢ liminf (fun (i : ι) ↦ f i - c) F = liminf f F - c

Tactic:
(Monotone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ x - c)
    (fun _ _ h ↦ tsub_le_tsub_right h c) (continuous_sub_right c).continuousAt).symm

Premises used: Filter.liminf, Set.Mem, Filter.map, ENNReal.continuous_sub_right, setOf, Continuous.continuousAt, Set.preimage, Monotone.map_limsInf_of_continuousAt, WithTop.sub, ENNReal, tsub_le_tsub_right, Eq.symm, WithTop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
inl : limsup (fun (i : ι) ↦ c - f i) ⊥ = c - liminf f ⊥
inr : F.NeBot → limsup (fun (i : ι) ↦ c - f i) F = c - liminf f F
⊢ limsup (fun (i : ι) ↦ c - f i) F = c - liminf f F

Tactic:
rcases F.eq_or_neBot with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
⊢ limsup (fun (i : ι) ↦ c - f i) ⊥ = c - liminf f ⊥

Tactic:
simp
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
h : F.NeBot
⊢ limsup (fun (i : ι) ↦ c - f i) F = c - liminf f F

Tactic:
(Antitone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ c - x)
    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c_ne_top).continuousAt).symm

Premises used: Filter.liminf, Set.Mem, Filter.map, setOf, Filter.limsup, tsub_le_tsub_left, Continuous.continuousAt, ENNReal.continuous_sub_left, Set.preimage, WithTop.sub, ENNReal, Eq.symm, Antitone.map_limsInf_of_continuousAt, WithTop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
F : Filter ι
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
h : F.NeBot
⊢ limsup (fun (i : ι) ↦ c - f i) F = c - liminf f F

Tactic:
exact (Antitone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ c - x)
    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c_ne_top).continuousAt).symm

Premises used: tsub_le_tsub_left, Continuous.continuousAt, ENNReal.continuous_sub_left, Eq.symm, Antitone.map_limsInf_of_continuousAt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
F : Filter ι
inst : F.NeBot
f : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ∞
⊢ liminf (fun (i : ι) ↦ c - f i) F = c - limsup f F

Tactic:
(Antitone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ c - x)
    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c_ne_top).continuousAt).symm

Premises used: Filter.liminf, Set.Mem, Antitone.map_limsSup_of_continuousAt, Filter.map, setOf, Filter.limsup, tsub_le_tsub_left, Continuous.continuousAt, ENNReal.continuous_sub_left, Set.preimage, WithTop.sub, ENNReal, Eq.symm, WithTop
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
mul_le_of_forall_lt fun a a_u b b_v ↦ (le_limsup_iff).2 fun c c_ab ↦
    Frequently.mono (Frequently.and_eventually ((frequently_lt_of_lt_limsup) a_u)
    ((eventually_lt_of_lt_liminf) b_v)) fun _ ab_x ↦ c_ab.trans (mul_lt_mul ab_x.1 ab_x.2)

Premises used: Iff.mpr, Filter.eventually_lt_of_lt_liminf, ENNReal.mul_lt_mul, Filter.le_limsup_iff, Filter.Frequently.mono, Filter.Frequently.and_eventually, And.right, And.left, Filter.frequently_lt_of_lt_limsup, LT.lt.trans, ENNReal.mul_le_of_forall_lt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ∞
h' : limsup u f ≠ ∞ ∨ limsup v f ≠ 0
⊢ limsup (u * v) f ≤ limsup u f * limsup v f

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

Premises used: Iff.mpr, ENNReal.le_mul_of_forall_lt, Filter.limsup_le_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ∞
h' : limsup u f ≠ ∞ ∨ limsup v f ≠ 0
refine :
  ∀ (a : ℝ≥0∞) (a_u : a > limsup u f) (b : ℝ≥0∞) (b_v : b > limsup v f) (c : ℝ≥0∞) (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_mul_of_forall_lt h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, ENNReal.le_mul_of_forall_lt, Filter.limsup_le_iff
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ∞
h' : limsup u f ≠ ∞ ∨ limsup v f ≠ 0
a : ℝ≥0∞
a_u : a > limsup u f
b : ℝ≥0∞
b_v : b > limsup v f
c : ℝ≥0∞
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.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ∞
h' : limsup u f ≠ ∞ ∨ limsup v f ≠ 0
a : ℝ≥0∞
a_u : a > limsup u f
b : ℝ≥0∞
b_v : b > limsup v f
c : ℝ≥0∞
c_ab : c > a * b
x : ι
a_x : u x < a
b_x : v x < b
⊢ (u * v) x < c

Tactic:
(mul_lt_mul a_x b_x).trans c_ab

Premises used: ENNReal.mul_lt_mul, LT.lt.trans
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
h : limsup u f ≠ 0 ∨ limsup v f ≠ ∞
h' : limsup u f ≠ ∞ ∨ limsup v f ≠ 0
a : ℝ≥0∞
a_u : a > limsup u f
b : ℝ≥0∞
b_v : b > limsup v f
c : ℝ≥0∞
c_ab : c > a * b
x : ι
a_x : u x < a
b_x : v x < b
⊢ (u * v) x < c

Tactic:
exact (mul_lt_mul a_x b_x).trans c_ab

Premises used: ENNReal.mul_lt_mul, LT.lt.trans
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
⊢ liminf u f * liminf v f ≤ liminf (u * v) f

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

Premises used: Iff.mpr, Filter.le_liminf_iff, ENNReal.mul_le_of_forall_lt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
refine :
  ∀ (a : ℝ≥0∞) (a_u : a < liminf u f) (b : ℝ≥0∞) (b_v : b < liminf v f) (c : ℝ≥0∞) (c_ab : c < a * b),
    ∀ᶠ (a : ι) in f, c < (u * v) a
⊢ liminf u f * liminf v f ≤ liminf (u * v) f

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

Premises used: Iff.mpr, Filter.le_liminf_iff, ENNReal.mul_le_of_forall_lt
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
a : ℝ≥0∞
a_u : a < liminf u f
b : ℝ≥0∞
b_v : b < liminf v f
c : ℝ≥0∞
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.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
a : ℝ≥0∞
a_u : a < liminf u f
b : ℝ≥0∞
b_v : b < liminf v f
c : ℝ≥0∞
c_ab : c < a * b
x : ι
a_x : a < u x
b_x : b < v x
⊢ c < (u * v) x

Tactic:
c_ab.trans (mul_lt_mul a_x b_x)

Premises used: ENNReal.mul_lt_mul, LT.lt.trans
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
a : ℝ≥0∞
a_u : a < liminf u f
b : ℝ≥0∞
b_v : b < liminf v f
c : ℝ≥0∞
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 (mul_lt_mul a_x b_x)

Premises used: ENNReal.mul_lt_mul, LT.lt.trans
-- Module: Mathlib.Topology.Instances.ENNReal.Lemmas
Goal:
ι : Type u_4
f : Filter ι
u v : ι → ℝ≥0∞
h : limsup u f ≠ 0 ∨ liminf v f ≠ ∞
h' : limsup u f ≠ ∞ ∨ liminf v f ≠ 0
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Tactic:
le_mul_of_forall_lt h h' fun a a_u b b_v ↦ (liminf_le_iff).2 fun c c_ab ↦
    Frequently.mono (((frequently_lt_of_liminf_lt) b_v).and_eventually
    ((eventually_lt_of_limsup_lt) a_u)) fun _ ab_x ↦ (mul_lt_mul ab_x.2 ab_x.1).trans c_ab

Premises used: Iff.mpr, ENNReal.le_mul_of_forall_lt, ENNReal.mul_lt_mul, Filter.eventually_lt_of_limsup_lt, Filter.Frequently.mono, Filter.Frequently.and_eventually, And.right, And.left, Filter.frequently_lt_of_liminf_lt, Filter.liminf_le_iff, LT.lt.trans