awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f g : α → β
hfg : f =ᶠ[ae μ] g
⊢ essInf f μ = essInf g μ

Tactic:
@essSup_congr_ae α βᵒᵈ _ _ _ _ _ hfg

Premises used: Filter.limsInf, Filter.liminf, setOf, essInf, OrderDual, essSup_congr_ae
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
inst_1 : NeZero μ
c : β
⊢ essSup (fun (x : α) ↦ c) μ = c

Tactic:
limsup_const _

Premises used: Filter.limsup_const, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
inst_1 : NeZero μ
c : β
⊢ essInf (fun (x : α) ↦ c) μ = c

Tactic:
liminf_const _

Premises used: essInf, Filter.liminf_const
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
c : β
hμ : μ ≠ 0
⊢ essSup (fun (x : α) ↦ c) μ = c

Tactic:
have := NeZero.mk hμ; essSup_const' _

Premises used: NeZero.mk, essSup_const'
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
c : β
hμ : μ ≠ 0
⊢ essInf (fun (x : α) ↦ c) μ = c

Tactic:
have := NeZero.mk hμ; essInf_const' _

Premises used: NeZero.mk, essInf_const'
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f g : α → β
hfg : f ≤ᶠ[ae μ] g
hf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) f
hg : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) g
⊢ essSup f μ ≤ essSup g μ

Tactic:
limsup_le_limsup hfg hf hg

Premises used: Filter.limsup_le_limsup, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f g : α → β
hfg : f ≤ᶠ[ae μ] g
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae μ) f
hg : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae μ) g
⊢ essInf f μ ≤ essInf g μ

Tactic:
liminf_le_liminf hfg hf hg

Premises used: essInf, Filter.liminf_le_liminf
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
c : β
hf : f ≤ᶠ[ae μ] fun (x : α) ↦ c
hfbdd : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) f
⊢ essSup f μ ≤ c

Tactic:
limsup_le_of_le hfbdd hf

Premises used: Filter.limsup_le_of_le, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
c : β
hf : (fun (x : α) ↦ c) ≤ᶠ[ae μ] f
hfbdd : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae μ) f
⊢ c ≤ essInf f μ

Tactic:
le_liminf_of_le hfbdd hf

Premises used: essInf, Filter.le_liminf_of_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice β
x : MeasurableSpace α
γ : Type u_3
inst_1 : ConditionallyCompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) f
hf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) f
hgf : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) (ae μ) fun (x : α) ↦ (g : (a : β) → γ) (f x)
hgf_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) (ae μ) fun (x : α) ↦ (g : (a : β) → γ) (f x)
⊢ Eq.{u_3 + 1} (α := γ) ((g : (a : β) → γ) (essSup f μ) : γ) (essSup (fun (x : α) ↦ (g : (a : β) → γ) (f x)) μ : γ)

Tactic:
OrderIso.limsup_apply g hf hf_co hgf hgf_co

Premises used: OrderIso.limsup_apply, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice β
x : MeasurableSpace α
γ : Type u_3
inst_1 : ConditionallyCompleteLattice γ
f : α → β
μ : Measure α
g : β ≃o γ
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae μ) f
hf_co : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae μ) f
hgf : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≥ x2) (ae μ) fun (x : α) ↦ (g : (a : β) → γ) (f x)
hgf_co : IsCoboundedUnder (fun (x1 x2 : γ) ↦ x1 ≥ x2) (ae μ) fun (x : α) ↦ (g : (a : β) → γ) (f x)
⊢ Eq.{u_3 + 1} (α := γ) ((g : (a : β) → γ) (essInf f μ) : γ) (essInf (fun (x : α) ↦ (g : (a : β) → γ) (f x)) μ : γ)

Tactic:
OrderIso.liminf_apply g hf hf_co hgf hgf_co

Premises used: essInf, OrderIso.liminf_apply
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
hμν : ν ≪ μ
hνf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae ν) f
hμf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) f
⊢ essSup f ν ≤ essSup f μ

Tactic:
limsup_le_limsup_of_le (Measure.ae_le_iff_absolutelyContinuous.mpr hμν) hνf hμf

Premises used: Iff.mpr, MeasureTheory.Measure.ae_le_iff_absolutelyContinuous, essSup, Filter.limsup_le_limsup_of_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
hμν : ν ≤ μ
hνf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae ν) f
hμf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) f
⊢ essSup f ν ≤ essSup f μ

Tactic:
essSup_mono_measure (Measure.absolutelyContinuous_of_le hμν) hνf hμf

Premises used: essSup_mono_measure, MeasureTheory.Measure.absolutelyContinuous_of_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst : ConditionallyCompleteLattice β
f : α → β
hμν : μ ≪ ν
hνf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae ν) f
hμf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) (ae μ) f
⊢ essInf f ν ≤ essInf f μ

Tactic:
liminf_le_liminf_of_le (Measure.ae_le_iff_absolutelyContinuous.mpr hμν) hνf hμf

Premises used: Iff.mpr, essInf, MeasureTheory.Measure.ae_le_iff_absolutelyContinuous, Filter.liminf_le_liminf_of_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f μ
hgf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
⊢ essSup (g ∘ f) μ ≤ @essSup _ _ _ mγ g (Measure.map f μ)

Tactic:
limsSup_le_limsSup_of_le ?_ hgf hg

Premises used: Filter.limsup, essSup, Filter.limsSup_le_limsSup_of_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f μ
hgf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
refine : map (g ∘ f) (ae μ) ≤ map g (ae (F := Measure γ) (Measure.map f μ))
⊢ essSup (g ∘ f) μ ≤ @essSup _ _ _ mγ g (Measure.map f μ)

Tactic:
refine limsSup_le_limsSup_of_le ?_ hgf hg

