awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulRightInvariant
map_mul_left_eq_self : ∀ (g : G), map (fun (x : G) ↦ g * x) μ.inv = μ.inv
⊢ μ.inv.IsMulLeftInvariant

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulRightInvariant
g : G
rw : Measure.inv (map (fun (x : G) ↦ x * g⁻¹) μ)
| μ.inv

Tactic:
rw [← map_mul_right_eq_self μ g⁻¹]

Premises used: Inv.inv, MeasureTheory.map_mul_right_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulRightInvariant
g : G
map_mul_left_eq_self :
  Eq (α := Measure G) (map (fun (x : G) ↦ g * x) μ.inv) (Measure.inv (map (fun (x : G) ↦ x * g⁻¹) μ))
⊢ map (fun (x : G) ↦ g * x) μ.inv = μ.inv

Tactic:
conv_rhs => rw [← map_mul_right_eq_self μ g⁻¹]

Premises used: Inv.inv, MeasureTheory.map_mul_right_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulRightInvariant
g : G
map_mul_left_eq_self :
  Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map inv μ)) (map inv (map (fun (x : G) ↦ x * g⁻¹) μ))
map_mul_left_eq_self₁ :
  Eq (α := Measure G) (map ((fun (x : G) ↦ g * x) ∘ inv) μ) (map inv (map (fun (x : G) ↦ x * g⁻¹) μ))
map_mul_left_eq_self₂ : Eq (α := Measure G) (map ((fun (x : G) ↦ g * x) ∘ inv) μ) (map (inv ∘ fun (x : G) ↦ x * g⁻¹) μ)
map_mul_left_eq_self₃ : Eq (α := Measure G) (map (fun (x : G) ↦ g * x⁻¹) μ) (map (fun (x : G) ↦ (x * g⁻¹)⁻¹) μ)
map_mul_left_eq_self₄ : Eq (α := Measure G) (map (fun (x : G) ↦ g * x⁻¹) μ) (map (fun (x : G) ↦ g⁻¹⁻¹ * x⁻¹) μ)
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ g * x) μ.inv) (Measure.inv (map (fun (x : G) ↦ x * g⁻¹) μ))

Tactic:
simp_rw [Measure.inv, map_map (measurable_const_mul g) measurable_inv,
    map_map measurable_inv (measurable_mul_const g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]

Premises used: MeasurableMul.measurable_const_mul, MeasurableInv.measurable_inv, Function.comp_def, Inv.inv, inv_inv, MeasurableMul.measurable_mul_const, mul_inv_rev, MeasureTheory.Measure.inv, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : DivisionMonoid G
inst_2 : MeasurableMul G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : μ.IsInvInvariant
inst_5 : μ.IsMulLeftInvariant
g : G
simp_rw : MeasurePreserving (fun (t : G) ↦ g * t⁻¹) μ μ
⊢ MeasurePreserving (fun (t : G) ↦ g / t) μ μ

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : DivisionMonoid G
inst_2 : MeasurableMul G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : μ.IsInvInvariant
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ MeasurePreserving (fun (t : G) ↦ g * t⁻¹) μ μ

Tactic:
(measurePreserving_mul_left μ g).comp (measurePreserving_inv μ)

Premises used: MeasureTheory.measurePreserving_mul_left, MeasureTheory.Measure.measurePreserving_inv, MeasureTheory.MeasurePreserving.comp
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : DivisionMonoid G
inst_2 : MeasurableMul G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : μ.IsInvInvariant
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ MeasurePreserving (fun (t : G) ↦ g * t⁻¹) μ μ

Tactic:
exact (measurePreserving_mul_left μ g).comp (measurePreserving_inv μ)

Premises used: MeasureTheory.measurePreserving_mul_left, MeasureTheory.Measure.measurePreserving_inv, MeasureTheory.MeasurePreserving.comp
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : DivisionMonoid G
inst_2 : MeasurableMul G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : μ.IsInvInvariant
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ map (fun (t : G) ↦ g / t) μ = μ

Tactic:
(measurePreserving_div_left μ g).map_eq

Premises used: MeasureTheory.Measure.measurePreserving_div_left, MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : DivisionMonoid G
inst_2 : MeasurableMul G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : μ.IsInvInvariant
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ MeasurePreserving (fun (t : G) ↦ (g * t)⁻¹) μ μ

Tactic:
(measurePreserving_inv μ).comp <| measurePreserving_mul_left μ g

Premises used: MeasureTheory.measurePreserving_mul_left, MeasureTheory.Measure.measurePreserving_inv, MeasureTheory.MeasurePreserving.comp
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : DivisionMonoid G
inst_2 : MeasurableMul G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : μ.IsInvInvariant
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ map (fun (t : G) ↦ (g * t)⁻¹) μ = μ

Tactic:
(measurePreserving_mul_right_inv μ g).map_eq

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.Measure.measurePreserving_mul_right_inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
h :
  ∀ (s : Set G) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ g * x) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
      (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Measure G) (map (fun (x : G) ↦ g * x) count) count

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
h : ((map (fun (x : G) ↦ g * x) count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
h₁ : ((count : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' s) = (↑s.encard : ℝ≥0∞)
h₂ : (↑(encard (α := G) ((fun (x : G) ↦ g * x) ⁻¹' s)) : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
h₃ h₄ : (↑s.encard : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ g * x) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [count_apply hs, map_apply (measurable_const_mul _) hs,
      count_apply (measurable_const_mul _ hs),
      encard_preimage_of_bijective (Group.mulLeft_bijective _)]

Premises used: MeasureTheory.Measure.count_apply, MeasureTheory.Measure.map_apply, MeasurableMul.measurable_const_mul, Group.mulLeft_bijective, Set.encard_preimage_of_bijective
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
h :
  ∀ (s : Set G) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
      (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Measure G) (map (fun (x : G) ↦ x * g) count) count

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
h : ((map (fun (x : G) ↦ x * g) count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
h₁ : ((count : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * g) ⁻¹' s) = (↑s.encard : ℝ≥0∞)
h₂ : (↑(encard (α := G) ((fun (x : G) ↦ x * g) ⁻¹' s)) : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
h₃ h₄ : (↑s.encard : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [count_apply hs, map_apply (measurable_mul_const _) hs,
      count_apply (measurable_mul_const _ hs),
      encard_preimage_of_bijective (Group.mulRight_bijective _)]

Premises used: MeasureTheory.Measure.count_apply, MeasureTheory.Measure.map_apply, Group.mulRight_bijective, MeasurableMul.measurable_mul_const, Set.encard_preimage_of_bijective
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
h :
  ∀ (s : Set G) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      (((map (fun (x : G) ↦ g * x) (comap (⇑f : (a : G) → H) μ) : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
      (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Measure G) (map (fun (x : G) ↦ g * x) (comap (⇑f : (a : G) → H) μ)) (comap (⇑f : (a : G) → H) μ)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
⊢ Measurable (β := G) fun (x : G) ↦ g * x

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' s) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ g * x) (comap (⇑f : (a : G) → H) μ) : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply (by fun_prop) hs]

Premises used: MeasureTheory.Measure.map_apply
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' s) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [hf.comap_apply]

Premises used: MeasurableEmbedding.comap_apply
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set H) → ℝ≥0∞) ((⇑f : (a : G) → H) '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [hf.comap_apply]

Premises used: MeasurableEmbedding.comap_apply
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set H) → ℝ≥0∞) ((⇑f : (a : G) → H) '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' s) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
repeat rw [hf.comap_apply]

Premises used: MeasurableEmbedding.comap_apply
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
h :
  ∀ (x : H),
    Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) x ↔
      Membership.mem (γ := Set H)
        (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s)) x
⊢ Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s))

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
x : H
h :
  Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) x →
    Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s)) x
h₁ :
  Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s)) x →
    Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) x
⊢ Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) x ↔
    Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s)) x

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
y : G
hy : Membership.mem (γ := Set G) ((fun (x : G) ↦ g * x) ⁻¹' s) y
⊢ Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) (g * y) : H)
    ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((f : (a : G) → H) y) : H)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
