[GOAL]
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
⊢ Measurable fun x => ↑↑μ ((fun y => y * x) ⁻¹' s)
[PROOFSTEP]
suffices Measurable fun y => μ ((fun x => (x, y)) ⁻¹' ((fun z : G × G => ((1 : G), z.1 * z.2)) ⁻¹' univ ×ˢ s)) by
  convert this using 1; ext1 x; congr 1 with y : 1; simp
[GOAL]
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
⊢ Measurable fun x => ↑↑μ ((fun y => y * x) ⁻¹' s)
[PROOFSTEP]
convert this using 1
[GOAL]
case 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
hs : MeasurableSet s
this : Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
⊢ (fun x => ↑↑μ ((fun y => y * x) ⁻¹' s)) = fun y =>
    ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
[PROOFSTEP]
ext1 x
[GOAL]
case 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
hs : MeasurableSet s
this : Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
x : G
⊢ ↑↑μ ((fun y => y * x) ⁻¹' s) = ↑↑μ ((fun x_1 => (x_1, x)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
[PROOFSTEP]
congr 1 with y : 1
[GOAL]
case h.e'_5.h.e_a.h
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
this : Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
x y : G
⊢ y ∈ (fun y => y * x) ⁻¹' s ↔ y ∈ (fun x_1 => (x_1, x)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s)
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
⊢ Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s))
[PROOFSTEP]
apply measurable_measure_prod_mk_right
[GOAL]
case hs
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
⊢ MeasurableSet ((fun z => (1, z.fst * z.snd)) ⁻¹' univ ×ˢ s)
[PROOFSTEP]
apply measurable_const.prod_mk measurable_mul (MeasurableSet.univ.prod hs)
[GOAL]
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : Group G
inst✝² : MeasurableMul₂ G
μ ν : Measure G
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set G
hs : MeasurableSet s
⊢ MeasurableSpace G
[PROOFSTEP]
infer_instance
[GOAL]
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 ν
⊢ MeasurePreserving fun z => (z.snd * z.fst, z.fst⁻¹)
[PROOFSTEP]
convert (measurePreserving_prod_inv_mul_swap ν μ).comp (measurePreserving_prod_mul_swap μ ν) using 1
[GOAL]
case 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 ν
⊢ (fun z => (z.snd * z.fst, z.fst⁻¹)) = (fun z => (z.snd, z.snd⁻¹ * z.fst)) ∘ fun z => (z.snd, z.snd * z.fst)
[PROOFSTEP]
ext1 ⟨x, y⟩
[GOAL]
case h.e'_5.h.mk
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 ν
x y : G
⊢ ((x, y).snd * (x, y).fst, (x, y).fst⁻¹) =
    ((fun z => (z.snd, z.snd⁻¹ * z.fst)) ∘ fun z => (z.snd, z.snd * z.fst)) (x, y)
[PROOFSTEP]
simp_rw [Function.comp_apply, mul_inv_rev, inv_mul_cancel_right]
[GOAL]
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 μ
⊢ QuasiMeasurePreserving Inv.inv
[PROOFSTEP]
refine' ⟨measurable_inv, AbsolutelyContinuous.mk fun s hsm hμs => _⟩
[GOAL]
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 μ
s : Set G
hsm : MeasurableSet s
hμs : ↑↑μ s = 0
⊢ ↑↑(map Inv.inv μ) s = 0
[PROOFSTEP]
rw [map_apply measurable_inv hsm, inv_preimage]
[GOAL]
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 μ
s : Set G
hsm : MeasurableSet s
hμs : ↑↑μ s = 0
⊢ ↑↑μ s⁻¹ = 0
[PROOFSTEP]
have hf : Measurable fun z : G × G => (z.2 * z.1, z.1⁻¹) :=
  (measurable_snd.mul measurable_fst).prod_mk measurable_fst.inv
[GOAL]
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 μ
s : Set G
hsm : MeasurableSet s
hμs : ↑↑μ s = 0
hf : Measurable fun z => (z.snd * z.fst, z.fst⁻¹)
⊢ ↑↑μ s⁻¹ = 0
[PROOFSTEP]
suffices map (fun z : G × G => (z.2 * z.1, z.1⁻¹)) (μ.prod μ) (s⁻¹ ×ˢ s⁻¹) = 0 by
  simpa only [(measurePreserving_mul_prod_inv μ μ).map_eq, prod_prod, mul_eq_zero (M₀ := ℝ≥0∞), or_self_iff] using this
[GOAL]
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 μ
s : Set G
hsm : MeasurableSet s
hμs : ↑↑μ s = 0
hf : Measurable fun z => (z.snd * z.fst, z.fst⁻¹)
this : ↑↑(map (fun z => (z.snd * z.fst, z.fst⁻¹)) (Measure.prod μ μ)) (s⁻¹ ×ˢ s⁻¹) = 0
⊢ ↑↑μ s⁻¹ = 0
[PROOFSTEP]
simpa only [(measurePreserving_mul_prod_inv μ μ).map_eq, prod_prod, mul_eq_zero (M₀ := ℝ≥0∞), or_self_iff] using this
[GOAL]
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 μ
s : Set G
hsm : MeasurableSet s
hμs : ↑↑μ s = 0
hf : Measurable fun z => (z.snd * z.fst, z.fst⁻¹)
⊢ ↑↑(map (fun z => (z.snd * z.fst, z.fst⁻¹)) (Measure.prod μ μ)) (s⁻¹ ×ˢ s⁻¹) = 0
[PROOFSTEP]
have hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹) := hsm.inv.prod hsm.inv
[GOAL]
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 μ
s : Set G
hsm : MeasurableSet s
hμs : ↑↑μ s = 0
hf : Measurable fun z => (z.snd * z.fst, z.fst⁻¹)
hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹)
⊢ ↑↑(map (fun z => (z.snd * z.fst, z.fst⁻¹)) (Measure.prod μ μ)) (s⁻¹ ×ˢ s⁻¹) = 0
[PROOFSTEP]
simp_rw [map_apply hf hsm', prod_apply_symm (μ := μ) (ν := μ) (hf hsm'), preimage_preimage, mk_preimage_prod,
  inv_preimage, inv_inv, measure_mono_null (inter_subset_right _ _) hμs, lintegral_zero]
