awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
g' : α → F
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
ho' : f =O[atTop] g'
hg' : IntegrableAtFilter g' atTop μ
⊢ Integrable f μ

Tactic:
integrable_iff_integrableAtFilter_atBot_atTop.mpr
    ⟨⟨ho.integrableAtFilter ?_ hg, ho'.integrableAtFilter ?_ hg'⟩, hf⟩

Premises used: Asymptotics.IsBigO.integrableAtFilter, Iff.mpr, MeasureTheory.integrable_iff_integrableAtFilter_atBot_atTop, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
g' : α → F
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
ho' : f =O[atTop] g'
hg' : IntegrableAtFilter g' atTop μ
refine_1 : StronglyMeasurableAtFilter f atBot μ
refine_2 : StronglyMeasurableAtFilter f atTop μ
⊢ Integrable f μ

Tactic:
refine integrable_iff_integrableAtFilter_atBot_atTop.mpr
    ⟨⟨ho.integrableAtFilter ?_ hg, ho'.integrableAtFilter ?_ hg'⟩, hf⟩

Premises used: Asymptotics.IsBigO.integrableAtFilter, Iff.mpr, MeasureTheory.integrable_iff_integrableAtFilter_atBot_atTop, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
g' : α → F
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
ho' : f =O[atTop] g'
hg' : IntegrableAtFilter g' atTop μ
⊢ StronglyMeasurableAtFilter f atBot μ

Tactic:
hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter, MeasureTheory.LocallyIntegrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
g' : α → F
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
ho' : f =O[atTop] g'
hg' : IntegrableAtFilter g' atTop μ
⊢ StronglyMeasurableAtFilter f atBot μ

Tactic:
exact hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter, MeasureTheory.LocallyIntegrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
g' : α → F
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
ho' : f =O[atTop] g'
hg' : IntegrableAtFilter g' atTop μ
⊢ StronglyMeasurableAtFilter f atTop μ

Tactic:
hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter, MeasureTheory.LocallyIntegrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
g' : α → F
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
ho' : f =O[atTop] g'
hg' : IntegrableAtFilter g' atTop μ
⊢ StronglyMeasurableAtFilter f atTop μ

Tactic:
exact hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter, MeasureTheory.LocallyIntegrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
hf : LocallyIntegrableOn f (Iic a) μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ IntegrableOn f (Iic a) μ

Tactic:
integrableOn_Iic_iff_integrableAtFilter_atBot.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Premises used: Asymptotics.IsBigO.integrableAtFilter, Iff.mpr, And.intro, MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBot
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
hf : LocallyIntegrableOn f (Iic a) μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
refine : StronglyMeasurableAtFilter f atBot μ
⊢ IntegrableOn f (Iic a) μ

Tactic:
refine integrableOn_Iic_iff_integrableAtFilter_atBot.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Premises used: Asymptotics.IsBigO.integrableAtFilter, Iff.mpr, And.intro, MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBot
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
hf : LocallyIntegrableOn f (Iic a) μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ StronglyMeasurableAtFilter f atBot μ

Tactic:
⟨Iic a, Iic_mem_atBot a, hf.aestronglyMeasurable⟩

Premises used: StronglyMeasurableAtFilter, Filter.Iic_mem_atBot, And.intro, Exists.intro, Set.Iic, MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
hf : LocallyIntegrableOn f (Iic a) μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ StronglyMeasurableAtFilter f atBot μ

Tactic:
exact ⟨Iic a, Iic_mem_atBot a, hf.aestronglyMeasurable⟩
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrableOn f (Ici a) μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ IntegrableOn f (Ici a) μ

Tactic:
integrableOn_Ici_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Premises used: Asymptotics.IsBigO.integrableAtFilter, Iff.mpr, And.intro, MeasureTheory.integrableOn_Ici_iff_integrableAtFilter_atTop
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrableOn f (Ici a) μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
refine : StronglyMeasurableAtFilter f atTop μ
⊢ IntegrableOn f (Ici a) μ

Tactic:
refine integrableOn_Ici_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Premises used: Asymptotics.IsBigO.integrableAtFilter, Iff.mpr, And.intro, MeasureTheory.integrableOn_Ici_iff_integrableAtFilter_atTop
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrableOn f (Ici a) μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ StronglyMeasurableAtFilter f atTop μ

Tactic:
⟨Ici a, Ici_mem_atTop a, hf.aestronglyMeasurable⟩

Premises used: Set.Ici, StronglyMeasurableAtFilter, Filter.Ici_mem_atTop, And.intro, Exists.intro, MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atTop
hf : LocallyIntegrableOn f (Ici a) μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ StronglyMeasurableAtFilter f atTop μ

Tactic:
exact ⟨Ici a, Ici_mem_atTop a, hf.aestronglyMeasurable⟩
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : OrderTop α
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ Integrable f μ

