awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : SecondCountableTopology β
inst_4 : OrderClosedTopology β
inst_5 : OpensMeasurableSpace β
hg : AEMeasurable (_m := mγ) g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hgf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)

Tactic:
simpa [IsBoundedUnder, ← map_congr hg.ae_eq_mk]

Premises used: Filter.map_congr, AEMeasurable.ae_eq_mk, Filter.IsBoundedUnder
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : SecondCountableTopology β
inst_4 : OrderClosedTopology β
inst_5 : OpensMeasurableSpace β
hg : AEMeasurable (_m := mγ) g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hgf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)

Tactic:
have hg_mk_bdd : IsBoundedUnder (· ≤ ·) (ae (Measure.map f μ)) (hg.mk g) := by
    simpa [IsBoundedUnder, ← map_congr hg.ae_eq_mk]
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : SecondCountableTopology β
inst_4 : OrderClosedTopology β
inst_5 : OpensMeasurableSpace β
hg : AEMeasurable (_m := mγ) g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hgf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
⊢ g ∘ f =ᶠ[ae μ] AEMeasurable.mk g hg ∘ f

Tactic:
have h_eq := ae_eq_comp hf hg.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : SecondCountableTopology β
inst_4 : OrderClosedTopology β
inst_5 : OpensMeasurableSpace β
hg : AEMeasurable (_m := mγ) g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hgf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᶠ[ae μ] AEMeasurable.mk g hg ∘ f
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)

Tactic:
simpa [IsBoundedUnder, ← map_congr h_eq]

Premises used: Filter.map_congr, Filter.IsBoundedUnder
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : SecondCountableTopology β
inst_4 : OrderClosedTopology β
inst_5 : OpensMeasurableSpace β
hg : AEMeasurable (_m := mγ) g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hgf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᶠ[ae μ] AEMeasurable.mk g hg ∘ f
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)

Tactic:
have hg_mk_f : IsBoundedUnder (· ≤ ·) (ae μ) ((hg.mk g) ∘ f) := by
    simpa [IsBoundedUnder, ← map_congr h_eq]
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : SecondCountableTopology β
inst_4 : OrderClosedTopology β
inst_5 : OpensMeasurableSpace β
hg : AEMeasurable (_m := mγ) g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hgf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᶠ[ae μ] AEMeasurable.mk g hg ∘ f
hg_mk_f : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)

Tactic:
simpa [IsCoboundedUnder, ← map_congr h_eq]

Premises used: Filter.map_congr, Filter.IsCoboundedUnder
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : SecondCountableTopology β
inst_4 : OrderClosedTopology β
inst_5 : OpensMeasurableSpace β
hg : AEMeasurable (_m := mγ) g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hgf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᶠ[ae μ] AEMeasurable.mk g hg ∘ f
hg_mk_f : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)

Tactic:
have hg_mk_f_co : IsCoboundedUnder (· ≤ ·) (ae μ) ((hg.mk g) ∘ f) := by
    simpa [IsCoboundedUnder, ← map_congr h_eq]
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : SecondCountableTopology β
inst_4 : OrderClosedTopology β
inst_5 : OpensMeasurableSpace β
hg : AEMeasurable (_m := mγ) g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hgf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᶠ[ae μ] AEMeasurable.mk g hg ∘ f
hg_mk_f : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
hg_mk_f_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
rw : essSup (AEMeasurable.mk g hg ∘ f) μ = essSup (g ∘ f) μ
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
rw [essSup_congr_ae hg.ae_eq_mk,
    essSup_map_measure_of_measurable hg.measurable_mk hf hg_mk_co hg_mk_f hg_mk_f_co hg_mk_bdd]

Premises used: essSup_map_measure_of_measurable, AEMeasurable.ae_eq_mk, essSup_congr_ae, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : SecondCountableTopology β
inst_4 : OrderClosedTopology β
inst_5 : OpensMeasurableSpace β
hg : AEMeasurable (_m := mγ) g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hgf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᶠ[ae μ] AEMeasurable.mk g hg ∘ f
hg_mk_f : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
hg_mk_f_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
⊢ essSup (AEMeasurable.mk g hg ∘ f) μ = essSup (g ∘ f) μ

Tactic:
essSup_congr_ae h_eq.symm

Premises used: essSup_congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst_1 : MeasurableSpace β
inst_2 : TopologicalSpace β
inst_3 : SecondCountableTopology β
inst_4 : OrderClosedTopology β
inst_5 : OpensMeasurableSpace β
hg : AEMeasurable (_m := mγ) g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hgf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᶠ[ae μ] AEMeasurable.mk g hg ∘ f
hg_mk_f : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
hg_mk_f_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
⊢ essSup (AEMeasurable.mk g hg ∘ f) μ = essSup (g ∘ f) μ