[GOAL]
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 μ
⊢ ↑↑μ s⁻¹ = 0 ↔ ↑↑μ s = 0
[PROOFSTEP]
refine' ⟨fun hs => _, (quasiMeasurePreserving_inv μ).preimage_null⟩
[GOAL]
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 μ
hs : ↑↑μ s⁻¹ = 0
⊢ ↑↑μ s = 0
[PROOFSTEP]
rw [← inv_inv s]
[GOAL]
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 μ
hs : ↑↑μ s⁻¹ = 0
⊢ ↑↑μ s⁻¹⁻¹ = 0
[PROOFSTEP]
exact (quasiMeasurePreserving_inv μ).preimage_null hs
[GOAL]
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 μ
⊢ μ ≪ Measure.inv μ
[PROOFSTEP]
refine' AbsolutelyContinuous.mk fun s _ => _
[GOAL]
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 μ
s : Set G
x✝ : MeasurableSet s
⊢ ↑↑(Measure.inv μ) s = 0 → ↑↑μ s = 0
[PROOFSTEP]
simp_rw [inv_apply μ s, measure_inv_null, imp_self]
[GOAL]
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 ν
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f)
⊢ ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
[PROOFSTEP]
have h : Measurable fun z : G × G => (z.2 * z.1, z.1⁻¹) :=
  (measurable_snd.mul measurable_fst).prod_mk measurable_fst.inv
[GOAL]
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 ν
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f)
h : Measurable fun z => (z.snd * z.fst, z.fst⁻¹)
⊢ ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
[PROOFSTEP]
have h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹) (μ.prod ν) :=
  hf.comp_quasiMeasurePreserving (measurePreserving_mul_prod_inv μ ν).quasiMeasurePreserving
[GOAL]
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 ν
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f)
h : Measurable fun z => (z.snd * z.fst, z.fst⁻¹)
h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹)
⊢ ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
[PROOFSTEP]
simp_rw [lintegral_lintegral h2f, lintegral_lintegral hf]
[GOAL]
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 ν
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f)
h : Measurable fun z => (z.snd * z.fst, z.fst⁻¹)
h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹)
⊢ ∫⁻ (z : G × G), f (z.snd * z.fst) z.fst⁻¹ ∂Measure.prod μ ν = ∫⁻ (z : G × G), f z.fst z.snd ∂Measure.prod μ ν
[PROOFSTEP]
conv_rhs => rw [← (measurePreserving_mul_prod_inv μ ν).map_eq]
[GOAL]
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 ν
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f)
h : Measurable fun z => (z.snd * z.fst, z.fst⁻¹)
h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹)
| ∫⁻ (z : G × G), f z.fst z.snd ∂Measure.prod μ ν
[PROOFSTEP]
rw [← (measurePreserving_mul_prod_inv μ ν).map_eq]
[GOAL]
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 ν
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f)
h : Measurable fun z => (z.snd * z.fst, z.fst⁻¹)
h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹)
| ∫⁻ (z : G × G), f z.fst z.snd ∂Measure.prod μ ν
[PROOFSTEP]
rw [← (measurePreserving_mul_prod_inv μ ν).map_eq]
[GOAL]
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 ν
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f)
h : Measurable fun z => (z.snd * z.fst, z.fst⁻¹)
h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹)
| ∫⁻ (z : G × G), f z.fst z.snd ∂Measure.prod μ ν
[PROOFSTEP]
rw [← (measurePreserving_mul_prod_inv μ ν).map_eq]
[GOAL]
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 ν
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f)
h : Measurable fun z => (z.snd * z.fst, z.fst⁻¹)
h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹)
⊢ ∫⁻ (z : G × G), f (z.snd * z.fst) z.fst⁻¹ ∂Measure.prod μ ν =
    ∫⁻ (z : G × G), f z.fst z.snd ∂map (fun z => (z.snd * z.fst, z.fst⁻¹)) (Measure.prod μ ν)
[PROOFSTEP]
symm
[GOAL]
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 ν
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f)
h : Measurable fun z => (z.snd * z.fst, z.fst⁻¹)
h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹)
⊢ ∫⁻ (z : G × G), f z.fst z.snd ∂map (fun z => (z.snd * z.fst, z.fst⁻¹)) (Measure.prod μ ν) =
    ∫⁻ (z : G × G), f (z.snd * z.fst) z.fst⁻¹ ∂Measure.prod μ ν
