awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableInv G
inst_4 : μ.IsInvInvariant
f : G → F
s : Set G
hf : IntegrableOn f s μ
apply : @Integrable _ _ _ _ inst f (map (⇑(MeasurableEquiv.inv G) : (a : G) → G) (μ.restrict s⁻¹))
⊢ IntegrableOn.{u_4, u_6} (ε := F) (fun (x : G) ↦ f x⁻¹) s⁻¹ μ

Tactic:
apply (integrable_map_equiv (MeasurableEquiv.inv G) f).mp

Premises used: MeasurableEquiv.inv, MeasureTheory.integrable_map_equiv, Iff.mp
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableInv G
inst_4 : μ.IsInvInvariant
f : G → F
s : Set G
hf : IntegrableOn f s μ
⊢ s⁻¹ = (⇑(MeasurableEquiv.inv G) : (a : G) → G) ⁻¹' s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableInv G
inst_4 : μ.IsInvInvariant
f : G → F
s : Set G
hf : IntegrableOn f s μ
⊢ s⁻¹ = (⇑(MeasurableEquiv.inv G) : (a : G) → G) ⁻¹' s

Tactic:
have : s⁻¹ = MeasurableEquiv.inv G ⁻¹' s := by simp
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableInv G
inst_4 : μ.IsInvInvariant
f : G → F
s : Set G
hf : IntegrableOn f s μ
this : s⁻¹ = (⇑(MeasurableEquiv.inv G) : (a : G) → G) ⁻¹' s
rw : @Integrable _ _ _ _ inst f (Measure.restrict (map (⇑(MeasurableEquiv.inv G) : (a : G) → G) μ) s)
⊢ @Integrable _ _ _ _ inst f (map (⇑(MeasurableEquiv.inv G) : (a : G) → G) (μ.restrict s⁻¹))

Tactic:
rw [this, ← MeasurableEquiv.restrict_map]

Premises used: MeasurableEquiv.restrict_map
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableInv G
inst_4 : μ.IsInvInvariant
f : G → F
s : Set G
hf : IntegrableOn f s μ
this : s⁻¹ = (⇑(MeasurableEquiv.inv G) : (a : G) → G) ⁻¹' s
⊢ @Integrable _ _ _ _ inst f (Measure.restrict (map (⇑(MeasurableEquiv.inv G) : (a : G) → G) μ) s)

Tactic:
simpa using hf
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : PartialOrder G
inst_3 : CommGroup G
inst_4 : IsOrderedMonoid G
inst_5 : MeasurableInv G
inst_6 : μ.IsInvInvariant
c : G
f : G → F
hf : IntegrableOn f (Set.Ici c⁻¹) μ
⊢ IntegrableOn.{u_4, u_6} (ε := F) (fun (x : G) ↦ f x⁻¹) (Set.Iic c) μ

Tactic:
simpa using hf.comp_inv

Premises used: MeasureTheory.IntegrableOn.comp_inv
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : PartialOrder G
inst_3 : CommGroup G
inst_4 : IsOrderedMonoid G
inst_5 : MeasurableInv G
inst_6 : μ.IsInvInvariant
c : G
f : G → F
hf : IntegrableOn f (Set.Iic c⁻¹) μ
⊢ IntegrableOn.{u_4, u_6} (ε := F) (fun (x : G) ↦ f x⁻¹) (Set.Ici c) μ

Tactic:
simpa using hf.comp_inv

Premises used: MeasureTheory.IntegrableOn.comp_inv
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : PartialOrder G
inst_3 : CommGroup G
inst_4 : IsOrderedMonoid G
inst_5 : MeasurableInv G
inst_6 : μ.IsInvInvariant
c : G
f : G → F
hf : IntegrableOn f (Set.Ioi c⁻¹) μ
⊢ IntegrableOn.{u_4, u_6} (ε := F) (fun (x : G) ↦ f x⁻¹) (Set.Iio c) μ

Tactic:
simpa using hf.comp_inv

