awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Pointwise
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : MeasurableConstSMul G α
s : Set α
hs : MeasurableSet s
a : G
⊢ MeasurableSet (α := α) ((fun (x : α) ↦ a⁻¹ • x) ⁻¹' s)

Tactic:
measurable_const_smul _ hs

Premises used: MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.Pointwise
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : MeasurableConstSMul G α
s : Set α
hs : MeasurableSet s
a : G
⊢ MeasurableSet (α := α) ((fun (x : α) ↦ a⁻¹ • x) ⁻¹' s)

Tactic:
exact measurable_const_smul _ hs

Premises used: MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.Pointwise
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : MulAction G₀ α
inst_2 : MeasurableSpace α
inst_3 : MeasurableConstSMul G₀ α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
rw : MeasurableSet (α := α) ((fun (x : α) ↦ a⁻¹ • x) ⁻¹' s)
⊢ MeasurableSet (a • s)

Tactic:
rw [← preimage_smul_inv₀ ha]

Premises used: Set.preimage_smul_inv₀
-- Module: Mathlib.MeasureTheory.Group.Pointwise
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : MulAction G₀ α
inst_2 : MeasurableSpace α
inst_3 : MeasurableConstSMul G₀ α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (α := α) ((fun (x : α) ↦ a⁻¹ • x) ⁻¹' s)

Tactic:
measurable_const_smul _ hs

Premises used: MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.Pointwise
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : MulAction G₀ α
inst_2 : MeasurableSpace α
inst_3 : MeasurableConstSMul G₀ α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (α := α) ((fun (x : α) ↦ a⁻¹ • x) ⁻¹' s)

Tactic:
exact measurable_const_smul _ hs

Premises used: MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.Pointwise
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Zero α
inst_2 : MulActionWithZero G₀ α
inst_3 : MeasurableSpace α
inst_4 : MeasurableConstSMul G₀ α
inst_5 : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
inl : MeasurableSet (HSMul.hSMul.{u_1, u_2, u_2} (α := G₀) 0 s)
inr : ∀ (ha : a ≠ 0), MeasurableSet (a • s)
⊢ MeasurableSet (a • s)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Group.Pointwise
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Zero α
inst_2 : MulActionWithZero G₀ α
inst_3 : MeasurableSpace α
inst_4 : MeasurableConstSMul G₀ α
inst_5 : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (HSMul.hSMul.{u_1, u_2, u_2} (α := G₀) 0 s)

Tactic:
(subsingleton_zero_smul_set s).measurableSet

Premises used: Set.subsingleton_zero_smul_set, Set.Subsingleton.measurableSet
-- Module: Mathlib.MeasureTheory.Group.Pointwise
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Zero α
inst_2 : MulActionWithZero G₀ α
inst_3 : MeasurableSpace α
inst_4 : MeasurableConstSMul G₀ α
inst_5 : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (a • s)

Tactic:
hs.const_smul_of_ne_zero ha

Premises used: MeasurableSet.const_smul_of_ne_zero
-- Module: Mathlib.MeasureTheory.Group.Pointwise
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Zero α
inst_2 : MulActionWithZero G₀ α
inst_3 : MeasurableSpace α
inst_4 : MeasurableConstSMul G₀ α
inst_5 : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (HSMul.hSMul.{u_1, u_2, u_2} (α := G₀) 0 s)

Tactic:
exacts [(subsingleton_zero_smul_set s).measurableSet, hs.const_smul_of_ne_zero ha]

Premises used: Set.subsingleton_zero_smul_set, Set.Subsingleton.measurableSet
-- 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 : ν.IsMulLeftInvariant
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.1, z.1 * z.2)) (μ.prod ν) (μ.prod ν)

Tactic:
(MeasurePreserving.id μ).skew_product measurable_mul <|
    Filter.Eventually.of_forall <| map_mul_left_eq_self ν

Premises used: MeasureTheory.map_mul_left_eq_self, MeasurableMul₂.measurable_mul, Filter.Eventually.of_forall, MeasureTheory.MeasurePreserving.skew_product, MeasureTheory.MeasurePreserving.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 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.2, z.2 * z.1)) (μ.prod ν) (ν.prod μ)

Tactic:
(measurePreserving_prod_mul ν μ).comp measurePreserving_swap

Premises used: MeasureTheory.measurePreserving_prod_mul, MeasureTheory.MeasurePreserving.comp, MeasureTheory.Measure.measurePreserving_swap
-- 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
hs : MeasurableSet s
this :
  Measurable (β := ℝ≥0∞) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
⊢ Measurable (β := ℝ≥0∞) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))

Tactic:
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 μ
s : Set G
hs : MeasurableSet s
this :
  Measurable (β := ℝ≥0∞) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
h :
  Eq.{u_1 + 1} (α := G → ℝ≥0∞) (fun (x : G) ↦ (μ : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s)) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
⊢ Measurable (β := ℝ≥0∞) fun (x : G) ↦ (μ : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s)

