awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ ∫⁻ (a : β), f x * φ (x, a) ∂ν = ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map (fun (z : α × β) ↦ z.1) (μ.prod ν) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
funProp : m0 ≤ m0
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : α) ↦ f z0
funProp₂ : Measure.map (fun (z : α × β) ↦ z.1) (μ.prod ν) ≪ μ
⊢ AEMeasurable ((fun (z : α × β) ↦ f z.1) * φ) (μ.prod ν)

Tactic:
fun_prop (disch := intro _ hs; simp [hs])
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
funProp : m0 ≤ m0
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : α) ↦ f z0
funProp₂ : Measure.map (fun (z : α × β) ↦ z.1) (μ.prod ν) ≪ μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)

Tactic:
fun_prop (disch := intro _ hs; simp [hs])
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ

Tactic:
fun_prop (disch := intro _ hs; simp [hs])
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : Measurable f
⊢ (μ.withDensity f).prod ν = (μ.prod ν).withDensity fun (z : α × β) ↦ f z.1

Tactic:
prod_withDensity_left₀ hf.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.prod_withDensity_left₀
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
⊢ μ.prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) ↦ g z.2

Tactic:
ext_of_lintegral _ fun φ hφ ↦ ?_

Premises used: MeasureTheory.Measure.ext_of_lintegral
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
refine :
  ∀ (φ : α × β → ℝ≥0∞) (hφ : Measurable φ),
    ∫⁻ (a : α × β), φ a ∂μ.prod (ν.withDensity g) = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ g z.2
⊢ μ.prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) ↦ g z.2

Tactic:
refine ext_of_lintegral _ fun φ hφ ↦ ?_

Premises used: MeasureTheory.Measure.ext_of_lintegral
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
rw :
  ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g ∂μ =
    ∫⁻ (x : α), ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ g z.2) φ (x, y) ∂ν ∂μ
hf : AEMeasurable ((fun (z : α × β) ↦ g z.2) * φ) (μ.prod ν)
rw₁ : AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ g z.2) (μ.prod ν)
⊢ ∫⁻ (a : α × β), φ a ∂μ.prod (ν.withDensity g) = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ g z.2

Tactic:
rw [lintegral_prod _ hφ.aemeasurable, lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable,
    lintegral_prod]

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_prod, MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g ∂μ =
    ∫⁻ (x : α), ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ g z.2) φ (x, y) ∂ν ∂μ

Tactic:
lintegral_congr (fun x ↦ ?_)

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
refine :
  ∀ (x : α),
    ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g =
      ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ g z.2) φ (x, y) ∂ν
⊢ ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g ∂μ =
    ∫⁻ (x : α), ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ g z.2) φ (x, y) ∂ν ∂μ

Tactic:
refine lintegral_congr (fun x ↦ ?_)

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y : β) ↦ φ (x, y)) ν

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
rw :
  ∫⁻ (a : β), HMul.hMul (β := β → ℝ≥0∞) g (fun (y : β) ↦ φ (x, y)) a ∂ν =
    ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ g z.2) φ (x, y) ∂ν
⊢ ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g =
    ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ g z.2) φ (x, y) ∂ν

Tactic:
rw [lintegral_withDensity_eq_lintegral_mul₀ hg (by fun_prop)]

Premises used: MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ ∫⁻ (a : β), HMul.hMul (β := β → ℝ≥0∞) g (fun (y : β) ↦ φ (x, y)) a ∂ν =
    ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ g z.2) φ (x, y) ∂ν

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
s : Set β
hs : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map (fun (z : α × β) ↦ z.2) (μ.prod ν) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
funProp : mβ ≤ mβ
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : β) ↦ g z0
funProp₂ : Measure.map (fun (z : α × β) ↦ z.2) (μ.prod ν) ≪ ν
⊢ AEMeasurable ((fun (z : α × β) ↦ g z.2) * φ) (μ.prod ν)