Premises used: MeasureTheory.IntegrableOn.comp_inv
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : PartialOrder G
inst_3 : CommGroup G
inst_4 : IsOrderedMonoid G
inst_5 : MeasurableInv G
inst_6 : μ.IsInvInvariant
c : G
f : G → F
hf : IntegrableOn f (Set.Iio c⁻¹) μ
⊢ IntegrableOn.{u_4, u_6} (ε := F) (fun (x : G) ↦ f x⁻¹) (Set.Ioi c) μ

Tactic:
simpa using hf.comp_inv

Premises used: MeasureTheory.IntegrableOn.comp_inv
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulLeftInvariant
f : G → E
g : G
⊢ MeasurableEmbedding (β := G) fun (x : G) ↦ g * x

Tactic:
have h_mul : MeasurableEmbedding fun x => g * x := (MeasurableEquiv.mulLeft g).measurableEmbedding
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulLeftInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding (β := G) fun (x : G) ↦ g * x
rw : Eq.{u_5 + 1} (α := E) (@integral _ _ _ _ inst (map (fun (x : G) ↦ g * x) μ) fun (y : G) ↦ f y) (∫ (x : G), f x ∂μ)
rw₁ rw₂ : Eq.{u_5 + 1} (α := E) (∫ (y : G), f y ∂μ) (∫ (x : G), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (g * x) ∂μ) (∫ (x : G), f x ∂μ)

Tactic:
rw [← h_mul.integral_map, map_mul_left_eq_self]

Premises used: MeasureTheory.map_mul_left_eq_self, MeasurableEmbedding.integral_map
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
f : G → E
g : G
⊢ MeasurableEmbedding (β := G) fun (x : G) ↦ x * g

Tactic:
have h_mul : MeasurableEmbedding fun x => x * g :=
    (MeasurableEquiv.mulRight g).measurableEmbedding
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding (β := G) fun (x : G) ↦ x * g
rw : Eq.{u_5 + 1} (α := E) (@integral _ _ _ _ inst (map (fun (x : G) ↦ x * g) μ) fun (y : G) ↦ f y) (∫ (x : G), f x ∂μ)
rw₁ rw₂ : Eq.{u_5 + 1} (α := E) (∫ (y : G), f y ∂μ) (∫ (x : G), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x * g) ∂μ) (∫ (x : G), f x ∂μ)

Tactic:
rw [← h_mul.integral_map, map_mul_right_eq_self]

Premises used: MeasurableEmbedding.integral_map, MeasureTheory.map_mul_right_eq_self
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
f : G → E
g : G
simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x * g⁻¹) ∂μ) (∫ (x : G), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x / g) ∂μ) (∫ (x : G), f x ∂μ)

Tactic:
simp_rw [div_eq_mul_inv, integral_mul_right_eq_self f g⁻¹]

Premises used: MeasureTheory.integral_mul_right_eq_self, div_eq_mul_inv, Inv.inv
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
⊢ IsAddTorsionFree E

Tactic:
have : IsAddTorsionFree E := .of_isTorsionFree ℝ E
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
this : IsAddTorsionFree E
simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (-∫ (x : G), f x ∂μ)
simp_rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (∫ (a : G), -f a ∂μ)
simp_rw₂ : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (∫ (a : G), f (g * a) ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) 0

Tactic:
simp_rw [← self_eq_neg, ← integral_neg, ← hf', integral_mul_left_eq_self]

Premises used: MeasureTheory.integral_neg, self_eq_neg, MeasureTheory.integral_mul_left_eq_self
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
hf' : ∀ (x : G), f (x * g) = -f x
⊢ IsAddTorsionFree E

Tactic:
have : IsAddTorsionFree E := .of_isTorsionFree ℝ E
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : μ.IsMulRightInvariant
hf' : ∀ (x : G), f (x * g) = -f x
this : IsAddTorsionFree E
simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (-∫ (x : G), f x ∂μ)
simp_rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (∫ (a : G), -f a ∂μ)
simp_rw₂ : Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) (∫ (a : G), f (a * g) ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f x ∂μ) 0

