awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
refine : ae μ ≤ (ae μ)⁻¹
⊢ (ae μ)⁻¹ = ae μ

Tactic:
refine le_antisymm (quasiMeasurePreserving_inv μ).tendsto_ae ?_

Premises used: le_antisymm, MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae, MeasureTheory.quasiMeasurePreserving_inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
nth_rewrite : (ae μ)⁻¹⁻¹ ≤ (ae μ)⁻¹
⊢ ae μ ≤ (ae μ)⁻¹

Tactic:
nth_rewrite 1 [← inv_inv (ae μ)]

Premises used: MeasureTheory.ae, inv_inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
⊢ (ae μ)⁻¹⁻¹ ≤ (ae μ)⁻¹

Tactic:
Filter.map_mono (quasiMeasurePreserving_inv μ).tendsto_ae

Premises used: Filter.map_mono, Set.Mem, MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae, MeasureTheory.quasiMeasurePreserving_inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
⊢ (ae μ)⁻¹⁻¹ ≤ (ae μ)⁻¹

Tactic:
exact Filter.map_mono (quasiMeasurePreserving_inv μ).tendsto_ae

Premises used: Filter.map_mono, MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae, MeasureTheory.quasiMeasurePreserving_inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
rw : EventuallyConst (Inv.inv ⁻¹' s) (ae μ) ↔ EventuallyConst s (ae μ)
rw₁ : EventuallyConst s (Filter.map Inv.inv (ae μ)) ↔ EventuallyConst s (ae μ)
rw₂ : EventuallyConst s (ae μ)⁻¹ ↔ EventuallyConst s (ae μ)
rw₃ rw₄ : EventuallyConst s (ae μ) ↔ EventuallyConst s (ae μ)
⊢ EventuallyConst s⁻¹ (ae μ) ↔ EventuallyConst s (ae μ)

Tactic:
rw [← inv_preimage, eventuallyConst_preimage, Filter.map_inv, inv_ae]

Premises used: Filter.map_inv, MeasureTheory.inv_ae, Filter.eventuallyConst_preimage, Set.inv_preimage
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
⊢ μ.inv ≪ μ

Tactic:
(quasiMeasurePreserving_inv μ).absolutelyContinuous

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.quasiMeasurePreserving_inv, MeasureTheory.Measure.inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
⊢ μ ≪ μ.inv

Tactic:
AbsolutelyContinuous.mk fun s _ => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
refine :
  ∀ (s : Set G),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((μ.inv : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ≪ μ.inv

Tactic:
refine AbsolutelyContinuous.mk fun s _ => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
s : Set G
h : MeasurableSet s
simp_rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.inv : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp_rw [inv_apply μ s, measure_inv_null, imp_self]

Premises used: MeasureTheory.measure_inv_null, MeasureTheory.Measure.inv_apply, imp_self
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
⊢ Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)

Tactic:
have h : Measurable fun z : G × G => (z.2 * z.1, z.1⁻¹) :=
    (measurable_snd.mul measurable_fst).prodMk measurable_fst.inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
⊢ AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ f (y * x) x⁻¹) (μ.prod ν)

Tactic:
have h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹) (μ.prod ν) :=
    hf.comp_quasiMeasurePreserving (measurePreserving_mul_prod_inv μ ν).quasiMeasurePreserving
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ f (y * x) x⁻¹) (μ.prod ν)
simp_rw : ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν = ∫⁻ (z : G × G), f z.1 z.2 ∂μ.prod ν
⊢ ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ

Tactic:
simp_rw [lintegral_lintegral h2f, lintegral_lintegral hf]

Premises used: MeasureTheory.lintegral_lintegral
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ f (y * x) x⁻¹) (μ.prod ν)
rw : ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν)
| ∫⁻ (z : G × G), f z.1 z.2 ∂μ.prod ν

Tactic:
rw [← (measurePreserving_mul_prod_inv μ ν).map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.measurePreserving_mul_prod_inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ f (y * x) x⁻¹) (μ.prod ν)
conv_rhs :
  ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν =
    ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν)
