Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (x : G), ∫⁻ (y : G), ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (x, y) ∂μ ∂μ =
    ∫⁻ (a : G), ((f ⋆ₘₗ[μ] g) * φ) a ∂μ

pp: case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (μ.prod μ)

pp: case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (f ⋆ₘₗ[μ] g) μ

pp: case hg
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable φ μ

pp: case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ f z.1 * g z.2) (μ.prod μ)

pp: case hg
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ φ (z.1 * z.2)) (μ.prod μ)

Tactic:
lintegral_congr (fun x ↦ by apply (lintegral_mul_left_eq_self _ x⁻¹).symm),

Goal state after:
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : G), ∫⁻ (x : G), ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (a, a⁻¹ * x) ∂μ ∂μ =
    ∫⁻ (a : G), ((f ⋆ₘₗ[μ] g) * φ) a ∂μ

case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (μ.prod μ)

case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (f ⋆ₘₗ[μ] g) μ

case hg
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable φ μ

case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ f z.1 * g z.2) (μ.prod μ)

case hg
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ φ (z.1 * z.2)) (μ.prod μ)