awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ QuasiMeasurePreserving (fun (h : G) ↦ g * h⁻¹) μ μ

Tactic:
(measurePreserving_mul_left μ g).quasiMeasurePreserving.comp (quasiMeasurePreserving_inv μ)

Premises used: MeasureTheory.measurePreserving_mul_left, MeasureTheory.Measure.QuasiMeasurePreserving.comp, MeasureTheory.MeasurePreserving.quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ QuasiMeasurePreserving (fun (h : G) ↦ g * h⁻¹) μ μ

Tactic:
exact
    (measurePreserving_mul_left μ g).quasiMeasurePreserving.comp (quasiMeasurePreserving_inv μ)

Premises used: MeasureTheory.measurePreserving_mul_left, MeasureTheory.Measure.QuasiMeasurePreserving.comp, MeasureTheory.MeasurePreserving.quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulRightInvariant
g : G
rw : QuasiMeasurePreserving (fun (h : G) ↦ g / h) μ.inv.inv μ.inv.inv
⊢ QuasiMeasurePreserving (fun (h : G) ↦ g / h) μ μ

Tactic:
rw [← μ.inv_inv]

Premises used: MeasureTheory.Measure.inv_inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulRightInvariant
g : G
⊢ QuasiMeasurePreserving (fun (h : G) ↦ g / h) μ.inv.inv μ.inv.inv

Tactic:
(quasiMeasurePreserving_div_left μ.inv g).mono (inv_absolutelyContinuous μ.inv)
      (absolutelyContinuous_inv μ.inv)

Premises used: MeasureTheory.inv_absolutelyContinuous, MeasureTheory.absolutelyContinuous_inv, MeasureTheory.quasiMeasurePreserving_div_left, MeasureTheory.Measure.inv, MeasureTheory.Measure.QuasiMeasurePreserving.mono
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulRightInvariant
g : G
⊢ QuasiMeasurePreserving (fun (h : G) ↦ g / h) μ.inv.inv μ.inv.inv

Tactic:
exact
    (quasiMeasurePreserving_div_left μ.inv g).mono (inv_absolutelyContinuous μ.inv)
      (absolutelyContinuous_inv μ.inv)

Premises used: MeasureTheory.inv_absolutelyContinuous, MeasureTheory.absolutelyContinuous_inv, MeasureTheory.quasiMeasurePreserving_div_left, MeasureTheory.Measure.inv, MeasureTheory.Measure.QuasiMeasurePreserving.mono
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulRightInvariant
⊢ QuasiMeasurePreserving (fun (p : G × G) ↦ p.1 / p.2) (μ.prod ν) μ

Tactic:
QuasiMeasurePreserving.prod_of_left measurable_div (Eventually.of_forall fun y => ?_)

Premises used: MeasureTheory.QuasiMeasurePreserving.prod_of_left, MeasurableDiv₂.measurable_div, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulRightInvariant
refine : ∀ (y : G), QuasiMeasurePreserving (fun (x : G) ↦ (x, y).1 / (x, y).2) μ μ
⊢ QuasiMeasurePreserving (fun (p : G × G) ↦ p.1 / p.2) (μ.prod ν) μ

Tactic:
refine QuasiMeasurePreserving.prod_of_left measurable_div (Eventually.of_forall fun y => ?_)

Premises used: MeasureTheory.QuasiMeasurePreserving.prod_of_left, MeasurableDiv₂.measurable_div, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulRightInvariant
y : G
⊢ QuasiMeasurePreserving (fun (x : G) ↦ (x, y).1 / (x, y).2) μ μ

Tactic:
(measurePreserving_div_right μ y).quasiMeasurePreserving

Premises used: MeasureTheory.measurePreserving_div_right, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulRightInvariant
y : G
⊢ QuasiMeasurePreserving (fun (x : G) ↦ (x, y).1 / (x, y).2) μ μ

Tactic:
exact (measurePreserving_div_right μ y).quasiMeasurePreserving