⊢ ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν = ∫⁻ (z : G × G), f z.1 z.2 ∂μ.prod ν

Tactic:
conv_rhs => rw [← (measurePreserving_mul_prod_inv μ ν).map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.measurePreserving_mul_prod_inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ f (y * x) x⁻¹) (μ.prod ν)
symm :
  ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν) =
    ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν
⊢ ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν =
    ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν)

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ f (y * x) x⁻¹) (μ.prod ν)
⊢ ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν) =
    ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν

Tactic:
lintegral_map' (hf.mono' (measurePreserving_mul_prod_inv μ ν).map_eq.absolutelyContinuous)
      h.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.MeasurePreserving.map_eq, Eq.absolutelyContinuous, MeasureTheory.measurePreserving_mul_prod_inv, MeasureTheory.lintegral_map', AEMeasurable.mono'
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ f (y * x) x⁻¹) (μ.prod ν)
⊢ ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν) =
    ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν

Tactic:
exact
    lintegral_map' (hf.mono' (measurePreserving_mul_prod_inv μ ν).map_eq.absolutelyContinuous)
      h.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.MeasurePreserving.map_eq, Eq.absolutelyContinuous, MeasureTheory.measurePreserving_mul_prod_inv, MeasureTheory.lintegral_map', AEMeasurable.mono'
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
y : G
simp_rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (Inv.inv ⁻¹' (fun (x : G) ↦ y⁻¹ * x) ⁻¹' Inv.inv ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ (y⁻¹ * x⁻¹)⁻¹) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x⁻¹⁻¹ * y⁻¹⁻¹) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp_rw [← inv_preimage, preimage_preimage, mul_inv_rev, inv_inv]

Premises used: Set.preimage_preimage, inv_inv, mul_inv_rev, Set.inv_preimage
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
y : G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [measure_inv_null μ, measure_preimage_mul]

Premises used: MeasureTheory.measure_inv_null, MeasureTheory.measure_preimage_mul
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
h2s : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
y : G
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(not_congr (measure_mul_right_null μ y)).mpr h2s

Premises used: Iff.mpr, MeasureTheory.measure_mul_right_null, not_congr
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ μ ≪ map (fun (x : G) ↦ x * g) μ

Tactic:
AbsolutelyContinuous.mk fun s hs => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
refine :
  ∀ (s : Set G) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ≪ map (fun (x : G) ↦ x * g) μ

Tactic:
refine AbsolutelyContinuous.mk fun s hs => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.measure_mul_right_null, MeasurableMul.measurable_mul_const
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
id

Premises used: id
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact id

Premises used: id
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
simp_rw : μ ≪ map (fun (h : G) ↦ g * h⁻¹) μ
⊢ μ ≪ map (fun (h : G) ↦ g / h) μ

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map Inv.inv μ)) (map ((fun (x : G) ↦ g * x) ∘ Inv.inv) μ)

Tactic:
have := map_map (μ := μ) (measurable_const_mul g) measurable_inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
this : Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map Inv.inv μ)) (map (fun (x : G) ↦ g * x⁻¹) μ)
rw : μ ≪ map (fun (x : G) ↦ g * x) (map Inv.inv μ)
⊢ μ ≪ map (fun (h : G) ↦ g * h⁻¹) μ

Tactic:
rw [← this]
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
this : Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map Inv.inv μ)) (map (fun (x : G) ↦ g * x⁻¹) μ)
rw : map (fun (x : G) ↦ g * x) μ
| μ

Tactic:
rw [← map_mul_left_eq_self μ g]

Premises used: MeasureTheory.map_mul_left_eq_self
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
this : Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map Inv.inv μ)) (map (fun (x : G) ↦ g * x⁻¹) μ)
conv_lhs :
  AbsolutelyContinuous (α := G) (_m0 := inst) (map (fun (x : G) ↦ g * x) μ) (map (fun (x : G) ↦ g * x) (map Inv.inv μ))