Tactic:
fun_prop (disch := intro _ hs; simp [hs])
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
funProp : mβ ≤ mβ
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : β) ↦ g z0
funProp₂ : Measure.map (fun (z : α × β) ↦ z.2) (μ.prod ν) ≪ ν
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ g z.2) (μ.prod ν)

Tactic:
fun_prop (disch := intro _ hs; simp [hs])
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : Measurable g
⊢ μ.prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) ↦ g z.2

Tactic:
prod_withDensity_right₀ hg.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.prod_withDensity_right₀
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
rw :
  (μ.prod ν).withDensity (HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) fun (z : α × β) ↦ g z.2) =
    (μ.prod ν).withDensity fun (z : α × β) ↦ f z.1 * g z.2
hf₁ : AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ g z.2) (μ.prod ν)
hg₁ : AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)
⊢ (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) ↦ f z.1 * g z.2

Tactic:
rw [prod_withDensity_left₀ hf, prod_withDensity_right₀ hg, ← withDensity_mul₀, mul_comm]

Premises used: MeasureTheory.withDensity_mul₀, MeasureTheory.prod_withDensity_left₀, MeasureTheory.prod_withDensity_right₀, mul_comm
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ (μ.prod ν).withDensity (HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) fun (z : α × β) ↦ g z.2) =
    (μ.prod ν).withDensity fun (z : α × β) ↦ f z.1 * g z.2

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s : Set β
hs : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map (fun (z : α × β) ↦ z.2) (μ.prod ν) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
funProp : mβ ≤ mβ
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : β) ↦ g z0
funProp₂ : Measure.map (fun (z : α × β) ↦ z.2) (μ.prod ν) ≪ ν
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ g z.2) (μ.prod ν)

Tactic:
fun_prop (disch := intro _ hs; simp [hs])
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map (fun (z : α × β) ↦ z.1) (μ.prod ν) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
funProp : m0 ≤ m0
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : α) ↦ f z0
funProp₂ : Measure.map (fun (z : α × β) ↦ z.1) (μ.prod ν) ≪ μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)

Tactic:
fun_prop (disch := intro _ hs; simp [hs])
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) ↦ f z.1 * g z.2

Tactic:
prod_withDensity₀ hf.aemeasurable hg.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.prod_withDensity₀
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
c : ℝ≥0∞
h :
  ∀ (s : Set (α × β)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.prod (c • ν) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
      ((c • μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.prod (c • ν) = c • μ.prod ν

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
h :
  ∫⁻ (x : α), HMul.hMul (β := ℝ≥0∞) c ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) ∂μ =
    c * ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ.prod (c • ν) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((c • μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [Measure.prod_apply hs, Measure.smul_apply, Measure.prod_apply hs, smul_eq_mul]

Premises used: MeasureTheory.Measure.prod_apply, MeasureTheory.Measure.smul_apply, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
h : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
⊢ ∫⁻ (x : α), HMul.hMul (β := ℝ≥0∞) c ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) ∂μ =
    c * ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ

Tactic:
rw [lintegral_const_mul]

Premises used: MeasureTheory.lintegral_const_mul
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)

Tactic:
measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)

Tactic:
exact measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
⊢ IsLocallyFiniteMeasure (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))

Tactic:
⟨fun x ↦ ?_⟩

Premises used: MeasureTheory.IsLocallyFiniteMeasure.mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
refine : ∀ (x : α), (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).FiniteAtFilter (nhds x)
⊢ IsLocallyFiniteMeasure (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))

Tactic:
refine ⟨fun x ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
rcases :
  ∀ (U : Set α) (hμU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hUf : U ⊆ {x_1 : α | (fun (a : α) ↦ f a ≤ f x + 1) x_1}) (hUx : U ∈ nhds x) (hUo : IsOpen U),
    (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).FiniteAtFilter (nhds x)
⊢ (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).FiniteAtFilter (nhds x)