Premises used: MeasureTheory.measurePreserving_div_right, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
⊢ QuasiMeasurePreserving (fun (p : G × G) ↦ p.1 / p.2) (μ.prod ν) μ

Tactic:
(quasiMeasurePreserving_div_of_right_invariant μ.inv ν).mono
    ((absolutelyContinuous_inv μ).prod AbsolutelyContinuous.rfl) (inv_absolutelyContinuous μ)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.prod, MeasureTheory.quasiMeasurePreserving_div_of_right_invariant, MeasureTheory.inv_absolutelyContinuous, MeasureTheory.absolutelyContinuous_inv, MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.inv, MeasureTheory.Measure.QuasiMeasurePreserving.mono
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ QuasiMeasurePreserving (fun (h : G) ↦ h * g) μ μ

Tactic:
⟨measurable_mul_const g, AbsolutelyContinuous.mk fun s hs => ?_⟩

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk, MeasureTheory.Measure.QuasiMeasurePreserving.mk, MeasurableMul.measurable_mul_const
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
refine :
  ∀ (s : Set G) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) (((map (fun (h : G) ↦ h * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ QuasiMeasurePreserving (fun (h : G) ↦ h * g) μ μ

Tactic:
refine ⟨measurable_mul_const g, AbsolutelyContinuous.mk fun s hs => ?_⟩
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) (((map (fun (h : G) ↦ h * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.measure_mul_right_null, MeasurableMul.measurable_mul_const
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulRightInvariant
g : G
⊢ QuasiMeasurePreserving (fun (h : G) ↦ h * g⁻¹) μ.inv.inv μ.inv.inv

Tactic:
have :=
    (quasiMeasurePreserving_mul_right μ.inv g⁻¹).mono (inv_absolutelyContinuous μ.inv)
      (absolutelyContinuous_inv μ.inv)
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulRightInvariant
g : G
this : QuasiMeasurePreserving (fun (h : G) ↦ h * g⁻¹) μ.inv.inv μ.inv.inv
⊢ QuasiMeasurePreserving (fun (h : G) ↦ h * g⁻¹) μ μ

Tactic:
rw [μ.inv_inv] at this

Premises used: MeasureTheory.Measure.inv_inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulRightInvariant
g : G
this : QuasiMeasurePreserving (fun (h : G) ↦ h * g⁻¹) μ μ
⊢ QuasiMeasurePreserving (Inv.inv ∘ (fun (h : G) ↦ h * g⁻¹) ∘ Inv.inv) μ μ

Tactic:
have :=
    (quasiMeasurePreserving_inv_of_right_invariant μ).comp
      (this.comp (quasiMeasurePreserving_inv_of_right_invariant μ))
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulRightInvariant
g : G
this_1 : QuasiMeasurePreserving (fun (h : G) ↦ h * g⁻¹) μ μ
this : QuasiMeasurePreserving (Inv.inv ∘ (fun (h : G) ↦ h * g⁻¹) ∘ Inv.inv) μ μ
⊢ QuasiMeasurePreserving (fun (x : G) ↦ g * x) μ μ

Tactic:
simp_rw [Function.comp_def, mul_inv_rev, inv_inv] at this

Premises used: Function.comp_def, inv_inv, mul_inv_rev
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulRightInvariant
g : G
this_1 : QuasiMeasurePreserving (fun (h : G) ↦ h * g⁻¹) μ μ
this : QuasiMeasurePreserving (fun (x : G) ↦ g * x) μ μ
⊢ QuasiMeasurePreserving (fun (h : G) ↦ g * h) μ μ

Tactic:
this
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulRightInvariant
g : G
this_1 : QuasiMeasurePreserving (fun (h : G) ↦ h * g⁻¹) μ μ
this : QuasiMeasurePreserving (fun (x : G) ↦ g * x) μ μ
⊢ QuasiMeasurePreserving (fun (h : G) ↦ g * h) μ μ

Tactic:
exact this
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst_1 : MeasurableSpace α
inst_2 : NormedAddCommGroup F
μ : Measure α
inst_3 : l.IsMeasurablyGenerated
hf : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg : IntegrableAtFilter g l μ
obtain : ∀ (C : ℝ) (hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖), IntegrableAtFilter f l μ
⊢ IntegrableAtFilter f l μ

Tactic:
obtain ⟨C, hC⟩ := hf.bound

Premises used: Asymptotics.IsBigO.bound
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst_1 : MeasurableSpace α
inst_2 : NormedAddCommGroup F
μ : Measure α
inst_3 : l.IsMeasurablyGenerated
hf : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
obtain :
  ∀ (s : Set α) (hsl : s ∈ l) (hsm : MeasurableSet s) (hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖)
    (hf : AEStronglyMeasurable f (μ.restrict s)) (hg : IntegrableOn g s μ), IntegrableAtFilter f l μ
⊢ IntegrableAtFilter f l μ

Tactic:
obtain ⟨s, hsl, hsm, hfg, hf, hg⟩ :=
    (hC.smallSets.and <| hfm.eventually.and hg.eventually).exists_measurable_mem_of_smallSets

Premises used: Filter.Eventually.exists_measurable_mem_of_smallSets, Filter.Eventually.and, StronglyMeasurableAtFilter.eventually, Filter.Eventually.smallSets, MeasureTheory.IntegrableAtFilter.eventually
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst_1 : MeasurableSpace α
inst_2 : NormedAddCommGroup F
μ : Measure α
inst_3 : l.IsMeasurablyGenerated
hf_1 : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg_1 : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖
hf : AEStronglyMeasurable f (μ.restrict s)
hg : IntegrableOn g s μ
⊢ IntegrableAtFilter f l μ

Tactic:
⟨s, hsl, (hg.norm.const_mul C).mono hf ?_⟩

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mono, MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst_1 : MeasurableSpace α
inst_2 : NormedAddCommGroup F
μ : Measure α
inst_3 : l.IsMeasurablyGenerated
hf_1 : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg_1 : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖
hf : AEStronglyMeasurable f (μ.restrict s)
hg : IntegrableOn g s μ
refine : ∀ᵐ (a : α) ∂μ.restrict s, ‖f a‖ ≤ ‖C * ‖g a‖‖
⊢ IntegrableAtFilter f l μ

Tactic:
refine ⟨s, hsl, (hg.norm.const_mul C).mono hf ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst_1 : MeasurableSpace α
inst_2 : NormedAddCommGroup F
μ : Measure α
inst_3 : l.IsMeasurablyGenerated
hf_1 : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg_1 : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖
hf : AEStronglyMeasurable f (μ.restrict s)
hg : IntegrableOn g s μ
⊢ ∀ᵐ (a : α) ∂μ.restrict s, ‖f a‖ ≤ ‖C * ‖g a‖‖

Tactic:
(ae_restrict_mem hsm).mono fun x hx ↦ ?_

Premises used: MeasureTheory.ae_restrict_mem, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst_1 : MeasurableSpace α
inst_2 : NormedAddCommGroup F
μ : Measure α
inst_3 : l.IsMeasurablyGenerated
hf_1 : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg_1 : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖
hf : AEStronglyMeasurable f (μ.restrict s)
hg : IntegrableOn g s μ
refine : ∀ (x : α) (hx : x ∈ s), ‖f x‖ ≤ ‖C * ‖g x‖‖
⊢ ∀ᵐ (a : α) ∂μ.restrict s, ‖f a‖ ≤ ‖C * ‖g a‖‖

Tactic:
refine (ae_restrict_mem hsm).mono fun x hx ↦ ?_

Premises used: MeasureTheory.ae_restrict_mem, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst_1 : MeasurableSpace α
inst_2 : NormedAddCommGroup F
μ : Measure α
inst_3 : l.IsMeasurablyGenerated
hf_1 : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg_1 : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖
hf : AEStronglyMeasurable f (μ.restrict s)
hg : IntegrableOn g s μ
x : α
hx : x ∈ s
⊢ ‖f x‖ ≤ ‖C * ‖g x‖‖

Tactic:
(hfg x hx).trans (le_abs_self _)

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst_1 : MeasurableSpace α
inst_2 : NormedAddCommGroup F
μ : Measure α
inst_3 : l.IsMeasurablyGenerated
hf_1 : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg_1 : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖
hf : AEStronglyMeasurable f (μ.restrict s)
hg : IntegrableOn g s μ
x : α
hx : x ∈ s
⊢ ‖f x‖ ≤ ‖C * ‖g x‖‖

Tactic:
exact (hfg x hx).trans (le_abs_self _)

Premises used: le_abs_self, LE.le.trans
-- 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 : MeasurableSpace α
inst_2 : NormedAddCommGroup F
μ : Measure α
hfm : AEStronglyMeasurable f μ
hf : f =O[⊤] g
hg : Integrable g μ
rewrite : ∀ (hg : IntegrableAtFilter g ⊤ μ), IntegrableAtFilter f ⊤ μ
⊢ Integrable f μ

Tactic:
rewrite [← integrableAtFilter_top] at *

Premises used: MeasureTheory.integrableAtFilter_top
-- 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 : MeasurableSpace α
inst_2 : NormedAddCommGroup F
μ : Measure α
hfm : AEStronglyMeasurable f μ
hf : f =O[⊤] g
hg : IntegrableAtFilter g ⊤ μ
⊢ IntegrableAtFilter f ⊤ μ

Tactic:
hf.integrableAtFilter ⟨univ, univ_mem, hfm.restrict⟩ hg

Premises used: Asymptotics.IsBigO.integrableAtFilter, Set.univ, MeasureTheory.AEStronglyMeasurable.restrict, And.intro, Exists.intro, Filter.univ_mem
-- 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 : MeasurableSpace α
inst_2 : NormedAddCommGroup F
μ : Measure α
hfm : AEStronglyMeasurable f μ
hf : f =O[⊤] g
hg : IntegrableAtFilter g ⊤ μ
⊢ IntegrableAtFilter f ⊤ μ

Tactic:
exact hf.integrableAtFilter ⟨univ, univ_mem, hfm.restrict⟩ hg

Premises used: Asymptotics.IsBigO.integrableAtFilter, Set.univ, MeasureTheory.AEStronglyMeasurable.restrict, And.intro, Exists.intro, Filter.univ_mem
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
obtain :
  ∀ (C : ℝ) (hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖),
    ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ
⊢ ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ

Tactic:
obtain ⟨C, hC⟩ := hf.bound

Premises used: Asymptotics.IsBigO.bound
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
obtain :
  ∀ (t : Set (ι × α)) (htl : t ∈ 𝓟 s ×ˢ l) (ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖),
    ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ
⊢ ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ

Tactic:
obtain ⟨t, htl, ht⟩ := hC.exists_mem

Premises used: Filter.Eventually.exists_mem
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
obtain :
  ∀ (u : Set ι) (hu : u ∈ 𝓟 s) (v : Set α) (hv : v ∈ l) (huv : u ×ˢ v ⊆ t),
    ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ
⊢ ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ

Tactic:
obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl

Premises used: Iff.mp, Filter.mem_prod_iff
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
obtain :
  ∀ (w : Set α) (hwl : w ∈ l)
    (hw : ∀ y ∈ w, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, y)) (μ.restrict s)),
    ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ
⊢ ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ

Tactic:
obtain ⟨w, hwl, hw⟩ := hfm.exists_mem

Premises used: Filter.Eventually.exists_mem
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, y)) (μ.restrict s)
⊢ ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ

Tactic:
eventually_iff_exists_mem.mpr ⟨w ∩ v, inter_mem hwl hv, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Filter.inter_mem, Inter.inter, And.intro, Exists.intro, Filter.eventually_iff_exists_mem
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, y)) (μ.restrict s)
refine : ∀ (x : α) (hx : x ∈ w ∩ v), IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ
⊢ ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ

Tactic:
refine eventually_iff_exists_mem.mpr ⟨w ∩ v, inter_mem hwl hv, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Filter.inter_mem, Inter.inter, And.intro, Exists.intro, Filter.eventually_iff_exists_mem