Premises used: Filter.limsSup_le_limsSup_of_le
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f μ
hgf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
rw : map g (map f (ae μ)) ≤ map g (ae (F := Measure γ) (Measure.map f μ))
⊢ map (g ∘ f) (ae μ) ≤ map g (ae (F := Measure γ) (Measure.map f μ))

Tactic:
rw [← map_map]

Premises used: Filter.map_map
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f μ
hgf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
⊢ map g (map f (ae μ)) ≤ map g (ae (F := Measure γ) (Measure.map f μ))

Tactic:
map_mono (Measure.tendsto_ae_map hf)

Premises used: Filter.map_mono, MeasureTheory.Measure.tendsto_ae_map
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f μ
hgf : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
⊢ map g (map f (ae μ)) ≤ map g (ae (F := Measure γ) (Measure.map f μ))

Tactic:
exact map_mono (Measure.tendsto_ae_map hf)

Premises used: Filter.map_mono, MeasureTheory.Measure.tendsto_ae_map
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding 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 : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
le_antisymm ?_ (essSup_comp_le_essSup_map_measure hf.measurable.aemeasurable hgf_co hg)

Premises used: Measurable.aemeasurable, le_antisymm, essSup_comp_le_essSup_map_measure, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding 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 : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
refine : @essSup _ _ _ mγ g (Measure.map f μ) ≤ essSup (g ∘ f) μ
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
refine le_antisymm ?_ (essSup_comp_le_essSup_map_measure hf.measurable.aemeasurable hgf_co hg)

Premises used: Measurable.aemeasurable, le_antisymm, essSup_comp_le_essSup_map_measure, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding 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 : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
⊢ @essSup _ _ _ mγ g (Measure.map f μ) ≤ essSup (g ∘ f) μ

Tactic:
limsSup_le_limsSup hg_co hgf (fun c h_le => ?_)

Premises used: Filter.limsSup_le_limsSup, Filter.limsup, essSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding 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 : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
refine :
  ∀ (c : β) (h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c),
    ∀ᶠ (n : β) in map g (ae (F := Measure γ) (Measure.map f μ)), n ≤ c
⊢ @essSup _ _ _ mγ g (Measure.map f μ) ≤ essSup (g ∘ f) μ

Tactic:
refine limsSup_le_limsSup hg_co hgf (fun c h_le => ?_)

Premises used: Filter.limsSup_le_limsSup
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding 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 : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c
rw : ∀ (h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c), ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
⊢ ∀ᶠ (n : β) in map g (ae (F := Measure γ) (Measure.map f μ)), n ≤ c

Tactic:
rw [eventually_map] at h_le ⊢

Premises used: Filter.eventually_map
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding 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 : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c

Tactic:
hf.ae_map_iff.mpr h_le

Premises used: Iff.mpr, MeasurableEmbedding.ae_map_iff
-- Module: Mathlib.MeasureTheory.Function.EssSup
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding 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 : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) g
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c

Tactic:
exact hf.ae_map_iff.mpr h_le

Premises used: Iff.mpr, MeasurableEmbedding.ae_map_iff
-- 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 : Measurable g
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
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
le_antisymm ?_ (essSup_comp_le_essSup_map_measure hf hgf_co hg_bdd)

Premises used: le_antisymm, essSup_comp_le_essSup_map_measure
-- 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 : Measurable g
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
refine : @essSup _ _ _ mγ g (Measure.map f μ) ≤ essSup (g ∘ f) μ
⊢ @essSup _ _ _ mγ g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
refine le_antisymm ?_ (essSup_comp_le_essSup_map_measure hf hgf_co hg_bdd)

Premises used: le_antisymm, essSup_comp_le_essSup_map_measure
-- 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 : Measurable g
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
⊢ @essSup _ _ _ mγ g (Measure.map f μ) ≤ essSup (g ∘ f) μ

Tactic:
limsSup_le_limsSup hg_co hgf (fun c h_le => ?_)

Premises used: Filter.limsSup_le_limsSup, Filter.limsup, essSup
-- 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 : Measurable g
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
refine :
  ∀ (c : β) (h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c),
    ∀ᶠ (n : β) in map g (ae (F := Measure γ) (Measure.map f μ)), n ≤ c
⊢ @essSup _ _ _ mγ g (Measure.map f μ) ≤ essSup (g ∘ f) μ

Tactic:
refine limsSup_le_limsSup hg_co hgf (fun c h_le => ?_)

Premises used: Filter.limsSup_le_limsSup
-- 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 : Measurable g
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
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c
rw : ∀ (h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c), ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
⊢ ∀ᶠ (n : β) in map g (ae (F := Measure γ) (Measure.map f μ)), n ≤ c

Tactic:
rw [eventually_map] at h_le ⊢

Premises used: Filter.eventually_map
-- 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 : Measurable g
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
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
rw : ∀ᵐ (x : α) ∂μ, g (f x) ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c

Tactic:
rw [ae_map_iff hf (measurableSet_le hg measurable_const)]

Premises used: measurableSet_le, MeasureTheory.ae_map_iff, measurable_const
-- 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 : Measurable g
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
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (x : α) ∂μ, g (f x) ≤ c

Tactic:
h_le
-- 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 : Measurable g
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
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (x : α) ∂μ, g (f x) ≤ c

Tactic:
exact h_le
-- 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
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)

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

Premises used: Filter.map_congr, Filter.IsCoboundedUnder, AEMeasurable.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
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) (ae (F := Measure γ) (Measure.map f μ)) (AEMeasurable.mk g hg)

Tactic:
have hg_mk_co : IsCoboundedUnder (· ≤ ·) (ae (Measure.map f μ)) (hg.mk g) := by
    simpa [IsCoboundedUnder, ← map_congr hg.ae_eq_mk]