awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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) ∂ν ∂μ
⊢ ∫⁻ (a : α × β), φ a ∂μ.prod (ν.withDensity g) = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ g z.2
have hf : AEMeasurable ((fun (z : α × β) ↦ g z.2) * φ) (μ.prod ν)
Tactic: rw [lintegral_prod _ hφ.aemeasurable, lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable,
    lintegral_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 ν)
⊢ ∫⁻ (a : α × β), φ a ∂μ.prod (ν.withDensity g) = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ g z.2
have rw₁ : AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ g z.2) (μ.prod ν)
Tactic: rw [lintegral_prod _ hφ.aemeasurable, lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable,
    lintegral_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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) ∂ν ∂μ
have refine : ∀ (x : α),
  ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g =
    ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ g z.2) φ (x, y) ∂ν
Tactic: refine lintegral_congr (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 =
    ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ g z.2) φ (x, y) ∂ν
have rw : ∫⁻ (a : β), HMul.hMul (β := β → ℝ≥0∞) g (fun (y : β) ↦ φ (x, y)) a ∂ν =
  ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ g z.2) φ (x, y) ∂ν
Tactic: rw [lintegral_withDensity_eq_lintegral_mul₀ hg (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun (z : α × β) ↦ g z.2) * φ) (μ.prod ν)
have funProp : mβ ≤ mβ
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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β
⊢ AEMeasurable ((fun (z : α × β) ↦ g z.2) * φ) (μ.prod ν)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : β) ↦ g z0
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable ((fun (z : α × β) ↦ g z.2) * φ) (μ.prod ν)
have funProp₂ : Measure.map (fun (z : α × β) ↦ z.2) (μ.prod ν) ≪ ν
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ g z.2) (μ.prod ν)
have funProp : mβ ≤ mβ
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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β
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ g z.2) (μ.prod ν)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : β) ↦ g z0
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ g z.2) (μ.prod ν)
have funProp₂ : Measure.map (fun (z : α × β) ↦ z.2) (μ.prod ν) ≪ ν
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 ν
⊢ (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) ↦ f z.1 * g z.2
have 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
Tactic: rw [prod_withDensity_left₀ hf, prod_withDensity_right₀ hg, ← withDensity_mul₀, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) ↦ f z.1 * g z.2
have hf₁ : AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ g z.2) (μ.prod ν)
Tactic: rw [prod_withDensity_left₀ hf, prod_withDensity_right₀ hg, ← withDensity_mul₀, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 ν)
⊢ (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) ↦ f z.1 * g z.2
have hg₁ : AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)
Tactic: rw [prod_withDensity_left₀ hf, prod_withDensity_right₀ hg, ← withDensity_mul₀, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 ν
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ g z.2) (μ.prod ν)
have funProp : mβ ≤ mβ
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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β
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ g z.2) (μ.prod ν)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : β) ↦ g z0
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ g z.2) (μ.prod ν)
have funProp₂ : Measure.map (fun (z : α × β) ↦ z.2) (μ.prod ν) ≪ ν
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 ν
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)
have funProp : m0 ≤ m0
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (z0 : α) ↦ f z0
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)
have funProp₂ : Measure.map (fun (z : α × β) ↦ z.1) (μ.prod ν) ≪ μ
Tactic: fun_prop (disch := intro _ hs; simp [hs])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
c : ℝ≥0∞
⊢ μ.prod (c • ν) = c • μ.prod ν
have h : ∀ (s : Set (α × β)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.prod (c • ν) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((c • μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.prod (c • ν) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((c • μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (x : α), HMul.hMul (β := ℝ≥0∞) c ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) ∂μ =
  c * ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ
Tactic: simp_rw [Measure.prod_apply hs, Measure.smul_apply, Measure.prod_apply hs, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), HMul.hMul (β := ℝ≥0∞) c ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) ∂μ =
    c * ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ
have h : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
Tactic: rw [lintegral_const_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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∞))
have refine : ∀ (x : α), (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).FiniteAtFilter (nhds x)
Tactic: refine ⟨fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : OpensMeasurableSpace α
inst_2 : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
⊢ (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)).FiniteAtFilter (nhds x)
have 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)
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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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)
have refine : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞) : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨U, hUx, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞) : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : ∫⁻ (a : α) in U, (↑(f a) : ℝ≥0∞) ∂μ < ∞
Tactic: rw [withDensity_apply _ hUo.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
M : Type u_2
inst : Monoid M
inst_1 : MeasurableSpace M
μ ν : Measure M
inst_2 : SFinite ν
s : ℝ≥0∞
⊢ 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 ν))
have 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 ν))
Tactic: rw [Measure.prod_smul_right, Measure.map_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 ν))
⊢ 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 ν))
have 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 ν))
Tactic: rw [Measure.prod_smul_right, Measure.map_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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)
have refine : ∀ (φ : G → ℝ≥0∞) (hφ : Measurable φ),
  ∫⁻ (a : G), φ a ∂μ.withDensity f ∗ₘ μ.withDensity g = ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)