⊢ μ ≪ map (fun (x : G) ↦ g * x) (map Inv.inv μ)

Tactic:
conv_lhs => rw [← map_mul_left_eq_self μ g]

Premises used: MeasureTheory.map_mul_left_eq_self
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
this : Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map Inv.inv μ)) (map (fun (x : G) ↦ g * x⁻¹) μ)
⊢ AbsolutelyContinuous (α := G) (_m0 := inst) (map (fun (x : G) ↦ g * x) μ) (map (fun (x : G) ↦ g * x) (map Inv.inv μ))

Tactic:
(absolutelyContinuous_inv μ).map (measurable_const_mul g)

Premises used: MeasurableMul.measurable_const_mul, MeasureTheory.absolutelyContinuous_inv, MeasureTheory.Measure.inv, MeasureTheory.Measure.AbsolutelyContinuous.map
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
this : Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map Inv.inv μ)) (map (fun (x : G) ↦ g * x⁻¹) μ)
⊢ AbsolutelyContinuous (α := G) (_m0 := inst) (map (fun (x : G) ↦ g * x) μ) (map (fun (x : G) ↦ g * x) (map Inv.inv μ))

Tactic:
exact (absolutelyContinuous_inv μ).map (measurable_const_mul g)

Premises used: MeasurableMul.measurable_const_mul, MeasureTheory.absolutelyContinuous_inv, MeasureTheory.Measure.AbsolutelyContinuous.map
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
rw :
  ∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun (x : G) ↦ 1) (y * x) * f x⁻¹ ∂ν ∂μ =
    ∫⁻ (x : G), HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞) (f x⁻¹) ∂μ
hf₁ : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ s.indicator (fun (x : G) ↦ 1) x * f y) (μ.prod ν)
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∫⁻ (y : G), f y ∂ν) =
    ∫⁻ (x : G), HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞) (f x⁻¹) ∂μ

Tactic:
rw [← setLIntegral_one, ← lintegral_indicator sm,
    ← lintegral_lintegral_mul (measurable_const.indicator sm).aemeasurable hf.aemeasurable,
    ← lintegral_lintegral_mul_inv μ ν]

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_lintegral_mul, Measurable.indicator, MeasureTheory.lintegral_lintegral_mul_inv, MeasureTheory.setLIntegral_one, MeasureTheory.lintegral_indicator, measurable_const
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ s.indicator (fun (x : G) ↦ 1) x * f y) (μ.prod ν)

Tactic:
(((measurable_const.indicator sm).comp measurable_fst).mul
      (hf.comp measurable_snd)).aemeasurable

Premises used: Measurable.mul, Measurable.aemeasurable, Measurable.comp, Set.indicator, Measurable.indicator, measurable_snd, measurable_const, measurable_fst, ite
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ s.indicator (fun (x : G) ↦ 1) x * f y) (μ.prod ν)

Tactic:
exact (((measurable_const.indicator sm).comp measurable_fst).mul
      (hf.comp measurable_snd)).aemeasurable

Premises used: Measurable.mul, Measurable.aemeasurable, Measurable.comp, Measurable.indicator, measurable_snd, measurable_const, measurable_fst
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y

Tactic:
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)
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y
x y : G
symm :
  Eq (α := ℝ≥0∞) (indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (b : G) ↦ 1) y) (s.indicator (fun (x : G) ↦ 1) (y * x))
⊢ Eq (α := ℝ≥0∞) (s.indicator (fun (x : G) ↦ 1) (y * x)) (indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (b : G) ↦ 1) y)

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y
x y : G
⊢ Eq (α := ℝ≥0∞) (indicator ((fun (y : G) ↦ y * x) ⁻¹' s) ((fun (x : G) ↦ 1) ∘ fun (y : G) ↦ y * x) y)
    (s.indicator (fun (x : G) ↦ 1) (y * x))

Tactic:
indicator_comp_right (M := ℝ≥0∞) fun y => y * x

Premises used: HMul.hMul, Set.indicator_comp_right