Tactic:
exact essSup_congr_ae h_eq.symm

Premises used: essSup_congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
inst_1 : Nonempty α
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
hf : BddAbove (range f)
rw : limsup f (ae μ) = ⨆ (a : α), f a
rw₁ : limsup f ⊤ = ⨆ (a : α), f a
rw₂ rw₃ : Eq.{u_2 + 1} (α := β) (⨆ (i : α), f i) (⨆ (a : α), f a)
⊢ essSup f μ = ⨆ (a : α), f a

Tactic:
rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_ciSup hf]

Premises used: Iff.mpr, Filter.limsup_top_eq_ciSup, MeasureTheory.ae_eq_top, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
inst_1 : Nonempty α
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
hf : BddBelow (range f)
rw : liminf f (ae μ) = ⨅ (a : α), f a
rw₁ : liminf f ⊤ = ⨅ (a : α), f a
rw₂ rw₃ : Eq.{u_2 + 1} (α := β) (⨅ (i : α), f i) (⨅ (a : α), f a)
⊢ essInf f μ = ⨅ (a : α), f a

Tactic:
rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_ciInf hf]

Premises used: Iff.mpr, MeasureTheory.ae_eq_top, essInf, Filter.liminf_top_eq_ciInf
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : ConditionallyCompleteLattice β
f : α → β
inst_1 : Nonempty α
inst_2 : MeasurableSingletonClass α
hf : BddAbove (range f)
⊢ ∀ (a : α), Ne (α := ℝ≥0∞) (((Measure.count : Measure α) : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : ConditionallyCompleteLattice β
f : α → β
inst_1 : Nonempty α
inst_2 : MeasurableSingletonClass α
hf : BddBelow (range f)
⊢ ∀ (a : α), Ne (α := ℝ≥0∞) (((Measure.count : Measure α) : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : ConditionallyCompleteLattice β
f : α → β
inst_1 : Nonempty α
inst_2 : MeasurableSingletonClass α
inst_3 : Finite α
hf : BddAbove (range f)
⊢ ∀ (a : α), Ne (α := ℝ≥0∞) (((uniformOn univ : Measure α) : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [uniformOn, cond_apply]

Premises used: ProbabilityTheory.cond_apply, ProbabilityTheory.uniformOn
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : ConditionallyCompleteLattice β
f : α → β
inst_1 : Nonempty α
inst_2 : MeasurableSingletonClass α
inst_3 : Finite α
hf : BddBelow (range f)
⊢ ∀ (a : α), Ne (α := ℝ≥0∞) (((uniformOn univ : Measure α) : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [uniformOn, cond_apply]

Premises used: ProbabilityTheory.cond_apply, ProbabilityTheory.uniformOn
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
m : MeasurableSpace α
μ : Measure α
f : α → β
dsimp :
  Eq.{u_2 + 1} (α := β) (sInf {a : β | ∀ᶠ (n : β) in map f (ae μ), n ≤ a})
    (sInf {a : β | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)})
⊢ essSup f μ = sInf {a : β | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}

Tactic:
dsimp [essSup, limsup, limsSup]

Premises used: Filter.limsSup, Filter.limsup, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ Eq.{u_2 + 1} (α := β) (sInf {a : β | ∀ᶠ (n : β) in map f (ae μ), n ≤ a})
    (sInf {a : β | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)})

Tactic:
simp only [eventually_map, ae_iff, not_le]

Premises used: not_le, Filter.eventually_map, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
m : MeasurableSpace α
μ : Measure α
f : α → β
dsimp :
  Eq.{u_2 + 1} (α := β) (sSup {a : β | ∀ᶠ (n : β) in map f (ae μ), a ≤ n})
    (sSup {a : β | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x < a} : ℝ≥0∞) (0 : ℝ≥0∞)})
⊢ essInf f μ = sSup {a : β | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x < a} : ℝ≥0∞) (0 : ℝ≥0∞)}

Tactic:
dsimp [essInf, liminf, limsInf]

Premises used: Filter.limsInf, Filter.liminf, essInf
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ Eq.{u_2 + 1} (α := β) (sSup {a : β | ∀ᶠ (n : β) in map f (ae μ), a ≤ n})
    (sSup {a : β | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x < a} : ℝ≥0∞) (0 : ℝ≥0∞)})

Tactic:
simp only [eventually_map, ae_iff, not_le]

Premises used: not_le, Filter.eventually_map, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLinearOrder β
x : β
f : α → β
hx : essSup f μ < x
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) f
⊢ ∀ᵐ (y : α) ∂μ, f y < x

Tactic:
eventually_lt_of_limsup_lt hx hf

Premises used: Filter.eventually_lt_of_limsup_lt
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLinearOrder β
x : β
f : α → β
hx : x < essInf f μ
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae μ) f
⊢ ∀ᵐ (y : α) ∂μ, x < f y