y : G
hy : Membership.mem (γ := Set G) ((fun (x : G) ↦ g * x) ⁻¹' s) y
⊢ Membership.mem.{u_3, u_3} (α := H) (γ := Set H)
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s))
    ((f : (a : G) → H) y : H)

Tactic:
exact ⟨g * y, hy, by simp⟩
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
x : H
y : G
yins : y ∈ s
hy :
  Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) y : H) ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) x : H)
⊢ Membership.mem (γ := Set G) ((fun (x : G) ↦ g * x) ⁻¹' s) (g⁻¹ * y)

Tactic:
simp [yins]
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
x : H
y : G
yins : y ∈ s
hy :
  Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) y : H) ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) x : H)
⊢ (f : (a : G) → H) (g⁻¹ * y) = x

Tactic:
simp [hy]
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
x : H
y : G
yins : y ∈ s
hy :
  Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) y : H) ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) x : H)
⊢ Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) x

Tactic:
exact ⟨g⁻¹ * y, by simp [yins], by simp [hy]⟩
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s))

Tactic:
have : f '' (g * ·) ⁻¹' s = (f g * ·) ⁻¹' f '' s := by
      ext
      constructor
      · rintro ⟨y, hy, rfl⟩
        exact ⟨g * y, hy, by simp⟩
      · intro ⟨y, yins, hy⟩
        exact ⟨g⁻¹ * y, by simp [yins], by simp [hy]⟩
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
this :
  Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s))
⊢ Measurable (β := H) fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
this :
  Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s))
h : MeasurableSet.{u_3} (α := H) ((⇑f : (a : G) → H) '' s)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set H) → ℝ≥0∞) ((⇑f : (a : G) → H) '' s) : ℝ≥0∞)

Tactic:
rw [this, ← map_apply (by fun_prop), IsMulLeftInvariant.map_mul_left_eq_self]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.IsMulLeftInvariant.map_mul_left_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
this :
  Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s))
⊢ MeasurableSet.{u_3} (α := H) ((⇑f : (a : G) → H) '' s)

Tactic:
hf.measurableSet_image.mpr hs

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
this :
  Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s))
⊢ MeasurableSet.{u_3} (α := H) ((⇑f : (a : G) → H) '' s)

Tactic:
exact hf.measurableSet_image.mpr hs

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
h :
  ∀ (s : Set G) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      (((map (fun (x : G) ↦ x * g) (comap (⇑f : (a : G) → H) μ) : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
      (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Measure G) (map (fun (x : G) ↦ x * g) (comap (⇑f : (a : G) → H) μ)) (comap (⇑f : (a : G) → H) μ)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
⊢ Measurable (β := G) fun (x : G) ↦ x * g

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * g) ⁻¹' s) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) (comap (⇑f : (a : G) → H) μ) : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply (by fun_prop) hs]

Premises used: MeasureTheory.Measure.map_apply