Tactic:
integrable_iff_integrableAtFilter_atBot.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Premises used: Asymptotics.IsBigO.integrableAtFilter, Iff.mpr, MeasureTheory.integrable_iff_integrableAtFilter_atBot, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : OrderTop α
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
refine : StronglyMeasurableAtFilter f atBot μ
⊢ Integrable f μ

Tactic:
refine integrable_iff_integrableAtFilter_atBot.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Premises used: Asymptotics.IsBigO.integrableAtFilter, Iff.mpr, MeasureTheory.integrable_iff_integrableAtFilter_atBot, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : OrderTop α
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ StronglyMeasurableAtFilter f atBot μ

Tactic:
hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter, MeasureTheory.LocallyIntegrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atBot
inst_8 : OrderTop α
hf : LocallyIntegrable f μ
ho : f =O[atBot] g
hg : IntegrableAtFilter g atBot μ
⊢ StronglyMeasurableAtFilter f atBot μ

Tactic:
exact hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter, MeasureTheory.LocallyIntegrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_8 : OrderBot α
hf : LocallyIntegrable f μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ Integrable f μ

Tactic:
integrable_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Premises used: Asymptotics.IsBigO.integrableAtFilter, Iff.mpr, MeasureTheory.integrable_iff_integrableAtFilter_atTop, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_8 : OrderBot α
hf : LocallyIntegrable f μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
refine : StronglyMeasurableAtFilter f atTop μ
⊢ Integrable f μ

Tactic:
refine integrable_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Premises used: Asymptotics.IsBigO.integrableAtFilter, Iff.mpr, MeasureTheory.integrable_iff_integrableAtFilter_atTop, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_8 : OrderBot α
hf : LocallyIntegrable f μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ StronglyMeasurableAtFilter f atTop μ

Tactic:
hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter, MeasureTheory.LocallyIntegrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : LinearOrder α
inst_6 : CompactIccSpace α
inst_7 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_8 : OrderBot α
hf : LocallyIntegrable f μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ StronglyMeasurableAtFilter f atTop μ

Tactic:
exact hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter, MeasureTheory.LocallyIntegrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ IntegrableOn f (Ici 0) μ

Tactic:
have h_int := (hf.locallyIntegrableOn (Ici 0)).integrableOn_of_isBigO_atTop ho hg
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
rw : IntegrableOn f (Iic 0) μ ∧ IntegrableOn f (Ici 0) μ
rw₁ : α
⊢ Integrable f μ

Tactic:
rw [← integrableOn_univ, ← Iic_union_Ici_of_le le_rfl, integrableOn_union]

Premises used: MeasureTheory.integrableOn_union, le_rfl, Set.Iic_union_Ici_of_le, MeasureTheory.integrableOn_univ
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ IntegrableOn f (Iic 0) μ ∧ IntegrableOn f (Ici 0) μ

Tactic:
⟨?_, h_int⟩

Premises used: And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
rhs : μ.restrict (Iic 0)
| Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)

Tactic:
rhs
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
rw : Measure.map Neg.neg (μ.restrict (Neg.neg ⁻¹' Iic 0))
| μ.restrict (Iic 0)

Tactic:
rw [← Measure.map_neg_eq_self μ, measurableEmbedding_neg.restrict_map]

Premises used: MeasurableEmbedding.restrict_map, measurableEmbedding_neg, MeasureTheory.Measure.map_neg_eq_self
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
rw : Measure.map Neg.neg (μ.restrict (Neg.neg ⁻¹' Iic 0))
| Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)

Tactic:
rhs; rw [← Measure.map_neg_eq_self μ, measurableEmbedding_neg.restrict_map]

Premises used: MeasurableEmbedding.restrict_map, measurableEmbedding_neg, MeasureTheory.Measure.map_neg_eq_self
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
conv :
  Eq (α := Measure α) (Measure.map Neg.neg (μ.restrict (Ici 0))) (Measure.map Neg.neg (μ.restrict (Neg.neg ⁻¹' Iic 0)))
⊢ Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)

Tactic:
conv => rhs; rw [← Measure.map_neg_eq_self μ, measurableEmbedding_neg.restrict_map]

Premises used: MeasurableEmbedding.restrict_map, measurableEmbedding_neg, MeasureTheory.Measure.map_neg_eq_self
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ Eq (α := Measure α) (Measure.map Neg.neg (μ.restrict (Ici 0))) (Measure.map Neg.neg (μ.restrict (Neg.neg ⁻¹' Iic 0)))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)

Tactic:
have h_map_neg : (μ.restrict (Ici 0)).map Neg.neg = μ.restrict (Iic 0) := by
    conv => rhs; rw [← Measure.map_neg_eq_self μ, measurableEmbedding_neg.restrict_map]
    simp