[PROOFSTEP]
exact lintegral_map' (hf.mono' (measurePreserving_mul_prod_inv μ ν).map_eq.absolutelyContinuous) h.aemeasurable
[GOAL]
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 μ
y : G
⊢ ↑↑μ ((fun x => x * y) ⁻¹' s) = 0 ↔ ↑↑μ ((fun x => y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ = 0
[PROOFSTEP]
simp_rw [← inv_preimage, preimage_preimage, mul_inv_rev, inv_inv]
[GOAL]
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 μ
y : G
⊢ ↑↑μ ((fun x => y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ = 0 ↔ ↑↑μ s = 0
[PROOFSTEP]
simp only [measure_inv_null μ, measure_preimage_mul]
[GOAL]
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 μ
g : G
⊢ μ ≪ map (fun x => x * g) μ
[PROOFSTEP]
refine' AbsolutelyContinuous.mk fun s hs => _
[GOAL]
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 μ
g : G
s : Set G
hs : MeasurableSet s
⊢ ↑↑(map (fun x => x * g) μ) s = 0 → ↑↑μ s = 0
[PROOFSTEP]
rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null]
[GOAL]
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 μ
g : G
s : Set G
hs : MeasurableSet s
⊢ ↑↑μ s = 0 → ↑↑μ s = 0
[PROOFSTEP]
exact id
[GOAL]
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 μ
g : G
⊢ μ ≪ map (fun h => g / h) μ
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
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 μ
g : G
⊢ μ ≪ map (fun h => g * h⁻¹) μ
[PROOFSTEP]
erw [← map_map (measurable_const_mul g) measurable_inv]
[GOAL]
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 μ
g : G
⊢ μ ≪ map (fun x => g * x) (map Inv.inv μ)
[PROOFSTEP]
conv_lhs => rw [← map_mul_left_eq_self μ g]
[GOAL]
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 μ
g : G
| μ
[PROOFSTEP]
rw [← map_mul_left_eq_self μ g]
[GOAL]
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 μ
g : G
| μ
[PROOFSTEP]
rw [← map_mul_left_eq_self μ g]
[GOAL]
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 μ
g : G
| μ
[PROOFSTEP]
rw [← map_mul_left_eq_self μ g]
[GOAL]
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 μ
g : G
⊢ map (fun x => g * x) μ ≪ map (fun x => g * x) (map Inv.inv μ)
[PROOFSTEP]
exact (absolutelyContinuous_inv μ).map (measurable_const_mul g)
[GOAL]
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⁻¹ ∂μ
[PROOFSTEP]
rw [← set_lintegral_one, ← lintegral_indicator _ sm, ←
  lintegral_lintegral_mul (measurable_const.indicator sm).aemeasurable hf.aemeasurable, ←
  lintegral_lintegral_mul_inv μ ν]
[GOAL]
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)
[PROOFSTEP]
swap
[GOAL]
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)
[PROOFSTEP]
exact (((measurable_const.indicator sm).comp measurable_fst).mul (hf.comp measurable_snd)).aemeasurable
[GOAL]
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⁻¹ ∂μ
[PROOFSTEP]
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)
[GOAL]
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⁻¹ ∂μ
[PROOFSTEP]
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
[GOAL]
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
[PROOFSTEP]
intro x y
[GOAL]
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
[PROOFSTEP]
symm
[GOAL]
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)
[PROOFSTEP]
convert indicator_comp_right (M := ℝ≥0∞) fun y => y * x using 2
[GOAL]
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
[PROOFSTEP]
ext1
[GOAL]
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✝
[PROOFSTEP]
rfl
[GOAL]
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⁻¹ ∂μ
[PROOFSTEP]
simp_rw [this, lintegral_mul_const _ (ms _), lintegral_indicator _ (measurable_mul_const _ sm), set_lintegral_one]
[GOAL]
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 ν
hν : ν ≠ 0
⊢ μ ≪ ν
[PROOFSTEP]
refine' AbsolutelyContinuous.mk fun s sm hνs => _
[GOAL]
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 ν
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ↑↑ν s = 0
⊢ ↑↑μ s = 0
[PROOFSTEP]
have h1 := measure_mul_lintegral_eq μ ν sm 1 measurable_one
[GOAL]
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 ν
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ↑↑ν s = 0
h1 : ↑↑μ s * ∫⁻ (y : G), OfNat.ofNat 1 y ∂ν = ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * OfNat.ofNat 1 x⁻¹ ∂μ
⊢ ↑↑μ s = 0
[PROOFSTEP]
simp_rw [Pi.one_apply, lintegral_one, mul_one, (measure_mul_right_null ν _).mpr hνs, lintegral_zero,
  mul_eq_zero (M₀ := ℝ≥0∞), measure_univ_eq_zero.not.mpr hν, or_false_iff] at h1
[GOAL]
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 ν
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ↑↑ν s = 0
h1 : ↑↑μ s = 0
⊢ ↑↑μ s = 0
[PROOFSTEP]
exact h1
[GOAL]
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
hμs : ↑↑μ s ≠ ⊤
⊢ ∀ᵐ (x : G) ∂μ, ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
[PROOFSTEP]
refine' ae_of_forall_measure_lt_top_ae_restrict' ν.inv _ _
[GOAL]
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
hμs : ↑↑μ s ≠ ⊤
⊢ ∀ (s_1 : Set G),
    MeasurableSet s_1 →
      ↑↑μ s_1 < ⊤ → ↑↑(Measure.inv ν) s_1 < ⊤ → ∀ᵐ (x : G) ∂Measure.restrict μ s_1, ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
