awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set G
h :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HSMul.hSMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h₁ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h₂ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
h₃ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HDiv.hDiv (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
h₄ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HDiv.hDiv (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
h₅ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HDiv.hDiv (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
h₆ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
    ((HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) • ν' :
          (a : Set G) → ℝ≥0∞)
        t :
      ℝ≥0∞)
have h₇ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
    measure_mul_measure_eq μ' ν' s t h2s h3s, mul_div_assoc, ENNReal.mul_div_cancel h2s h3s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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
inst_7 : ν.IsMulRightInvariant
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.1 * z.2, z.1⁻¹)) (μ.prod ν) (μ.prod ν)
have h : Eq.{u_1 + 1} (α := G × G → G × G) (fun (z : G × G) ↦ (z.1 * z.2, z.1⁻¹))
  ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2))
Tactic: convert!
    (measurePreserving_prod_div_swap ν μ).comp (measurePreserving_prod_mul_swap_right μ ν) using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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
inst_7 : ν.IsMulRightInvariant
⊢ Eq.{u_1 + 1} (α := G × G → G × G) (fun (z : G × G) ↦ (z.1 * z.2, z.1⁻¹))
    ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2))
have h : ∀ (x y : G),
  ((x, y).1 * (x, y).2, (x, y).1⁻¹) = ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (x, y)
