-- Mathlib/MeasureTheory/Group/Prod.lean
theorem quasiMeasurePreserving_mul_left [IsMulRightInvariant μ] (g : G) :
    QuasiMeasurePreserving (fun h : G => g * h) μ μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this✝ : QuasiMeasurePreserving (fun h => h * g⁻¹) μ μ
this : QuasiMeasurePreserving (fun x => g * x) μ μ
⊢ QuasiMeasurePreserving (fun h => g * h) μ μ

Tactic:
exact this

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this : QuasiMeasurePreserving (fun h => h * g⁻¹) μ μ
⊢ QuasiMeasurePreserving (fun h => g * h) μ μ

Tactic:
have :=
  (quasiMeasurePreserving_inv_of_right_invariant μ).comp
    (this.comp (quasiMeasurePreserving_inv_of_right_invariant μ))

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
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) μ μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
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) μ μ

Tactic:
simp_rw [Function.comp_def, mul_inv_rev, inv_inv] at this

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this✝ : QuasiMeasurePreserving (fun h => h * g⁻¹) μ μ
this : QuasiMeasurePreserving (fun x => g * x) μ μ
⊢ QuasiMeasurePreserving (fun h => g * h) μ μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this : QuasiMeasurePreserving (fun h => h * g⁻¹) μ.inv.inv μ.inv.inv
⊢ QuasiMeasurePreserving (fun h => g * h) μ μ

Tactic:
rw [μ.inv_inv] at this

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this : QuasiMeasurePreserving (fun h => h * g⁻¹) μ μ
⊢ QuasiMeasurePreserving (fun h => g * h) μ μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ QuasiMeasurePreserving (fun h => g * h) μ μ

Tactic:
have :=
  (quasiMeasurePreserving_mul_right μ.inv g⁻¹).mono (inv_absolutelyContinuous μ.inv)
    (absolutelyContinuous_inv μ.inv)

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this : QuasiMeasurePreserving (fun h => h * g⁻¹) μ.inv.inv μ.inv.inv
⊢ QuasiMeasurePreserving (fun h => g * h) μ μ