Tactic:
rcases (μ.finiteAt_nhds x).exists_mem_basis ((nhds_basis_opens' x).restrict_subset
    ((hf.tendsto x).eventually_le_const (lt_add_one _))) with ⟨U, ⟨⟨hUx, hUo⟩, hUf⟩, hμU⟩

Premises used: MeasureTheory.Measure.finiteAt_nhds, lt_add_one, Filter.Tendsto.eventually_le_const, Continuous.tendsto, nhds_basis_opens', Filter.HasBasis.restrict_subset, MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hUf : U ⊆ {x_1 : α | (fun (a : α) ↦ f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).FiniteAtFilter (nhds x)

Tactic:
⟨U, hUx, ?_⟩

Premises used: MeasureTheory.Measure.FiniteAtFilter, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hUf : U ⊆ {x_1 : α | (fun (a : α) ↦ f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
refine : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞) : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).FiniteAtFilter (nhds x)

Tactic:
refine ⟨U, hUx, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hUf : U ⊆ {x_1 : α | (fun (a : α) ↦ f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
rw : ∫⁻ (a : α) in U, (↑(f a) : ℝ≥0∞) ∂μ < ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞) : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ hUo.measurableSet]

Premises used: IsOpen.measurableSet, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hUf : U ⊆ {x_1 : α | (fun (a : α) ↦ f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ ∫⁻ (a : α) in U, (↑(f a) : ℝ≥0∞) ∂μ < ∞

Tactic:
setLIntegral_lt_top_of_bddAbove hμU.ne ⟨f x + 1, forall_mem_image.2 hUf⟩

Premises used: Iff.mpr, MeasureTheory.setLIntegral_lt_top_of_bddAbove, HAdd.hAdd, Exists.intro, OfNat.ofNat, Set.forall_mem_image, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hUf : U ⊆ {x_1 : α | (fun (a : α) ↦ f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ ∫⁻ (a : α) in U, (↑(f a) : ℝ≥0∞) ∂μ < ∞

Tactic:
exact setLIntegral_lt_top_of_bddAbove hμU.ne ⟨f x + 1, forall_mem_image.2 hUf⟩

Premises used: Iff.mpr, MeasureTheory.setLIntegral_lt_top_of_bddAbove, HAdd.hAdd, Exists.intro, OfNat.ofNat, Set.forall_mem_image, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : IsLocallyFiniteMeasure μ
f : α → ℝ
hf : Continuous f
⊢ IsLocallyFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))

Tactic:
.withDensity_coe <| continuous_real_toNNReal.comp hf

Premises used: ENNReal.ofReal, Continuous.comp, MeasureTheory.IsLocallyFiniteMeasure.withDensity_coe, continuous_real_toNNReal
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
M : Type u_2
inst : Monoid M
inst_1 : MeasurableSpace M
μ ν : Measure M
inst_2 : SFinite ν
s : ℝ≥0∞
rw :
  map (fun (x : M × M) ↦ x.1 * x.2) (s • μ.prod ν) =
    HSMul.hSMul (β := Measure M) s (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν))
rw₁ rw₂ :
  HSMul.hSMul (β := Measure M) s (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν)) =
    HSMul.hSMul (β := Measure M) s (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν))
⊢ map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod (s • ν)) =
    HSMul.hSMul (β := Measure M) s (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν))

Tactic:
rw [Measure.prod_smul_right, Measure.map_smul]

Premises used: MeasureTheory.Measure.prod_smul_right, MeasureTheory.Measure.map_smul
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ μ.withDensity f ∗ₘ μ.withDensity g = μ.withDensity (f ⋆ₘₗ[μ] g)

Tactic:
ext_of_lintegral _ fun φ hφ ↦ ?_

Premises used: MeasureTheory.Measure.ext_of_lintegral
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
refine :
  ∀ (φ : G → ℝ≥0∞) (hφ : Measurable φ),
    ∫⁻ (a : G), φ a ∂μ.withDensity f ∗ₘ μ.withDensity g = ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)
⊢ μ.withDensity f ∗ₘ μ.withDensity g = μ.withDensity (f ⋆ₘₗ[μ] g)

Tactic:
refine ext_of_lintegral _ fun φ hφ ↦ ?_

Premises used: MeasureTheory.Measure.ext_of_lintegral