Tactic:
simp_rw [← self_eq_neg, ← integral_neg, ← hf', integral_mul_right_eq_self]

Premises used: MeasureTheory.integral_mul_right_eq_self, MeasureTheory.integral_neg, self_eq_neg
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
f : G → F
inst_4 : μ.IsMulLeftInvariant
hf : Integrable f μ
g : G
⊢ Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g * t)) μ

Tactic:
(hf.mono_measure (map_mul_left_eq_self μ g).le).comp_measurable <| measurable_const_mul g

Premises used: MeasureTheory.Integrable.mono_measure, MeasureTheory.map_mul_left_eq_self, MeasureTheory.Integrable.comp_measurable, MeasurableMul.measurable_const_mul, Eq.le
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
f : G → F
inst_4 : μ.IsMulRightInvariant
hf : Integrable f μ
g : G
⊢ Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (t * g)) μ

Tactic:
(hf.mono_measure (map_mul_right_eq_self μ g).le).comp_measurable <| measurable_mul_const g

Premises used: MeasureTheory.Integrable.mono_measure, MeasureTheory.Integrable.comp_measurable, Eq.le, MeasurableMul.measurable_mul_const, MeasureTheory.map_mul_right_eq_self
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
f : G → F
inst_4 : μ.IsMulRightInvariant
hf : Integrable f μ
g : G
simp_rw : Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (t * g⁻¹)) μ
⊢ Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (t / g)) μ

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
f : G → F
inst_4 : μ.IsMulRightInvariant
hf : Integrable f μ
g : G
⊢ Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (t * g⁻¹)) μ

Tactic:
hf.comp_mul_right g⁻¹

Premises used: MeasureTheory.Integrable.comp_mul_right, Inv.inv
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
f : G → F
inst_4 : μ.IsMulRightInvariant
hf : Integrable f μ
g : G
⊢ Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (t * g⁻¹)) μ

Tactic:
exact hf.comp_mul_right g⁻¹

Premises used: MeasureTheory.Integrable.comp_mul_right, Inv.inv
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
f : G → F
inst_5 : μ.IsInvInvariant
inst_6 : μ.IsMulLeftInvariant
hf : Integrable f μ
g : G
⊢ Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g / t)) μ

Tactic:
((measurePreserving_div_left μ g).integrable_comp hf.aestronglyMeasurable).mpr hf

Premises used: Iff.mpr, MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.MeasurePreserving.integrable_comp, MeasureTheory.Measure.measurePreserving_div_left
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
f : G → F
inst_5 : μ.IsInvInvariant
inst_6 : μ.IsMulLeftInvariant
g : G
⊢ Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g / t)) μ ↔ Integrable f μ

Tactic:
⟨fun h => ?_, fun h => h.comp_div_left g⟩

Premises used: MeasureTheory.Integrable.comp_div_left, Iff.intro
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
f : G → F
inst_5 : μ.IsInvInvariant
inst_6 : μ.IsMulLeftInvariant
g : G
refine : ∀ (h : Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g / t)) μ), Integrable f μ
⊢ Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g / t)) μ ↔ Integrable f μ

Tactic:
refine ⟨fun h => ?_, fun h => h.comp_div_left g⟩
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
f : G → F
inst_5 : μ.IsInvInvariant
inst_6 : μ.IsMulLeftInvariant
g : G
h : Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g / t)) μ
⊢ Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g / (g⁻¹ * t)⁻¹)) μ

Tactic:
h.comp_inv.comp_mul_left g⁻¹

Premises used: Inv.inv, MeasureTheory.Integrable.comp_inv, MeasureTheory.Integrable.comp_mul_left
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
f : G → F
inst_5 : μ.IsInvInvariant
inst_6 : μ.IsMulLeftInvariant
g : G
h : Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g / t)) μ
h₁ : ∀ (x : G), x = g / (g⁻¹ * x)⁻¹
⊢ Integrable f μ