Tactic:
eventually_lt_of_lt_liminf hx hf

Premises used: Filter.eventually_lt_of_lt_liminf
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLinearOrder β
f : α → β
inst_1 : TopologicalSpace β
inst_2 : FirstCountableTopology β
inst_3 : OrderTopology β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) f
⊢ ∀ᵐ (y : α) ∂μ, f y ≤ essSup f μ

Tactic:
eventually_le_limsup hf

Premises used: eventually_le_limsup, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLinearOrder β
f : α → β
inst_1 : TopologicalSpace β
inst_2 : FirstCountableTopology β
inst_3 : OrderTopology β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae μ) f
⊢ ∀ᵐ (y : α) ∂μ, essInf f μ ≤ f y

Tactic:
eventually_liminf_le hf

Premises used: essInf, eventually_liminf_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLinearOrder β
f : α → β
inst_1 : TopologicalSpace β
inst_2 : FirstCountableTopology β
inst_3 : OrderTopology β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) f
simp_rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | ¬f y ≤ essSup f μ} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | essSup f μ < f y} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp_rw [← not_le]

Premises used: not_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLinearOrder β
f : α → β
inst_1 : TopologicalSpace β
inst_2 : FirstCountableTopology β
inst_3 : OrderTopology β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) f
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | ¬f y ≤ essSup f μ} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
ae_le_essSup hf

Premises used: Set.Mem, Filter.Eventually, setOf, ae_le_essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLinearOrder β
f : α → β
inst_1 : TopologicalSpace β
inst_2 : FirstCountableTopology β
inst_3 : OrderTopology β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) f
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | ¬f y ≤ essSup f μ} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ae_le_essSup hf

Premises used: ae_le_essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLinearOrder β
f : α → β
inst_1 : TopologicalSpace β
inst_2 : FirstCountableTopology β
inst_3 : OrderTopology β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae μ) f
simp_rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | ¬essInf f μ ≤ f y} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | f y < essInf f μ} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp_rw [← not_le]

Premises used: not_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLinearOrder β
f : α → β
inst_1 : TopologicalSpace β
inst_2 : FirstCountableTopology β
inst_3 : OrderTopology β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae μ) f
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | ¬essInf f μ ≤ f y} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
ae_essInf_le hf

Premises used: Set.Mem, Filter.Eventually, setOf, ae_essInf_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLinearOrder β
f : α → β
inst_1 : TopologicalSpace β
inst_2 : FirstCountableTopology β
inst_3 : OrderTopology β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae μ) f
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {y : α | ¬essInf f μ ≤ f y} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ae_essInf_le hf

Premises used: ae_essInf_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice β
m : MeasurableSpace α
f : α → β
⊢ Membership.mem (γ := Set β) {a : β | ∀ᶠ (n : β) in map f (ae (F := Measure α) 0), n ≤ a} ⊥

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice β
x : MeasurableSpace α
f : α → β
⊢ @essInf _ _ _ x f 0 = ⊤

Tactic:
@essSup_measure_zero α βᵒᵈ _ _ _

Premises used: Filter.limsInf, Filter.liminf, setOf, essInf, essSup_measure_zero, OrderDual
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : CompleteLattice β
⊢ Eq.{u_2 + 1} (α := β) (essSup (fun (x : α) ↦ ⊥) μ) ⊥

Tactic:
limsup_const_bot

Premises used: Filter.limsup_const_bot, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : CompleteLattice β
⊢ Eq.{u_2 + 1} (α := β) (essInf (fun (x : α) ↦ ⊤) μ) ⊤

Tactic:
liminf_const_top

Premises used: Filter.liminf_const_top, essInf
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : CompleteLattice β
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
f : α → β
rw : limsup f (ae μ) = ⨆ (i : α), f i
rw₁ : limsup f ⊤ = ⨆ (i : α), f i
rw₂ rw₃ : Eq.{u_2 + 1} (α := β) (⨆ (i : α), f i) (⨆ (i : α), f i)
⊢ essSup f μ = ⨆ (i : α), f i

Tactic:
rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_iSup]

Premises used: Iff.mpr, MeasureTheory.ae_eq_top, essSup, Filter.limsup_top_eq_iSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : CompleteLattice β
hμ : ∀ (a : α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
f : α → β
rw : liminf f (ae μ) = ⨅ (i : α), f i
rw₁ : liminf f ⊤ = ⨅ (i : α), f i
rw₂ rw₃ : Eq.{u_2 + 1} (α := β) (⨅ (i : α), f i) (⨅ (i : α), f i)
⊢ essInf f μ = ⨅ (i : α), f i

Tactic:
rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_iInf]

Premises used: Iff.mpr, MeasureTheory.ae_eq_top, essInf, Filter.liminf_top_eq_iInf