Tactic:
convert! this using 1
-- 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
hs : MeasurableSet s
this :
  Measurable (β := ℝ≥0∞) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
h :
  ∀ (x : G),
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set G) → ℝ≥0∞)
          (preimage (β := G × G) (fun (x_1 : G) ↦ (x_1, x))
            ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s)) :
        ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := G → ℝ≥0∞) (fun (x : G) ↦ (μ : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s)) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))

Tactic:
ext1 x
-- 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
hs : MeasurableSet s
this :
  Measurable (β := ℝ≥0∞) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
x : G
h :
  ∀ (y : G),
    Membership.mem (γ := Set G) ((fun (y : G) ↦ y * x) ⁻¹' s) y ↔
      Membership.mem (γ := Set G)
        (preimage (β := G × G) (fun (x_1 : G) ↦ (x_1, x))
          ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
        y
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞)
        (preimage (β := G × G) (fun (x_1 : G) ↦ (x_1, x))
          ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s)) :
      ℝ≥0∞)

Tactic:
congr 1 with y : 1
-- 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
hs : MeasurableSet s
this :
  Measurable (β := ℝ≥0∞) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
x y : G
⊢ Membership.mem (γ := Set G) ((fun (y : G) ↦ y * x) ⁻¹' s) y ↔
    Membership.mem (γ := Set G)
      (preimage (β := G × G) (fun (x_1 : G) ↦ (x_1, x))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
      y

Tactic:
simp
-- 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
hs : MeasurableSet s
Measurable :
  _root_.Measurable (β := ℝ≥0∞) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
⊢ _root_.Measurable (β := ℝ≥0∞) fun (x : G) ↦ (μ : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s)

Tactic:
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
-- 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
hs : MeasurableSet s
hs₁ : MeasurableSet (α := G × G) ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s)
⊢ Measurable (β := ℝ≥0∞) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))

Tactic:
apply measurable_measure_prodMk_right

Premises used: measurable_measure_prodMk_right
-- 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
hs : MeasurableSet s
apply : MeasurableSpace G
⊢ MeasurableSet (α := G × G) ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s)

Tactic:
apply measurable_const.prodMk measurable_mul (MeasurableSet.univ.prod hs)

Premises used: MeasurableMul₂.measurable_mul, Measurable.prodMk, MeasurableSet.prod, measurable_const, MeasurableSet.univ
-- 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
hs : MeasurableSet s
⊢ MeasurableSpace G

Tactic:
infer_instance
-- 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
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.1, z.1⁻¹ * z.2)) (μ.prod ν) (μ.prod ν)

Tactic:
(measurePreserving_prod_mul μ ν).symm <| MeasurableEquiv.shearMulRight G

Premises used: MeasureTheory.MeasurePreserving.symm, MeasurableEquiv.shearMulRight, MeasureTheory.measurePreserving_prod_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 ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) (μ.prod ν) (ν.prod μ)

Tactic:
(measurePreserving_prod_inv_mul ν μ).comp measurePreserving_swap

Premises used: MeasureTheory.MeasurePreserving.comp, MeasureTheory.measurePreserving_prod_inv_mul, MeasureTheory.Measure.measurePreserving_swap
-- 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
⊢ MeasurePreserving ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1)) (μ.prod ν) (μ.prod ν)

Tactic:
(measurePreserving_prod_inv_mul_swap ν μ).comp (measurePreserving_prod_mul_swap μ ν)

Premises used: MeasureTheory.measurePreserving_prod_mul_swap, MeasureTheory.measurePreserving_prod_inv_mul_swap, MeasureTheory.MeasurePreserving.comp
-- 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
h :
  Eq.{u_1 + 1} (α := G × G → G × G) (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹))
    ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1))
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (μ.prod ν)

Tactic:
convert!
    (measurePreserving_prod_inv_mul_swap ν μ).comp (measurePreserving_prod_mul_swap μ ν) using 1

Premises used: MeasureTheory.measurePreserving_prod_mul_swap, MeasureTheory.measurePreserving_prod_inv_mul_swap, MeasureTheory.MeasurePreserving.comp
-- 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
h :
  ∀ (x y : G),
    ((x, y).2 * (x, y).1, (x, y).1⁻¹) =
      ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1)) (x, y)
⊢ Eq.{u_1 + 1} (α := G × G → G × G) (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹))
    ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1))

Tactic:
ext1 ⟨x, y⟩
-- 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
x y : G
h h₁ : (y * x, x⁻¹) = ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1)) (x, y)
h₂ : (y * x, x⁻¹) = (y * x, (y * x)⁻¹ * y)
h₃ : (y * x, x⁻¹) = (y * x, x⁻¹ * y⁻¹ * y)
⊢ ((x, y).2 * (x, y).1, (x, y).1⁻¹) =
    ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1)) (x, y)

Tactic:
simp_rw [Function.comp_apply, mul_inv_rev, inv_mul_cancel_right]