Tactic:
convert! h.comp_inv.comp_mul_left g⁻¹

Premises used: Inv.inv, MeasureTheory.Integrable.comp_inv, MeasureTheory.Integrable.comp_mul_left
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
F : Type u_6
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup F
μ : Measure G
inst_2 : Group G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
f : G → F
inst_5 : μ.IsInvInvariant
inst_6 : μ.IsMulLeftInvariant
g : G
h : Integrable.{u_6, u_4} (ε := F) (fun (t : G) ↦ f (g / t)) μ
x : G
h₁ : x = g * (g⁻¹ * x)
⊢ x = g / (g⁻¹ * x)⁻¹

Tactic:
simp_rw [div_inv_eq_mul, mul_inv_cancel_left]

Premises used: div_inv_eq_mul, mul_inv_cancel_left
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
G : Type u_4
E : Type u_5
inst : MeasurableSpace G
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : Group G
inst_4 : MeasurableMul G
inst_5 : MeasurableInv G
f : G → E
μ : Measure G
inst_6 : μ.IsInvInvariant
inst_7 : μ.IsMulLeftInvariant
x' : G
simp_rw : Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x' * x⁻¹) ∂μ) (∫ (x : G), f x ∂μ)
simp_rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x' * x) ∂μ) (∫ (x : G), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : G), f (x' / x) ∂μ) (∫ (x : G), f x ∂μ)