Tactic: refine ext_of_lintegral _ fun φ hφ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : G), φ a ∂μ.withDensity f ∗ₘ μ.withDensity g = ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)
have rw : ∫⁻ (y : G),
    ∫⁻ (x : G),
      HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
        (fun (z : G × G) ↦ φ (z.1 * z.2)) (x, x⁻¹ * y) ∂μ ∂μ =
  ∫⁻ (a : G), ((f ⋆ₘₗ[μ] g) * φ) a ∂μ
Tactic: rw [lintegral_mconv_eq_lintegral_prod hφ, prod_withDensity₀ hf hg,
    lintegral_withDensity_eq_lintegral_mul₀,
    lintegral_withDensity_eq_lintegral_mul₀, lintegral_prod,
    lintegral_congr (fun x ↦ by apply (lintegral_mul_left_eq_self _ x⁻¹).symm),
    lintegral_lintegral_swap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 μ
φ : G → ℝ≥0∞
hφ : Measurable φ
rw :
  ∫⁻ (y : G),
      ∫⁻ (x : G),
        HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
          (fun (z : G × G) ↦ φ (z.1 * z.2)) (x, x⁻¹ * y) ∂μ ∂μ =
    ∫⁻ (a : G), ((f ⋆ₘₗ[μ] g) * φ) a ∂μ
⊢ ∫⁻ (a : G), φ a ∂μ.withDensity f ∗ₘ μ.withDensity g = ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)
have hf₁ : AEMeasurable (β := ℝ≥0∞)
  (Function.uncurry fun (a x : G) ↦
    HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
      (fun (z : G × G) ↦ φ (z.1 * z.2)) (a, a⁻¹ * x))
  (μ.prod μ)
Tactic: rw [lintegral_mconv_eq_lintegral_prod hφ, prod_withDensity₀ hf hg,
    lintegral_withDensity_eq_lintegral_mul₀,
    lintegral_withDensity_eq_lintegral_mul₀, lintegral_prod,
    lintegral_congr (fun x ↦ by apply (lintegral_mul_left_eq_self _ x⁻¹).symm),
    lintegral_lintegral_swap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 μ
φ : G → ℝ≥0∞
hφ : Measurable φ
rw :
  ∫⁻ (y : G),
      ∫⁻ (x : G),
        HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
          (fun (z : G × G) ↦ φ (z.1 * z.2)) (x, x⁻¹ * y) ∂μ ∂μ =
    ∫⁻ (a : G), ((f ⋆ₘₗ[μ] g) * φ) a ∂μ
hf₁ :
  AEMeasurable (β := ℝ≥0∞)
    (Function.uncurry fun (a x : G) ↦
      HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
        (fun (z : G × G) ↦ φ (z.1 * z.2)) (a, a⁻¹ * x))
    (μ.prod μ)
⊢ ∫⁻ (a : G), φ a ∂μ.withDensity f ∗ₘ μ.withDensity g = ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)
have hf₂ : AEMeasurable (HMul.hMul (α := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) fun (z : G × G) ↦ φ (z.1 * z.2))
  (μ.prod μ)