Premises used: Function.comp_apply, mul_inv_rev, inv_mul_cancel_right
-- 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
⊢ QuasiMeasurePreserving Inv.inv μ μ

Tactic:
⟨measurable_inv, AbsolutelyContinuous.mk fun s hsm hμs => ?_⟩

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk, MeasureTheory.Measure.QuasiMeasurePreserving.mk, MeasurableInv.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
refine :
  ∀ (s : Set G) (hsm : MeasurableSet s) (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) (((map Inv.inv μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ QuasiMeasurePreserving Inv.inv μ μ

Tactic:
refine ⟨measurable_inv, AbsolutelyContinuous.mk fun s hsm hμs => ?_⟩
-- 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
hsm : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map Inv.inv μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [map_apply measurable_inv hsm, inv_preimage]

Premises used: MeasureTheory.Measure.map_apply, MeasurableInv.measurable_inv, 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
s : Set G
hsm : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)

Tactic:
have hf : 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 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hf : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
this :
  Eq (α := ℝ≥0∞)
    (((map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod μ) : Measure (G × G)) : (a : Set (G × G)) → ℝ≥0∞)
        (s⁻¹ ×ˢ s⁻¹) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa only [(measurePreserving_mul_prod_inv μ μ).map_eq, prod_prod, mul_eq_zero (M₀ := ℝ≥0∞),
      or_self_iff] using this

Premises used: or_self_iff, MeasureTheory.Measure.prod_prod, MeasureTheory.MeasurePreserving.map_eq, mul_eq_zero, 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 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hf : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
suffices :
  Eq (α := ℝ≥0∞)
    (((map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod μ) : Measure (G × G)) : (a : Set (G × G)) → ℝ≥0∞)
        (s⁻¹ ×ˢ s⁻¹) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
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
-- 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
hsm : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hf : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
⊢ MeasurableSet (s⁻¹ ×ˢ s⁻¹)

Tactic:
have hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹) := hsm.inv.prod hsm.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
s : Set G
hsm : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hf : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹)
simp_rw :
  Eq (α := ℝ≥0∞) ((μ.prod μ : (a : Set (G × G)) → ℝ≥0∞) ((fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) ⁻¹' s⁻¹ ×ˢ s⁻¹) : ℝ≥0∞)
    (0 : ℝ≥0∞)
simp_rw₁ :
  ∫⁻ (y : G),
      (μ : (a : Set G) → ℝ≥0∞)
        (preimage (β := G × G) (fun (x : G) ↦ (x, y)) ((fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) ⁻¹' s⁻¹ ×ˢ s⁻¹)) ∂μ =
    0
simp_rw₂ : ∫⁻ (y : G), (μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ (y * x, x⁻¹)) ⁻¹' s⁻¹ ×ˢ s⁻¹) ∂μ = 0
simp_rw₃ : ∫⁻ (y : G), (μ : (a : Set G) → ℝ≥0∞) (HMul.hMul y ⁻¹' s⁻¹ ∩ Inv.inv ⁻¹' s⁻¹) ∂μ = 0
simp_rw₄ : ∫⁻ (y : G), (μ : (a : Set G) → ℝ≥0∞) (HMul.hMul y ⁻¹' s⁻¹ ∩ s⁻¹⁻¹) ∂μ = 0
simp_rw₅ : ∫⁻ (y : G), (μ : (a : Set G) → ℝ≥0∞) (HMul.hMul y ⁻¹' s⁻¹ ∩ s) ∂μ = 0
simp_rw₆ : ∫⁻ (y : G), 0 ∂μ = 0
⊢ Eq (α := ℝ≥0∞)
    (((map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod μ) : Measure (G × G)) : (a : Set (G × G)) → ℝ≥0∞)
        (s⁻¹ ×ˢ s⁻¹) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
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]

Premises used: MeasureTheory.Measure.prod_apply_symm, Set.preimage_preimage, MeasureTheory.Measure.map_apply, MeasureTheory.lintegral_zero, MeasureTheory.measure_mono_null, inv_inv, Set.inv_preimage, Set.inter_subset_right, Set.mk_preimage_prod
-- 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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨fun hs => ?_, (quasiMeasurePreserving_inv μ).preimage_null⟩

Premises used: Iff.intro, MeasureTheory.quasiMeasurePreserving_inv, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null
-- 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
refine :
  ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine ⟨fun hs => ?_, (quasiMeasurePreserving_inv μ).preimage_null⟩
-- 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
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← inv_inv s]

Premises used: 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 μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(quasiMeasurePreserving_inv μ).preimage_null hs

Premises used: MeasureTheory.quasiMeasurePreserving_inv, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null
-- 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
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact (quasiMeasurePreserving_inv μ).preimage_null hs

Premises used: MeasureTheory.quasiMeasurePreserving_inv, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null
-- 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:
le_antisymm (quasiMeasurePreserving_inv μ).tendsto_ae ?_

Premises used: le_antisymm, MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae, MeasureTheory.quasiMeasurePreserving_inv