G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (x : G), ∫⁻ (y : G), indicator s (fun x => 1) (y * x) * f x⁻¹ ∂ν ∂μ) =
    ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ

case hf
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (uncurry fun x y => indicator s (fun x => 1) x * f y)
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ (↑↑μ s * ∫⁻ (y : G), f y ∂ν) = ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
rw [← set_lintegral_one, ← lintegral_indicator _ sm,
  ← lintegral_lintegral_mul (measurable_const.indicator sm).aemeasurable hf.aemeasurable,
  ← lintegral_lintegral_mul_inv μ ν]
case hf
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (uncurry fun x y => indicator s (fun x => 1) x * f y)

G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (x : G), ∫⁻ (y : G), indicator s (fun x => 1) (y * x) * f x⁻¹ ∂ν ∂μ) =
    ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (x : G), ∫⁻ (y : G), indicator s (fun x => 1) (y * x) * f x⁻¹ ∂ν ∂μ) =
    ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ

case hf
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (uncurry fun x y => indicator s (fun x => 1) x * f y)
swap
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
⊢ (∫⁻ (x : G), ∫⁻ (y : G), indicator s (fun x => 1) (y * x) * f x⁻¹ ∂ν ∂μ) =
    ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (x : G), ∫⁻ (y : G), indicator s (fun x => 1) (y * x) * f x⁻¹ ∂ν ∂μ) =
    ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
have ms :
  ∀ x : G, Measurable fun y => ((fun z => z * x) ⁻¹' s).indicator (fun _ => (1 : ℝ≥0∞)) y :=
  fun x => measurable_const.indicator (measurable_mul_const _ sm)
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
this : ∀ (x y : G), indicator s (fun x => 1) (y * x) = indicator ((fun z => z * x) ⁻¹' s) (fun b => 1) y
⊢ (∫⁻ (x : G), ∫⁻ (y : G), indicator s (fun x => 1) (y * x) * f x⁻¹ ∂ν ∂μ) =
    ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
⊢ (∫⁻ (x : G), ∫⁻ (y : G), indicator s (fun x => 1) (y * x) * f x⁻¹ ∂ν ∂μ) =
    ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
have : ∀ x y, s.indicator (fun _ : G => (1 : ℝ≥0∞)) (y * x) =
    ((fun z => z * x) ⁻¹' s).indicator (fun b : G => 1) y := by
  intro x y; symm; convert indicator_comp_right (M := ℝ≥0∞) fun y => y * x using 2; ext1; rfl
no goals
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
this : ∀ (x y : G), indicator s (fun x => 1) (y * x) = indicator ((fun z => z * x) ⁻¹' s) (fun b => 1) y
⊢ (∫⁻ (x : G), ∫⁻ (y : G), indicator s (fun x => 1) (y * x) * f x⁻¹ ∂ν ∂μ) =
    ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
simp_rw [this, lintegral_mul_const _ (ms _), lintegral_indicator _ (measurable_mul_const _ sm),
  set_lintegral_one]
no goals
case hf
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (uncurry fun x y => indicator s (fun x => 1) x * f y)
exact (((measurable_const.indicator sm).comp measurable_fst).mul
  (hf.comp measurable_snd)).aemeasurable
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
x y : G
⊢ indicator s (fun x => 1) (y * x) = indicator ((fun z => z * x) ⁻¹' s) (fun b => 1) y
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
⊢ ∀ (x y : G), indicator s (fun x => 1) (y * x) = indicator ((fun z => z * x) ⁻¹' s) (fun b => 1) y
intro x y
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
x y : G
⊢ indicator ((fun z => z * x) ⁻¹' s) (fun b => 1) y = indicator s (fun x => 1) (y * x)
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
x y : G
⊢ indicator s (fun x => 1) (y * x) = indicator ((fun z => z * x) ⁻¹' s) (fun b => 1) y
symm
case h.e'_2.h.e'_5
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
x y : G
⊢ (fun b => 1) = (fun x => 1) ∘ fun y => y * x
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
x y : G
⊢ indicator ((fun z => z * x) ⁻¹' s) (fun b => 1) y = indicator s (fun x => 1) (y * x)
convert indicator_comp_right (M := ℝ≥0∞) fun y => y * x using 2
case h.e'_2.h.e'_5.h
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
x y x✝ : G
⊢ 1 = ((fun x => 1) ∘ fun y => y * x) x✝
case h.e'_2.h.e'_5
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
x y : G
⊢ (fun b => 1) = (fun x => 1) ∘ fun y => y * x
ext1
no goals
case h.e'_2.h.e'_5.h
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y => indicator ((fun z => z * x) ⁻¹' s) (fun x => 1) y
x y x✝ : G
⊢ 1 = ((fun x => 1) ∘ fun y => y * x) x✝
rfl