Tactic: ext1 ⟨x, y⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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
inst_7 : ν.IsMulRightInvariant
x y : G
⊢ ((x, y).1 * (x, y).2, (x, y).1⁻¹) = ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (x, y)
have h : (x * y, x⁻¹) = ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (x, y)
Tactic: simp_rw [Function.comp_apply, div_mul_eq_div_div_swap, div_self', one_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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
inst_7 : ν.IsMulRightInvariant
x y : G
h h₁ : (x * y, x⁻¹) = ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (x, y)
⊢ ((x, y).1 * (x, y).2, (x, y).1⁻¹) = ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (x, y)
have h₂ : (x * y, x⁻¹) = (x * y, y / (x * y))
Tactic: simp_rw [Function.comp_apply, div_mul_eq_div_div_swap, div_self', one_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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
inst_7 : ν.IsMulRightInvariant
x y : G
h h₁ : (x * y, x⁻¹) = ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (x, y)
h₂ : (x * y, x⁻¹) = (x * y, y / (x * y))
⊢ ((x, y).1 * (x, y).2, (x, y).1⁻¹) = ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (x, y)
have h₃ : (x * y, x⁻¹) = (x * y, y / y / x)
Tactic: simp_rw [Function.comp_apply, div_mul_eq_div_div_swap, div_self', one_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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
inst_7 : ν.IsMulRightInvariant
x y : G
h h₁ : (x * y, x⁻¹) = ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (x, y)
h₂ : (x * y, x⁻¹) = (x * y, y / (x * y))
h₃ : (x * y, x⁻¹) = (x * y, y / y / x)
⊢ ((x, y).1 * (x, y).2, (x, y).1⁻¹) = ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (x, y)
have h₄ : (x * y, x⁻¹) = (x * y, 1 / x)
Tactic: simp_rw [Function.comp_apply, div_mul_eq_div_div_swap, div_self', one_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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
⊢ QuasiMeasurePreserving Inv.inv μ μ
have rw : QuasiMeasurePreserving Inv.inv μ.inv.inv μ.inv.inv
Tactic: rw [← μ.inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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) μ μ
have simp_rw : QuasiMeasurePreserving (fun (h : G) ↦ g * h⁻¹) μ μ
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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) μ μ
have rw : QuasiMeasurePreserving (fun (h : G) ↦ g / h) μ.inv.inv μ.inv.inv
Tactic: rw [← μ.inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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 ν) μ
have refine : ∀ (y : G), QuasiMeasurePreserving (fun (x : G) ↦ (x, y).1 / (x, y).2) μ μ
Tactic: refine QuasiMeasurePreserving.prod_of_left measurable_div (Eventually.of_forall fun y => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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) μ μ
have 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∞)
Tactic: refine ⟨measurable_mul_const g, AbsolutelyContinuous.mk fun s hs => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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
⊢ 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∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
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) μ μ
have this : QuasiMeasurePreserving (fun (h : G) ↦ h * g⁻¹) μ.inv.inv μ.inv.inv
Tactic: have :=
    (quasiMeasurePreserving_mul_right μ.inv g⁻¹).mono (inv_absolutelyContinuous μ.inv)
      (absolutelyContinuous_inv μ.inv)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
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) ↦ g * h) μ μ
have this₁ : QuasiMeasurePreserving (fun (h : G) ↦ h * g⁻¹) μ μ
Tactic: rw [μ.inv_inv] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
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 (fun (h : G) ↦ g * h) μ μ
have this₁ : 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 μ))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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 μ
⊢ IntegrableAtFilter f l μ
have obtain : ∀ (C : ℝ) (hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖), IntegrableAtFilter f l μ
Tactic: obtain ⟨C, hC⟩ := hf.bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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‖
⊢ IntegrableAtFilter f l μ
have 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 μ
Tactic: obtain ⟨s, hsl, hsm, hfg, hf, hg⟩ :=
    (hC.smallSets.and <| hfm.eventually.and hg.eventually).exists_measurable_mem_of_smallSets
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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 μ
have refine : ∀ᵐ (a : α) ∂μ.restrict s, ‖f a‖ ≤ ‖C * ‖g a‖‖
Tactic: refine ⟨s, hsl, (hg.norm.const_mul C).mono hf ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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‖‖
have refine : ∀ (x : α) (hx : x ∈ s), ‖f x‖ ≤ ‖C * ‖g x‖‖
Tactic: refine (ae_restrict_mem hsm).mono fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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 μ
⊢ Integrable f μ
have rewrite : ∀ (hg : IntegrableAtFilter g ⊤ μ), IntegrableAtFilter f ⊤ μ
Tactic: rewrite [← integrableAtFilter_top] at *
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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)
⊢ ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ
have 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 μ
Tactic: obtain ⟨C, hC⟩ := hf.bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ
have 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 μ
Tactic: obtain ⟨t, htl, ht⟩ := hC.exists_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ
have 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 μ
Tactic: obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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
⊢ ∀ᶠ (x : α) in l, IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ
have 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 μ
Tactic: obtain ⟨w, hwl, hw⟩ := hfm.exists_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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 μ
have refine : ∀ (x : α) (hx : x ∈ w ∩ v), 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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (hypothesis)
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 : α
hx : x ∈ w ∩ v
⊢ IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ
have this : IsFiniteMeasure (μ.restrict s)
Tactic: haveI : IsFiniteMeasure (μ.restrict s) := ⟨Measure.restrict_apply_univ s ▸ hμ⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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 : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
⊢ IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ
have refine : ∀ᵐ (a : ι) ∂μ.restrict s, ‖f (a, x)‖ ≤ C * ‖g x‖
Tactic: refine Integrable.mono' (integrable_const (C * ‖g x‖)) (hw x hx.1) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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 : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
⊢ ∀ᵐ (a : ι) ∂μ.restrict s, ‖f (a, x)‖ ≤ C * ‖g x‖
have h : ∀ a ∈ s, ‖f (a, x)‖ ≤ C * ‖g x‖
Tactic: filter_upwards [MeasureTheory.self_mem_ae_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
⊢ IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g
have obtain : ∀ (C : ℝ) (hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖),
  IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g
Tactic: obtain ⟨C, hC⟩ := hf.bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Asymptotics (goal)
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 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
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‖
⊢ IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g
have obtain : ∀ (t : Set (ι × α)) (htl : t ∈ 𝓟 s ×ˢ l) (ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖),
  IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g
Tactic: obtain ⟨t, htl, ht⟩ := hC.exists_mem