Tactic: rw [lintegral_mconv_eq_lintegral_prod hφ, prod_withDensity₀ hf hg,
    lintegral_withDensity_eq_lintegral_mul₀,
    lintegral_withDensity_eq_lintegral_mul₀, lintegral_prod,
    lintegral_congr (fun x ↦ by apply (lintegral_mul_left_eq_self _ x⁻¹).symm),
    lintegral_lintegral_swap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 μ
φ : G → ℝ≥0∞
hφ : Measurable φ
rw :
  ∫⁻ (y : G),
      ∫⁻ (x : G),
        HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
          (fun (z : G × G) ↦ φ (z.1 * z.2)) (x, x⁻¹ * y) ∂μ ∂μ =
    ∫⁻ (a : G), ((f ⋆ₘₗ[μ] g) * φ) a ∂μ
hf₁ :
  AEMeasurable (β := ℝ≥0∞)
    (Function.uncurry fun (a x : G) ↦
      HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
        (fun (z : G × G) ↦ φ (z.1 * z.2)) (a, a⁻¹ * x))
    (μ.prod μ)
hf₂ :
  AEMeasurable (HMul.hMul (α := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) fun (z : G × G) ↦ φ (z.1 * z.2))
    (μ.prod μ)
⊢ ∫⁻ (a : G), φ a ∂μ.withDensity f ∗ₘ μ.withDensity g = ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)
have hf₃ : AEMeasurable (f ⋆ₘₗ[μ] g) μ
Tactic: rw [lintegral_mconv_eq_lintegral_prod hφ, prod_withDensity₀ hf hg,
    lintegral_withDensity_eq_lintegral_mul₀,
    lintegral_withDensity_eq_lintegral_mul₀, lintegral_prod,
    lintegral_congr (fun x ↦ by apply (lintegral_mul_left_eq_self _ x⁻¹).symm),
    lintegral_lintegral_swap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 μ
φ : G → ℝ≥0∞
hφ : Measurable φ
rw :
  ∫⁻ (y : G),
      ∫⁻ (x : G),
        HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
          (fun (z : G × G) ↦ φ (z.1 * z.2)) (x, x⁻¹ * y) ∂μ ∂μ =
    ∫⁻ (a : G), ((f ⋆ₘₗ[μ] g) * φ) a ∂μ
hf₁ :
  AEMeasurable (β := ℝ≥0∞)
    (Function.uncurry fun (a x : G) ↦
      HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
        (fun (z : G × G) ↦ φ (z.1 * z.2)) (a, a⁻¹ * x))
    (μ.prod μ)
hf₂ :
  AEMeasurable (HMul.hMul (α := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) fun (z : G × G) ↦ φ (z.1 * z.2))
    (μ.prod μ)
hf₃ : AEMeasurable (f ⋆ₘₗ[μ] g) μ
⊢ ∫⁻ (a : G), φ a ∂μ.withDensity f ∗ₘ μ.withDensity g = ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)
have hg₁ : AEMeasurable φ μ
Tactic: rw [lintegral_mconv_eq_lintegral_prod hφ, prod_withDensity₀ hf hg,
    lintegral_withDensity_eq_lintegral_mul₀,
    lintegral_withDensity_eq_lintegral_mul₀, lintegral_prod,
    lintegral_congr (fun x ↦ by apply (lintegral_mul_left_eq_self _ x⁻¹).symm),
    lintegral_lintegral_swap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 μ
φ : G → ℝ≥0∞
hφ : Measurable φ
rw :
  ∫⁻ (y : G),
      ∫⁻ (x : G),
        HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
          (fun (z : G × G) ↦ φ (z.1 * z.2)) (x, x⁻¹ * y) ∂μ ∂μ =
    ∫⁻ (a : G), ((f ⋆ₘₗ[μ] g) * φ) a ∂μ
hf₁ :
  AEMeasurable (β := ℝ≥0∞)
    (Function.uncurry fun (a x : G) ↦
      HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
        (fun (z : G × G) ↦ φ (z.1 * z.2)) (a, a⁻¹ * x))
    (μ.prod μ)
hf₂ :
  AEMeasurable (HMul.hMul (α := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) fun (z : G × G) ↦ φ (z.1 * z.2))
    (μ.prod μ)
hf₃ : AEMeasurable (f ⋆ₘₗ[μ] g) μ
hg₁ : AEMeasurable φ μ
⊢ ∫⁻ (a : G), φ a ∂μ.withDensity f ∗ₘ μ.withDensity g = ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)
have hf₄ : AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) (μ.prod μ)
Tactic: rw [lintegral_mconv_eq_lintegral_prod hφ, prod_withDensity₀ hf hg,
    lintegral_withDensity_eq_lintegral_mul₀,
    lintegral_withDensity_eq_lintegral_mul₀, lintegral_prod,
    lintegral_congr (fun x ↦ by apply (lintegral_mul_left_eq_self _ x⁻¹).symm),
    lintegral_lintegral_swap]