[PROOFSTEP]
intro A hA _ h3A
[GOAL]
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
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑(Measure.inv ν) A < ⊤
⊢ ∀ᵐ (x : G) ∂Measure.restrict μ A, ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
[PROOFSTEP]
simp only [ν.inv_apply] at h3A
[GOAL]
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
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
⊢ ∀ᵐ (x : G) ∂Measure.restrict μ A, ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
[PROOFSTEP]
apply ae_lt_top (measurable_measure_mul_right ν sm)
[GOAL]
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
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
⊢ ∫⁻ (x : G) in A, ↑↑ν ((fun y => y * x) ⁻¹' s) ∂μ ≠ ⊤
[PROOFSTEP]
have h1 := measure_mul_lintegral_eq μ ν sm (A⁻¹.indicator 1) (measurable_one.indicator hA.inv)
[GOAL]
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
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
h1 : ↑↑μ s * ∫⁻ (y : G), indicator A⁻¹ 1 y ∂ν = ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * indicator A⁻¹ 1 x⁻¹ ∂μ
⊢ ∫⁻ (x : G) in A, ↑↑ν ((fun y => y * x) ⁻¹' s) ∂μ ≠ ⊤
[PROOFSTEP]
rw [lintegral_indicator _ hA.inv] at h1
[GOAL]
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
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
h1 : ↑↑μ s * ∫⁻ (a : G) in A⁻¹, OfNat.ofNat 1 a ∂ν = ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * indicator A⁻¹ 1 x⁻¹ ∂μ
⊢ ∫⁻ (x : G) in A, ↑↑ν ((fun y => y * x) ⁻¹' s) ∂μ ≠ ⊤
[PROOFSTEP]
simp_rw [Pi.one_apply, set_lintegral_one, ← image_inv, indicator_image inv_injective, image_inv, ←
  indicator_mul_right _ fun x => ν ((fun y => y * x) ⁻¹' s), Function.comp, Pi.one_apply, mul_one] at h1
[GOAL]
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
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
h1 : ↑↑μ s * ↑↑ν A⁻¹ = ∫⁻ (x : G), indicator A (fun a => ↑↑ν ((fun y => y * a) ⁻¹' s)) x ∂μ
⊢ ∫⁻ (x : G) in A, ↑↑ν ((fun y => y * x) ⁻¹' s) ∂μ ≠ ⊤
[PROOFSTEP]
rw [← lintegral_indicator _ hA, ← h1]
[GOAL]
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
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
h1 : ↑↑μ s * ↑↑ν A⁻¹ = ∫⁻ (x : G), indicator A (fun a => ↑↑ν ((fun y => y * a) ⁻¹' s)) x ∂μ
⊢ ↑↑μ s * ↑↑ν A⁻¹ ≠ ⊤
[PROOFSTEP]
exact ENNReal.mul_ne_top hμs h3A.ne
[GOAL]
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
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
⊢ ∀ᵐ (x : G) ∂μ, ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
[PROOFSTEP]
refine' (ae_measure_preimage_mul_right_lt_top ν ν sm h3s).filter_mono _
[GOAL]
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
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
⊢ ae μ ≤ ae ν
[PROOFSTEP]
refine' (absolutelyContinuous_of_isMulLeftInvariant μ ν _).ae_le
[GOAL]
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
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
⊢ ν ≠ 0
[PROOFSTEP]
refine' mt _ h2s
[GOAL]
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
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
⊢ ν = 0 → ↑↑ν s = 0
[PROOFSTEP]
intro hν
[GOAL]
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
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
hν : ν = 0
⊢ ↑↑ν s = 0
[PROOFSTEP]
rw [hν, Measure.coe_zero, Pi.zero_apply]
[GOAL]
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
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
⊢ ↑↑μ s * ∫⁻ (y : G), f y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν = ∫⁻ (x : G), f x ∂μ
[PROOFSTEP]
set g := fun y => f y⁻¹ / ν ((fun x => x * y⁻¹) ⁻¹' s)
[GOAL]
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
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s)
⊢ ↑↑μ s * lintegral ν g = ∫⁻ (x : G), f x ∂μ
[PROOFSTEP]
have hg : Measurable g := (hf.comp measurable_inv).div ((measurable_measure_mul_right ν sm).comp measurable_inv)
[GOAL]
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
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ ↑↑μ s * lintegral ν g = ∫⁻ (x : G), f x ∂μ
[PROOFSTEP]
simp_rw [measure_mul_lintegral_eq μ ν sm g hg, inv_inv]
[GOAL]
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
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * (f x / ↑↑ν ((fun z => z * x) ⁻¹' s)) ∂μ = ∫⁻ (x : G), f x ∂μ
[PROOFSTEP]
refine' lintegral_congr_ae _
[GOAL]
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
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ (fun x => ↑↑ν ((fun z => z * x) ⁻¹' s) * (f x / ↑↑ν ((fun z => z * x) ⁻¹' s))) =ᶠ[ae μ] fun x => f x
[PROOFSTEP]
refine' (ae_measure_preimage_mul_right_lt_top_of_ne_zero μ ν sm h2s h3s).mono fun x hx => _
[GOAL]
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
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s)
hg : Measurable g
x : G
hx : ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
⊢ (fun x => ↑↑ν ((fun z => z * x) ⁻¹' s) * (f x / ↑↑ν ((fun z => z * x) ⁻¹' s))) x = (fun x => f x) x
[PROOFSTEP]
simp_rw [ENNReal.mul_div_cancel' (measure_mul_right_ne_zero ν h2s _) hx.ne]
[GOAL]
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 ν
s t : Set G
hs : MeasurableSet s
ht : MeasurableSet t
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
⊢ ↑↑μ s * ↑↑ν t = ↑↑ν s * ↑↑μ t
[PROOFSTEP]
have h1 := measure_lintegral_div_measure ν ν hs h2s h3s (t.indicator fun _ => 1) (measurable_const.indicator ht)
[GOAL]
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 ν
s t : Set G
hs : MeasurableSet s
ht : MeasurableSet t
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
h1 :
  ↑↑ν s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν =
    ∫⁻ (x : G), indicator t (fun x => 1) x ∂ν
⊢ ↑↑μ s * ↑↑ν t = ↑↑ν s * ↑↑μ t
[PROOFSTEP]
have h2 := measure_lintegral_div_measure μ ν hs h2s h3s (t.indicator fun _ => 1) (measurable_const.indicator ht)
[GOAL]
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 ν
s t : Set G
hs : MeasurableSet s
ht : MeasurableSet t
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
h1 :
  ↑↑ν s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν =
    ∫⁻ (x : G), indicator t (fun x => 1) x ∂ν
h2 :
  ↑↑μ s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν =
    ∫⁻ (x : G), indicator t (fun x => 1) x ∂μ
⊢ ↑↑μ s * ↑↑ν t = ↑↑ν s * ↑↑μ t
[PROOFSTEP]
rw [lintegral_indicator _ ht, set_lintegral_one] at h1 h2
[GOAL]
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 ν
s t : Set G
hs : MeasurableSet s
ht : MeasurableSet t
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
h1 : ↑↑ν s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν = ↑↑ν t
h2 : ↑↑μ s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν = ↑↑μ t
⊢ ↑↑μ s * ↑↑ν t = ↑↑ν s * ↑↑μ t
[PROOFSTEP]
rw [← h1, mul_left_comm, h2]
[GOAL]
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 ν
hs : MeasurableSet s
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
⊢ μ = (↑↑μ s / ↑↑ν s) • ν
[PROOFSTEP]
ext1 t ht
[GOAL]
case 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 ν
hs : MeasurableSet s
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
t : Set G
ht : MeasurableSet t
⊢ ↑↑μ t = ↑↑((↑↑μ s / ↑↑ν s) • ν) t
[PROOFSTEP]
rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm, measure_mul_measure_eq μ ν hs ht h2s h3s,
  mul_div_assoc, ENNReal.mul_div_cancel' h2s h3s]
[GOAL]
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ ν : Measure G
inst✝² : SigmaFinite ν
inst✝¹ : SigmaFinite μ
s : Set G
inst✝ : IsMulRightInvariant μ
⊢ MeasurePreserving ?m.111352
[PROOFSTEP]
apply measurePreserving_prod_mul_swap_right μ ν
[GOAL]
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✝ : IsMulRightInvariant μ
⊢ MeasurePreserving ?m.118254
[PROOFSTEP]
apply measurePreserving_prod_div_swap μ ν
[GOAL]
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✝¹ : IsMulRightInvariant μ
inst✝ : IsMulRightInvariant ν
⊢ MeasurePreserving fun z => (z.fst * z.snd, z.fst⁻¹)
[PROOFSTEP]
convert (measurePreserving_prod_div_swap ν μ).comp (measurePreserving_prod_mul_swap_right μ ν) using 1
[GOAL]
case 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✝¹ : IsMulRightInvariant μ
inst✝ : IsMulRightInvariant ν
⊢ (fun z => (z.fst * z.snd, z.fst⁻¹)) = (fun z => (z.snd, z.fst / z.snd)) ∘ fun z => (z.snd, z.fst * z.snd)
[PROOFSTEP]
ext1 ⟨x, y⟩
[GOAL]
case h.e'_5.h.mk
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✝¹ : IsMulRightInvariant μ
inst✝ : IsMulRightInvariant ν
x y : G
⊢ ((x, y).fst * (x, y).snd, (x, y).fst⁻¹) = ((fun z => (z.snd, z.fst / z.snd)) ∘ fun z => (z.snd, z.fst * z.snd)) (x, y)
[PROOFSTEP]
simp_rw [Function.comp_apply, div_mul_eq_div_div_swap, div_self', one_div]
[GOAL]
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✝ : IsMulRightInvariant μ
⊢ QuasiMeasurePreserving Inv.inv
[PROOFSTEP]
rw [← μ.inv_inv]
[GOAL]
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✝ : IsMulRightInvariant μ
⊢ QuasiMeasurePreserving Inv.inv
[PROOFSTEP]
exact (quasiMeasurePreserving_inv μ.inv).mono (inv_absolutelyContinuous μ.inv) (absolutelyContinuous_inv μ.inv)
[GOAL]
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 μ
g : G
⊢ QuasiMeasurePreserving fun h => g / h
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
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 μ
g : G
⊢ QuasiMeasurePreserving fun h => g * h⁻¹
[PROOFSTEP]
exact (measurePreserving_mul_left μ g).quasiMeasurePreserving.comp (quasiMeasurePreserving_inv μ)
[GOAL]
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✝ : IsMulRightInvariant μ
g : G
⊢ QuasiMeasurePreserving fun h => g / h
[PROOFSTEP]
rw [← μ.inv_inv]
[GOAL]
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✝ : IsMulRightInvariant μ
g : G
⊢ QuasiMeasurePreserving fun h => g / h
[PROOFSTEP]
exact (quasiMeasurePreserving_div_left μ.inv g).mono (inv_absolutelyContinuous μ.inv) (absolutelyContinuous_inv μ.inv)
[GOAL]
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✝ : IsMulRightInvariant μ
⊢ QuasiMeasurePreserving fun p => p.fst / p.snd
[PROOFSTEP]
refine' QuasiMeasurePreserving.prod_of_left measurable_div (eventually_of_forall fun y => _)
[GOAL]
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✝ : IsMulRightInvariant μ
y : G
⊢ QuasiMeasurePreserving fun x => (x, y).fst / (x, y).snd
[PROOFSTEP]
exact (measurePreserving_div_right μ y).quasiMeasurePreserving
[GOAL]
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 μ
g : G
⊢ QuasiMeasurePreserving fun h => h * g
[PROOFSTEP]
refine' ⟨measurable_mul_const g, AbsolutelyContinuous.mk fun s hs => _⟩
[GOAL]
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 μ
g : G
s : Set G
hs : MeasurableSet s
⊢ ↑↑μ s = 0 → ↑↑(map (fun h => h * g) μ) s = 0
[PROOFSTEP]
rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null]
[GOAL]
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 μ
g : G
s : Set G
hs : MeasurableSet s
⊢ ↑↑μ s = 0 → ↑↑μ s = 0
[PROOFSTEP]
exact id
[GOAL]
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✝ : IsMulRightInvariant μ
g : G
⊢ QuasiMeasurePreserving fun h => g * h
[PROOFSTEP]
have :=
  (quasiMeasurePreserving_mul_right μ.inv g⁻¹).mono (inv_absolutelyContinuous μ.inv) (absolutelyContinuous_inv μ.inv)
[GOAL]
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✝ : IsMulRightInvariant μ
g : G
this : QuasiMeasurePreserving fun h => h * g⁻¹
⊢ QuasiMeasurePreserving fun h => g * h
[PROOFSTEP]
rw [μ.inv_inv] at this
[GOAL]
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✝ : IsMulRightInvariant μ
g : G
this : QuasiMeasurePreserving fun h => h * g⁻¹
⊢ QuasiMeasurePreserving fun h => g * h
[PROOFSTEP]
have :=
  (quasiMeasurePreserving_inv_of_right_invariant μ).comp (this.comp (quasiMeasurePreserving_inv_of_right_invariant μ))
[GOAL]
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✝ : IsMulRightInvariant μ
g : G
this✝ : QuasiMeasurePreserving fun h => h * g⁻¹
this : QuasiMeasurePreserving (Inv.inv ∘ (fun h => h * g⁻¹) ∘ Inv.inv)
⊢ QuasiMeasurePreserving fun h => g * h
[PROOFSTEP]
simp_rw [Function.comp, mul_inv_rev, inv_inv] at this
[GOAL]
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✝ : IsMulRightInvariant μ
g : G
this✝ : QuasiMeasurePreserving fun h => h * g⁻¹
this : QuasiMeasurePreserving fun x => g * x
⊢ QuasiMeasurePreserving fun h => g * h
[PROOFSTEP]
exact this


[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : IsInvInvariant μ
⊢ ∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
have h : MeasurableEmbedding fun x : G => x⁻¹ := (MeasurableEquiv.inv G).measurableEmbedding
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : IsInvInvariant μ
h : MeasurableEmbedding fun x => x⁻¹
⊢ ∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
rw [← h.integral_map, map_inv_eq_self]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulLeftInvariant μ
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ
[PROOFSTEP]
convert (lintegral_map_equiv f <| MeasurableEquiv.mulLeft g).symm
[GOAL]
case h.e'_3.h.e'_3
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulLeftInvariant μ
f : G → ℝ≥0∞
g : G
⊢ μ = map (↑(MeasurableEquiv.mulLeft g)) μ
[PROOFSTEP]
simp [map_mul_left_eq_self μ g]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x * g) ∂μ = ∫⁻ (x : G), f x ∂μ
[PROOFSTEP]
convert (lintegral_map_equiv f <| MeasurableEquiv.mulRight g).symm using 1
[GOAL]
case h.e'_3
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f x ∂μ = ∫⁻ (a : G), f a ∂map (↑(MeasurableEquiv.mulRight g)) μ
[PROOFSTEP]
simp [map_mul_right_eq_self μ g]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
  -- Porting note: was `simp_rw`
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x * g⁻¹) ∂μ = ∫⁻ (x : G), f x ∂μ
[PROOFSTEP]
rw [lintegral_mul_right_eq_self f g⁻¹]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulLeftInvariant μ
f : G → E
g : G
⊢ ∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
have h_mul : MeasurableEmbedding fun x => g * x := (MeasurableEquiv.mulLeft g).measurableEmbedding
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulLeftInvariant μ
f : G → E
g : G
h_mul : MeasurableEmbedding fun x => g * x
⊢ ∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
rw [← h_mul.integral_map, map_mul_left_eq_self]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → E
g : G
⊢ ∫ (x : G), f (x * g) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
have h_mul : MeasurableEmbedding fun x => x * g := (MeasurableEquiv.mulRight g).measurableEmbedding
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → E
g : G
h_mul : MeasurableEmbedding fun x => x * g
⊢ ∫ (x : G), f (x * g) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
rw [← h_mul.integral_map, map_mul_right_eq_self]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → E
g : G
⊢ ∫ (x : G), f (x / g) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
  -- Porting note: was `simp_rw`
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → E
g : G
⊢ ∫ (x : G), f (x * g⁻¹) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
rw [integral_mul_right_eq_self f g⁻¹]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulLeftInvariant μ
hf' : ∀ (x : G), f (g * x) = -f x
⊢ ∫ (x : G), f x ∂μ = 0
[PROOFSTEP]
simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_left_eq_self]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
hf' : ∀ (x : G), f (x * g) = -f x
⊢ ∫ (x : G), f x ∂μ = 0
[PROOFSTEP]
simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_right_eq_self]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
f : G → F
inst✝ : IsMulRightInvariant μ
hf : Integrable f
g : G
⊢ Integrable fun t => f (t / g)
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
f : G → F
inst✝ : IsMulRightInvariant μ
hf : Integrable f
g : G
⊢ Integrable fun t => f (t * g⁻¹)
[PROOFSTEP]
exact hf.comp_mul_right g⁻¹
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
⊢ (Integrable fun t => f (g / t)) ↔ Integrable f
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.comp_div_left g⟩
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
h : Integrable fun t => f (g / t)
⊢ Integrable f
[PROOFSTEP]
convert h.comp_inv.comp_mul_left g⁻¹
[GOAL]
case h.e'_5.h.h.e'_1
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
h : Integrable fun t => f (g / t)
x✝ : G
⊢ x✝ = g / (g⁻¹ * x✝)⁻¹
[PROOFSTEP]
simp_rw [div_inv_eq_mul, mul_inv_cancel_left]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
x' : G
⊢ ∫ (x : G), f (x' / x) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
  -- Porting note: was `simp_rw`
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
x' : G
⊢ ∫ (x : G), f (x' * x⁻¹) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
rw [integral_inv_eq_self (fun x => f (x' * x)) μ, integral_mul_left_eq_self f x']
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableSpace α
inst✝² : MulAction G α
inst✝¹ : MeasurableSMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
f : α → E
g : G
⊢ ∫ (x : α), f (g • x) ∂μ = ∫ (x : α), f x ∂μ
[PROOFSTEP]
have h : MeasurableEmbedding fun x : α => g • x := (MeasurableEquiv.smul g).measurableEmbedding
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableSpace α
inst✝² : MulAction G α
inst✝¹ : MeasurableSMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
f : α → E
g : G
h : MeasurableEmbedding fun x => g • x
⊢ ∫ (x : α), f (g • x) ∂μ = ∫ (x : α), f x ∂μ
[PROOFSTEP]
rw [← h.integral_map, map_smul]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g : G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalGroup G
inst✝² : BorelSpace G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
hμ : μ ≠ 0
f : G → ℝ≥0∞
hf : Continuous f
⊢ ∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0
[PROOFSTEP]
haveI := isOpenPosMeasure_of_mulLeftInvariant_of_regular hμ
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g : G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalGroup G
inst✝² : BorelSpace G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
hμ : μ ≠ 0
f : G → ℝ≥0∞
hf : Continuous f
this : IsOpenPosMeasure μ
⊢ ∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0
[PROOFSTEP]
rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]


[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : MeasurableSpace M
inst✝² : SMul M α
inst✝¹ : MeasurableSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
⊢ map (fun x => c • x) μ = μ
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝³ : MeasurableSpace M
inst✝² : SMul M α
inst✝¹ : MeasurableSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑(map (fun x => c • x) μ) s = ↑↑μ s
[PROOFSTEP]
rw [map_apply (measurable_const_smul c) hs]
[GOAL]
case h
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝³ : MeasurableSpace M
inst✝² : SMul M α
inst✝¹ : MeasurableSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ ((fun x x_1 => x • x_1) c ⁻¹' s) = ↑↑μ s
[PROOFSTEP]
exact SMulInvariantMeasure.measure_preimage_smul c hs
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 1 ↔ 2
[GOAL]
case tfae_1_iff_2
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
⊢ SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
[PROOFSTEP]
exact ⟨fun h => h.1, fun h => ⟨h⟩⟩
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 1 → 6
[GOAL]
case tfae_1_to_6
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
⊢ SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
[PROOFSTEP]
intro h c
[GOAL]
case tfae_1_to_6
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c✝ : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
h : SMulInvariantMeasure G α μ
c : G
⊢ map (fun x => c • x) μ = μ
[PROOFSTEP]
exact (measurePreserving_smul c μ).map_eq
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 6 → 7
[GOAL]
case tfae_6_to_7
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
⊢ (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
[PROOFSTEP]
exact fun H c => ⟨measurable_const_smul c, H c⟩
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 7 → 4
[GOAL]
case tfae_7_to_4
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
⊢ (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
[PROOFSTEP]
exact fun H c => (H c).measure_preimage_emb (measurableEmbedding_const_smul c)
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 4 → 5
[GOAL]
case tfae_4_to_5
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
⊢ (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
[PROOFSTEP]
exact fun H c s => by
  rw [← preimage_smul_inv]
  apply H
[GOAL]
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c✝ : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
H : ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
c : G
s : Set α
⊢ ↑↑μ (c • s) = ↑↑μ s
[PROOFSTEP]
rw [← preimage_smul_inv]
[GOAL]
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c✝ : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
H : ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
c : G
s : Set α
⊢ ↑↑μ ((fun x => c⁻¹ • x) ⁻¹' s) = ↑↑μ s
[PROOFSTEP]
apply H
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 5 → 3
[GOAL]
case tfae_5_to_3
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
⊢ (∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
[PROOFSTEP]
exact fun H c s _ => H c s
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
tfae_5_to_3 :
  (∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 3 → 2
[GOAL]
case tfae_3_to_2
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
tfae_5_to_3 :
  (∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
⊢ (∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s) →
    ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
[PROOFSTEP]
intro H c s hs
[GOAL]
case tfae_3_to_2
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c✝ : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
tfae_5_to_3 :
  (∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
H : ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
c : G
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
[PROOFSTEP]
rw [preimage_smul]
[GOAL]
case tfae_3_to_2
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c✝ : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
tfae_5_to_3 :
  (∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
H : ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
c : G
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ (c⁻¹ • s) = ↑↑μ s
[PROOFSTEP]
exact H c⁻¹ s hs
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
tfae_5_to_3 :
  (∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
tfae_3_to_2 :
  (∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s) →
    ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_finish
[GOAL]
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c✝ : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s
c : G
⊢ NullMeasurableSet (c • s)
[PROOFSTEP]
simpa only [← preimage_smul_inv] using hs.preimage (measurePreserving_smul _ _).quasiMeasurePreserving
[GOAL]
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c✝ : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
h : ↑↑μ s = 0
c : G
⊢ ↑↑μ (c • s) = 0
[PROOFSTEP]
rwa [measure_smul]
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
c : G
μ : Measure α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousConstSMul G α
inst✝ : MulAction.IsMinimal G α
K U : Set α
hK : IsCompact K
hμK : ↑↑μ K ≠ 0
hU : IsOpen U
hne : Set.Nonempty U
t : Finset G
ht : K ⊆ ⋃ (g : G) (_ : g ∈ t), g • U
hμU : ↑↑μ U = 0
x✝¹ : G
x✝ : x✝¹ ∈ ↑t
⊢ ↑↑μ (x✝¹ • U) = 0
[PROOFSTEP]
rwa [measure_smul]
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
c : G
μ : Measure α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousConstSMul G α
inst✝ : MulAction.IsMinimal G α
K U : Set α
hU : IsOpen U
hne : Set.Nonempty U
hμU : ↑↑μ U ≠ ⊤
x : α
g : G
hg : g • x ∈ U
⊢ ↑↑μ ((fun x x_1 => x • x_1) g ⁻¹' U) ≠ ⊤
[PROOFSTEP]
rwa [measure_preimage_smul]
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSMul G α
c : G
μ : Measure α
inst✝⁴ : SMulInvariantMeasure G α μ
inst✝³ : TopologicalSpace α
inst✝² : ContinuousConstSMul G α
inst✝¹ : MulAction.IsMinimal G α
K U : Set α
inst✝ : Regular μ
hμ : μ ≠ 0
hU : IsOpen U
⊢ ↑↑μ U = 0 ↔ U = ∅
[PROOFSTEP]
rw [← not_iff_not, ← Ne.def, ← pos_iff_ne_zero, measure_pos_iff_nonempty_of_smulInvariant G hμ hU,
  nonempty_iff_ne_empty]
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x y : G
hs : x • s =ᶠ[ae μ] s
hy : y ∈ Subgroup.zpowers x
⊢ y • s =ᶠ[ae μ] s
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp hy
[GOAL]
case intro
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
⊢ x ^ k • s =ᶠ[ae μ] s
[PROOFSTEP]
let e : α ≃ α := MulAction.toPermHom G α x
[GOAL]
case intro
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
⊢ x ^ k • s =ᶠ[ae μ] s
[PROOFSTEP]
have he : QuasiMeasurePreserving e μ μ := (measurePreserving_smul x μ).quasiMeasurePreserving
[GOAL]
case intro
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
⊢ x ^ k • s =ᶠ[ae μ] s
[PROOFSTEP]
have he' : QuasiMeasurePreserving e.symm μ μ := (measurePreserving_smul x⁻¹ μ).quasiMeasurePreserving
[GOAL]
case intro
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
⊢ x ^ k • s =ᶠ[ae μ] s
[PROOFSTEP]
have h := he.image_zpow_ae_eq he' k hs
[GOAL]
case intro
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
h : ↑(e ^ k) '' s =ᶠ[ae μ] s
⊢ x ^ k • s =ᶠ[ae μ] s
[PROOFSTEP]
simp only [← MonoidHom.map_zpow] at h
[GOAL]
case intro
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
h : (fun a => ↑(↑(MulAction.toPermHom G α) (x ^ k)) a) '' s =ᶠ[ae μ] s
⊢ x ^ k • s =ᶠ[ae μ] s
[PROOFSTEP]
simpa only [MulAction.toPermHom_apply, MulAction.toPerm_apply, image_smul] using h
[GOAL]
G✝ : Type u
M : Type v
α✝ : Type w
s✝ : Set α✝
m✝ : MeasurableSpace α✝
inst✝⁹ : Group G✝
inst✝⁸ : MulAction G✝ α✝
inst✝⁷ : MeasurableSpace G✝
inst✝⁶ : MeasurableSMul G✝ α✝
c : G✝
μ✝ : Measure α✝
inst✝⁵ : SMulInvariantMeasure G✝ α✝ μ✝
G : Type u
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : AddGroup G
inst✝³ : AddAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableVAdd G α
μ : Measure α
inst✝ : VAddInvariantMeasure G α μ
x y : G
hs : x +ᵥ s =ᶠ[ae μ] s
hy : y ∈ AddSubgroup.zmultiples x
⊢ y +ᵥ s =ᶠ[ae μ] s
[PROOFSTEP]
letI : MeasurableSpace (Multiplicative G) := (inferInstanceAs (MeasurableSpace G))
[GOAL]
G✝ : Type u
M : Type v
α✝ : Type w
s✝ : Set α✝
m✝ : MeasurableSpace α✝
inst✝⁹ : Group G✝
inst✝⁸ : MulAction G✝ α✝
inst✝⁷ : MeasurableSpace G✝
inst✝⁶ : MeasurableSMul G✝ α✝
c : G✝
μ✝ : Measure α✝
inst✝⁵ : SMulInvariantMeasure G✝ α✝ μ✝
G : Type u
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : AddGroup G
inst✝³ : AddAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableVAdd G α
μ : Measure α
inst✝ : VAddInvariantMeasure G α μ
x y : G
hs : x +ᵥ s =ᶠ[ae μ] s
hy : y ∈ AddSubgroup.zmultiples x
this : MeasurableSpace (Multiplicative G) := inferInstanceAs (MeasurableSpace G)
⊢ y +ᵥ s =ᶠ[ae μ] s
[PROOFSTEP]
letI : SMulInvariantMeasure (Multiplicative G) α μ :=
  ⟨fun g => VAddInvariantMeasure.measure_preimage_vadd (Multiplicative.toAdd g)⟩
[GOAL]
G✝ : Type u
M : Type v
α✝ : Type w
s✝ : Set α✝
m✝ : MeasurableSpace α✝
inst✝⁹ : Group G✝
inst✝⁸ : MulAction G✝ α✝
inst✝⁷ : MeasurableSpace G✝
inst✝⁶ : MeasurableSMul G✝ α✝
c : G✝
μ✝ : Measure α✝
inst✝⁵ : SMulInvariantMeasure G✝ α✝ μ✝
G : Type u
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : AddGroup G
inst✝³ : AddAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableVAdd G α
μ : Measure α
inst✝ : VAddInvariantMeasure G α μ
x y : G
hs : x +ᵥ s =ᶠ[ae μ] s
hy : y ∈ AddSubgroup.zmultiples x
this✝ : MeasurableSpace (Multiplicative G) := inferInstanceAs (MeasurableSpace G)
this : SMulInvariantMeasure (Multiplicative G) α μ :=
  { measure_preimage_smul := fun g => VAddInvariantMeasure.measure_preimage_vadd (↑Multiplicative.toAdd g) }
⊢ y +ᵥ s =ᶠ[ae μ] s
[PROOFSTEP]
letI : MeasurableSMul (Multiplicative G) α :=
  { measurable_const_smul := fun g => measurable_const_vadd (Multiplicative.toAdd g)
    measurable_smul_const := fun a =>
      @measurable_vadd_const (Multiplicative G) α (inferInstanceAs (VAdd G α)) _ _
        (inferInstanceAs (MeasurableVAdd G α)) a }
[GOAL]
G✝ : Type u
M : Type v
α✝ : Type w
s✝ : Set α✝
m✝ : MeasurableSpace α✝
inst✝⁹ : Group G✝
inst✝⁸ : MulAction G✝ α✝
inst✝⁷ : MeasurableSpace G✝
inst✝⁶ : MeasurableSMul G✝ α✝
c : G✝
μ✝ : Measure α✝
inst✝⁵ : SMulInvariantMeasure G✝ α✝ μ✝
G : Type u
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : AddGroup G
inst✝³ : AddAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableVAdd G α
μ : Measure α
inst✝ : VAddInvariantMeasure G α μ
x y : G
hs : x +ᵥ s =ᶠ[ae μ] s
hy : y ∈ AddSubgroup.zmultiples x
this✝¹ : MeasurableSpace (Multiplicative G) := inferInstanceAs (MeasurableSpace G)
this✝ : SMulInvariantMeasure (Multiplicative G) α μ :=
  { measure_preimage_smul := fun g => VAddInvariantMeasure.measure_preimage_vadd (↑Multiplicative.toAdd g) }
this : MeasurableSMul (Multiplicative G) α :=
  { measurable_const_smul := fun g => measurable_const_vadd (↑Multiplicative.toAdd g),
    measurable_smul_const := fun a => measurable_vadd_const a }
⊢ y +ᵥ s =ᶠ[ae μ] s
[PROOFSTEP]
exact @smul_ae_eq_self_of_mem_zpowers (Multiplicative G) α _ _ _ _ _ _ _ _ _ _ hs hy