Tactic:
simp_rw [div_eq_mul_inv, integral_inv_eq_self (fun x => f (x' * x)) μ,
    integral_mul_left_eq_self f x']

Premises used: HMul.hMul, div_eq_mul_inv, MeasureTheory.integral_mul_left_eq_self, MeasureTheory.integral_inv_eq_self
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
α : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
G : Type u_7
inst_2 : Group G
inst_3 : MeasurableSpace α
inst_4 : MulAction G α
inst_5 : MeasurableConstSMul G α
μ : Measure α
inst_6 : SMulInvariantMeasure G α μ
f : α → E
g : G
⊢ MeasurableEmbedding (β := α) fun (x : α) ↦ g • x

Tactic:
have h : MeasurableEmbedding fun x : α => g • x := (MeasurableEquiv.smul g).measurableEmbedding
-- Module: Mathlib.MeasureTheory.Group.Integral
Goal:
α : Type u_3
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
G : Type u_7
inst_2 : Group G
inst_3 : MeasurableSpace α
inst_4 : MulAction G α
inst_5 : MeasurableConstSMul G α
μ : Measure α
inst_6 : SMulInvariantMeasure G α μ
f : α → E
g : G
h : MeasurableEmbedding (β := α) fun (x : α) ↦ g • x
rw :
  Eq.{u_5 + 1} (α := E) (@integral _ _ _ _ inst_3 (map (fun (x : α) ↦ g • x) μ) fun (y : α) ↦ f y) (∫ (x : α), f x ∂μ)
rw₁ rw₂ : Eq.{u_5 + 1} (α := E) (∫ (y : α), f y ∂μ) (∫ (x : α), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α), f (g • x) ∂μ) (∫ (x : α), f x ∂μ)

Tactic:
rw [← h.integral_map, MeasureTheory.map_smul]

Premises used: MeasureTheory.map_smul, MeasurableEmbedding.integral_map
-- Module: Mathlib.MeasureTheory.Group.IntegralConvolution
Goal:
M : Type u_1
F : Type u_2
inst : Monoid M
mM : MeasurableSpace M
inst_1 : MeasurableMul₂ M
inst_2 : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst_3 : SFinite ν
hf : AEStronglyMeasurable f (μ ∗ₘ ν)
⊢ AEMeasurable (β := M) (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.IntegralConvolution
Goal:
M : Type u_1
F : Type u_2
inst : Monoid M
mM : MeasurableSpace M
inst_1 : MeasurableMul₂ M
inst_2 : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst_3 : SFinite ν
hf : AEStronglyMeasurable f (μ ∗ₘ ν)
⊢ Measurable (β := M) fun (x : M × M) ↦ x.1 * x.2

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.IntegralConvolution
Goal:
M : Type u_1
F : Type u_2
inst : Monoid M
mM : MeasurableSpace M
inst_1 : MeasurableMul₂ M
inst_2 : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst_3 : SFinite ν
hf : AEStronglyMeasurable f (μ ∗ₘ ν)
⊢ Integrable f (μ ∗ₘ ν) ↔
    (∀ᵐ (x : M) ∂μ, Integrable.{u_2, u_1} (ε := F) (fun (y : M) ↦ f (x * y)) ν) ∧
      Integrable (ε := ℝ) (fun (x : M) ↦ ∫ (y : M), ‖f (x * y)‖ ∂ν) μ

Tactic:
simp [Measure.mconv, integrable_map_measure hf (by fun_prop),
    integrable_prod_iff (hf.comp_measurable (by fun_prop))]

Premises used: MeasureTheory.AEStronglyMeasurable.comp_measurable, MeasureTheory.integrable_prod_iff, MeasureTheory.integrable_map_measure, MeasureTheory.Measure.mconv
-- Module: Mathlib.MeasureTheory.Group.IntegralConvolution
Goal:
M : Type u_1
F : Type u_2
inst : Monoid M
mM : MeasurableSpace M
inst_1 : MeasurableMul₂ M
inst_2 : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst_3 : NormedSpace ℝ F
inst_4 : SFinite μ
inst_5 : SFinite ν
hf : Integrable f (μ ∗ₘ ν)
⊢ AEMeasurable (β := M) (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.IntegralConvolution
Goal:
M : Type u_1
F : Type u_2
inst : Monoid M
mM : MeasurableSpace M
inst_1 : MeasurableMul₂ M
inst_2 : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst_3 : NormedSpace ℝ F
inst_4 : SFinite μ
inst_5 : SFinite ν
hf : Integrable f (μ ∗ₘ ν)
hf₁ : Integrable.{u_2, u_1} (ε := F) (fun (x : M × M) ↦ f (x.1 * x.2)) (μ.prod ν)
⊢ Eq.{u_2 + 1} (α := F) (@integral _ _ _ _ mM (Measure.map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν)) fun (x : M) ↦ f x)
    (∫ (x : M), ∫ (y : M), f (x * y) ∂ν ∂μ)

Tactic:
rw [integral_map (by fun_prop) hf.1, integral_prod]

Premises used: MeasureTheory.integral_map, And.left, MeasureTheory.integral_prod
-- Module: Mathlib.MeasureTheory.Group.IntegralConvolution
Goal:
M : Type u_1
F : Type u_2
inst : Monoid M
mM : MeasurableSpace M
inst_1 : MeasurableMul₂ M
inst_2 : NormedAddCommGroup F
μ ν : Measure M
f : M → F
inst_3 : NormedSpace ℝ F
inst_4 : SFinite μ
inst_5 : SFinite ν
hf : Integrable f (μ ∗ₘ ν)
⊢ Integrable.{u_2, u_1} (ε := F) (fun (x : M × M) ↦ f (x.1 * x.2)) (μ.prod ν)

Tactic:
exact (integrable_map_measure hf.1 (by fun_prop)).mp hf

Premises used: And.left, Iff.mp, MeasureTheory.integrable_map_measure
-- Module: Mathlib.MeasureTheory.Group.LIntegral
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : InvolutiveInv G
inst_2 : MeasurableInv G
inst_3 : μ.IsInvInvariant
f : G → ℝ≥0∞
⊢ ∫⁻ (x : G), f x⁻¹ ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
simpa using (lintegral_map_equiv f (μ := μ) <| MeasurableEquiv.inv G).symm

Premises used: MeasurableEquiv.inv, Eq.symm, MeasureTheory.lintegral_map_equiv
-- Module: Mathlib.MeasureTheory.Group.LIntegral
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulLeftInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (a : G), f ((MeasurableEquiv.mulLeft g : (a : G) → G) a) ∂μ =
    ∫⁻ (a : G), f a ∂map (⇑(MeasurableEquiv.mulLeft g) : (a : G) → G) μ

Tactic:
(lintegral_map_equiv f <| MeasurableEquiv.mulLeft g).symm

Premises used: MeasurableEquiv.mulLeft, Eq.symm, MeasureTheory.lintegral_map_equiv
-- Module: Mathlib.MeasureTheory.Group.LIntegral
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulLeftInvariant
f : G → ℝ≥0∞
g : G
h : μ = map (⇑(MeasurableEquiv.mulLeft g) : (a : G) → G) μ
⊢ ∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
convert! (lintegral_map_equiv f <| MeasurableEquiv.mulLeft g).symm

Premises used: MeasurableEquiv.mulLeft, Eq.symm, MeasureTheory.lintegral_map_equiv
-- Module: Mathlib.MeasureTheory.Group.LIntegral
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulLeftInvariant
f : G → ℝ≥0∞
g : G
⊢ μ = map (⇑(MeasurableEquiv.mulLeft g) : (a : G) → G) μ

Tactic:
simp [map_mul_left_eq_self μ g]

Premises used: MeasureTheory.map_mul_left_eq_self
-- Module: Mathlib.MeasureTheory.Group.LIntegral
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (a : G), f ((MeasurableEquiv.mulRight g : (a : G) → G) a) ∂μ =
    ∫⁻ (a : G), f a ∂map (⇑(MeasurableEquiv.mulRight g) : (a : G) → G) μ

Tactic:
(lintegral_map_equiv f <| MeasurableEquiv.mulRight g).symm

Premises used: MeasurableEquiv.mulRight, Eq.symm, MeasureTheory.lintegral_map_equiv
-- Module: Mathlib.MeasureTheory.Group.LIntegral
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
h : ∫⁻ (x : G), f x ∂μ = ∫⁻ (a : G), f a ∂map (⇑(MeasurableEquiv.mulRight g) : (a : G) → G) μ
⊢ ∫⁻ (x : G), f (x * g) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
convert! (lintegral_map_equiv f <| MeasurableEquiv.mulRight g).symm using 1

Premises used: MeasurableEquiv.mulRight, Eq.symm, MeasureTheory.lintegral_map_equiv
-- Module: Mathlib.MeasureTheory.Group.LIntegral
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f x ∂μ = ∫⁻ (a : G), f a ∂map (⇑(MeasurableEquiv.mulRight g) : (a : G) → G) μ

Tactic:
simp [map_mul_right_eq_self μ g]

Premises used: MeasureTheory.map_mul_right_eq_self
-- Module: Mathlib.MeasureTheory.Group.LIntegral
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulRightInvariant
f : G → ℝ≥0∞
g : G
simp_rw : ∫⁻ (x : G), f (x * g⁻¹) ∂μ = ∫⁻ (x : G), f x ∂μ
⊢ ∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
simp_rw [div_eq_mul_inv, lintegral_mul_right_eq_self f g⁻¹]

Premises used: MeasureTheory.lintegral_mul_right_eq_self, div_eq_mul_inv, Inv.inv
-- Module: Mathlib.MeasureTheory.Group.LIntegral
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Group G
inst_2 : MeasurableMul G
inst_3 : μ.IsMulLeftInvariant
inst_4 : MeasurableInv G
inst_5 : μ.IsInvInvariant
f : G → ℝ≥0∞
g : G
simp_rw : ∫⁻ (x : G), f (g * x⁻¹) ∂μ = ∫⁻ (x : G), f x ∂μ
simp_rw₁ : ∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ
⊢ ∫⁻ (x : G), f (g / x) ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
simp_rw [div_eq_mul_inv, lintegral_inv_eq_self (f <| g * ·), lintegral_mul_left_eq_self]

Premises used: HMul.hMul, MeasureTheory.lintegral_inv_eq_self, div_eq_mul_inv, MeasureTheory.lintegral_mul_left_eq_self