awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ : Measure M
inst_3 : SFinite μ
x : M
⊢ Eq (α := Measure M) (map ((fun (x : M × M) ↦ x.1 * x.2) ∘ fun (x_1 : M) ↦ (x_1, x)) μ) (map (fun (y : M) ↦ y * x) μ)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
x y : M
⊢ Measurable (β := M) fun (y_1 : M) ↦ y_1 * y

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
x y : M
rw : Eq (α := Measure M) (map (fun (y_1 : M) ↦ y_1 * y) (dirac x)) (dirac (x * y))
rw₁ rw₂ : Eq (α := Measure M) (dirac (x * y)) (dirac (x * y))
⊢ Eq (α := Measure M) (dirac x ∗ₘ dirac y) (dirac (x * y))

Tactic:
rw [mconv_dirac, map_dirac' (by fun_prop)]

Premises used: MeasureTheory.Measure.map_dirac', MeasureTheory.Measure.mconv_dirac
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ : Measure M
inst_3 : SFinite μ
⊢ dirac 1 ∗ₘ μ = μ

Tactic:
simp [dirac_mconv]

Premises used: MeasureTheory.Measure.dirac_mconv
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ : Measure M
inst_3 : SFinite μ
⊢ μ ∗ₘ dirac 1 = μ

Tactic:
simp [mconv_dirac]

Premises used: MeasureTheory.Measure.mconv_dirac
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
μ : Measure M
⊢ Eq (α := Measure M) (map (fun (x : M × M) ↦ x.1 * x.2) (Measure.prod 0 μ)) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
μ : Measure M
⊢ Eq (α := Measure M) (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod 0)) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
μ ν : Measure M
inst_2 : SFinite ν
s : ℝ≥0∞
rw :
  Eq (α := Measure M) (map (fun (x : M × M) ↦ x.1 * x.2) ((s • μ).prod ν))
    (map (fun (x : M × M) ↦ x.1 * x.2) (s • μ.prod ν))
rw₁ rw₂ :
  Eq (α := Measure M) (map (fun (x : M × M) ↦ x.1 * x.2) (s • μ.prod ν))
    (map (fun (x : M × M) ↦ x.1 * x.2) (s • μ.prod ν))
⊢ map (fun (x : M × M) ↦ x.1 * x.2) ((s • μ).prod ν) =
    HSMul.hSMul (β := Measure M) s (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν))

Tactic:
rw [← Measure.map_smul, Measure.prod_smul_left]

Premises used: MeasureTheory.Measure.map_smul, MeasureTheory.Measure.prod_smul_left
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite μ
inst_4 : SFinite ν
inst_5 : SFinite ρ
hf : Measurable (β := M) fun (x : M × M) ↦ x.1 * x.2
⊢ map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod (ν + ρ)) =
    HAdd.hAdd (α := Measure M) (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν))
      (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ρ))

Tactic:
rw [prod_add, Measure.map_add]

Premises used: MeasureTheory.Measure.map_add, MeasureTheory.Measure.prod_add
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite μ
inst_4 : SFinite ν
inst_5 : SFinite ρ
⊢ Measurable (β := M) fun (x : M × M) ↦ x.1 * x.2

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite μ
inst_4 : SFinite ν
inst_5 : SFinite ρ
hf : Measurable (β := M) fun (x : M × M) ↦ x.1 * x.2
⊢ map (fun (x : M × M) ↦ x.1 * x.2) ((μ + ν).prod ρ) =
    HAdd.hAdd (α := Measure M) (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ρ))
      (map (fun (x : M × M) ↦ x.1 * x.2) (ν.prod ρ))

Tactic:
rw [add_prod, Measure.map_add]

Premises used: MeasureTheory.Measure.map_add, MeasureTheory.Measure.add_prod
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_2
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν : Measure M
inst_3 : SFinite μ
inst_4 : SFinite ν
⊢ Measurable (β := M) fun (x : M × M) ↦ x.1 * x.2

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_2
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν : Measure M
inst_3 : SFinite μ
inst_4 : SFinite ν
rw :
  Eq (α := Measure M) (map ((fun (x : M × M) ↦ x.1 * x.2) ∘ Prod.swap) (ν.prod μ))
    (map (fun (x : M × M) ↦ x.1 * x.2) (ν.prod μ))
rw₁ : Measurable.{u_2, u_2} (α := M × M) Prod.swap
⊢ Eq (α := Measure M) (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν)) (map (fun (x : M × M) ↦ x.1 * x.2) (ν.prod μ))

Tactic:
rw [← prod_swap, map_map (by fun_prop)]

Premises used: MeasureTheory.Measure.prod_swap, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_2
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν : Measure M
inst_3 : SFinite μ
inst_4 : SFinite ν
⊢ Eq (α := Measure M) (map ((fun (x : M × M) ↦ x.1 * x.2) ∘ Prod.swap) (ν.prod μ))
    (map (fun (x : M × M) ↦ x.1 * x.2) (ν.prod μ))

Tactic:
simp [Function.comp_def, mul_comm]

Premises used: Function.comp_def, mul_comm
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_2
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν : Measure M
inst_3 : SFinite μ
inst_4 : SFinite ν
⊢ Measurable.{u_2, u_2} (α := M × M) Prod.swap

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
μ ν : Measure M
inst_2 : SFinite μ
inst_3 : SFinite ν
⊢ SFinite (μ ∗ₘ ν)

Tactic:
inferInstanceAs <| SFinite ((μ.prod ν).map fun (x : M × M) ↦ x.1 * x.2)

Premises used: _private.0.MeasureTheory.Measure.sfinite_mconv_of_sfinite._proof_1
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
μ ν : Measure M
inst_2 : IsFiniteMeasure μ
inst_3 : IsFiniteMeasure ν
⊢ LT.lt (α := ℝ≥0∞) (((map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν) : Measure M) : (a : Set M) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
IsFiniteMeasure.measure_univ_lt_top

Premises used: MeasureTheory.IsFiniteMeasure.measure_univ_lt_top
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
μ ν : Measure M
inst_2 : IsFiniteMeasure μ
inst_3 : IsFiniteMeasure ν
⊢ LT.lt (α := ℝ≥0∞) (((map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν) : Measure M) : (a : Set M) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact IsFiniteMeasure.measure_univ_lt_top

Premises used: MeasureTheory.IsFiniteMeasure.measure_univ_lt_top
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
μ ν : Measure M
inst_2 : IsFiniteMeasure μ
inst_3 : IsFiniteMeasure ν
⊢ LT.lt (α := ℝ≥0∞) ((μ ∗ₘ ν : (a : Set M) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have h : (μ ∗ₘ ν) Set.univ < ⊤ := by
    unfold mconv
    exact IsFiniteMeasure.measure_univ_lt_top
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
μ ν : Measure M
inst_2 : IsFiniteMeasure μ
inst_3 : IsFiniteMeasure ν
h : LT.lt (α := ℝ≥0∞) ((μ ∗ₘ ν : (a : Set M) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure (μ ∗ₘ ν)

Tactic:
{ measure_univ_lt_top := h }

Premises used: MeasureTheory.IsFiniteMeasure.mk
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
μ ν : Measure M
inst_2 : IsFiniteMeasure μ
inst_3 : IsFiniteMeasure ν
h : LT.lt (α := ℝ≥0∞) ((μ ∗ₘ ν : (a : Set M) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure (μ ∗ₘ ν)

Tactic:
exact { measure_univ_lt_top := h }
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
⊢ (μ ∗ₘ ν) ∗ₘ ρ = μ ∗ₘ ν ∗ₘ ρ

Tactic:
ext_of_lintegral _ fun f hf ↦ ?_

Premises used: MeasureTheory.Measure.ext_of_lintegral
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
refine : ∀ (f : M → ℝ≥0∞) (hf : Measurable f), ∫⁻ (a : M), f a ∂(μ ∗ₘ ν) ∗ₘ ρ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ
⊢ (μ ∗ₘ ν) ∗ₘ ρ = μ ∗ₘ ν ∗ₘ ρ

Tactic:
refine ext_of_lintegral _ fun f hf ↦ ?_

Premises used: MeasureTheory.Measure.ext_of_lintegral
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ Measurable f

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
rw : ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ρ ∂μ ∗ₘ ν = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ
⊢ ∫⁻ (a : M), f a ∂(μ ∗ₘ ν) ∗ₘ ρ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ

Tactic:
rw [lintegral_mconv (by fun_prop)]

Premises used: MeasureTheory.Measure.lintegral_mconv
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (x : M) ↦ ∫⁻ (y : M), f (x * y) ∂ρ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
rw : ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ
⊢ ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ρ ∂μ ∗ₘ ν = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ

Tactic:
rw [lintegral_mconv (by fun_prop)]

Premises used: MeasureTheory.Measure.lintegral_mconv
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
rw : ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ ∂μ
⊢ ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ

Tactic:
rw [lintegral_mconv (by fun_prop)]

Premises used: MeasureTheory.Measure.lintegral_mconv
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
repeat : ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ ∂μ
⊢ ∫⁻ (a : M), f a ∂(μ ∗ₘ ν) ∗ₘ ρ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ

Tactic:
repeat rw [lintegral_mconv (by fun_prop)]

Premises used: MeasureTheory.Measure.lintegral_mconv
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ ∂μ

Tactic:
lintegral_congr fun x ↦ ?_

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
refine : ∀ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν = ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ
⊢ ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ ∂μ

Tactic:
refine lintegral_congr fun x ↦ ?_

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x : M
⊢ Measurable (β := ℝ≥0∞) fun (y : M) ↦ f (x * y)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x : M
rw : ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν = ∫⁻ (x_1 : M), ∫⁻ (y : M), f (x * (x_1 * y)) ∂ρ ∂ν
⊢ ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν = ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ

Tactic:
rw [lintegral_mconv (by fun_prop)]

Premises used: MeasureTheory.Measure.lintegral_mconv
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x : M
⊢ ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν = ∫⁻ (x_1 : M), ∫⁻ (y : M), f (x * (x_1 * y)) ∂ρ ∂ν

Tactic:
lintegral_congr fun x ↦ ?_

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x : M
refine : ∀ (x_1 : M), ∫⁻ (y : M), f (x * x_1 * y) ∂ρ = ∫⁻ (y : M), f (x * (x_1 * y)) ∂ρ
⊢ ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν = ∫⁻ (x_1 : M), ∫⁻ (y : M), f (x * (x_1 * y)) ∂ρ ∂ν

Tactic:
refine lintegral_congr fun x ↦ ?_

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x_1 x : M
⊢ ∫⁻ (y : M), f (x_1 * x * y) ∂ρ = ∫⁻ (y : M), f (x_1 * (x * y)) ∂ρ

Tactic:
lintegral_congr fun x ↦ ?_

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x_1 x : M
refine : ∀ (x_2 : M), f (x_1 * x * x_2) = f (x_1 * (x * x_2))
⊢ ∫⁻ (y : M), f (x_1 * x * y) ∂ρ = ∫⁻ (y : M), f (x_1 * (x * y)) ∂ρ

Tactic:
refine lintegral_congr fun x ↦ ?_

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x : M
repeat : ∀ (x_1 x_2 : M), f (x * x_1 * x_2) = f (x * (x_1 * x_2))
⊢ ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν = ∫⁻ (x_1 : M), ∫⁻ (y : M), f (x * (x_1 * y)) ∂ρ ∂ν

Tactic:
repeat refine lintegral_congr fun x ↦ ?_

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x_1 x_2 x : M
⊢ f (x_1 * x_2 * x) = f (x_1 * (x_2 * x))

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
μ ν : Measure M
inst_2 : MeasurableMul₂ M
inst_3 : IsProbabilityMeasure μ
inst_4 : IsProbabilityMeasure ν
⊢ AEMeasurable (β := M) (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
⊢ μ ∗ₘ ν ≪ ρ

Tactic:
AbsolutelyContinuous.mk (fun s hs h ↦ ?_)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
refine :
  ∀ (s : Set M) (hs : MeasurableSet s) (h : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ ∗ₘ ν : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ∗ₘ ν ≪ ρ

Tactic:
refine AbsolutelyContinuous.mk (fun s hs h ↦ ?_)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) (s.indicator 1)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : ∫⁻ (x : M), ∫⁻ (y : M), s.indicator 1 (x * y) ∂ν ∂μ = 0
⊢ Eq (α := ℝ≥0∞) ((μ ∗ₘ ν : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← lintegral_indicator_one hs, lintegral_mconv (by measurability)]

Premises used: MeasureTheory.Measure.lintegral_mconv, MeasureTheory.lintegral_indicator_one
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
simp : ∫⁻ (x : M), ∫⁻ (y : M), Set.indicator (HMul.hMul x ⁻¹' s) 1 y ∂ν ∂μ = 0
⊢ ∫⁻ (x : M), ∫⁻ (y : M), s.indicator 1 ((fun (y : M) ↦ x * y) y) ∂ν ∂μ = 0

Tactic:
simp only [← Set.indicator_comp_right, Pi.one_comp]

Premises used: Pi.one_comp, Set.indicator_comp_right
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : M
⊢ Measurable (α := M) (HMul.hMul x)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : M
⊢ MeasurableSet (α := M) (HMul.hMul x ⁻¹' s)

Tactic:
apply MeasurableSet.preimage hs (by fun_prop)

Premises used: MeasurableSet.preimage
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : M
rw : ((ν : (a : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) : ℝ≥0∞)
| ∫⁻ (y : M), Set.indicator (HMul.hMul x ⁻¹' s) 1 y ∂ν

Tactic:
rw [lintegral_indicator_one (by apply MeasurableSet.preimage hs (by fun_prop))]

Premises used: MeasureTheory.lintegral_indicator_one
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
conv : ∫⁻ (x : M), (ν : (a : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) ∂μ = 0
⊢ ∫⁻ (x : M), ∫⁻ (y : M), Set.indicator (HMul.hMul x ⁻¹' s) 1 y ∂ν ∂μ = 0

Tactic:
conv in ∫⁻ _, _ ∂ν =>
    rw [lintegral_indicator_one (by apply MeasurableSet.preimage hs (by fun_prop))]

Premises used: MeasureTheory.lintegral_indicator_one
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : M
a : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply hν
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : M
a : Eq (α := ℝ≥0∞) (((map (HMul.hMul x) ρ : Measure M) : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
a₁ : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
a₂ a₃ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

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

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.IsMulLeftInvariant.map_mul_left_eq_self
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (x : M), Eq (α := ℝ≥0∞) ((ν : (a : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have h0 (x : M) : ν (HMul.hMul x ⁻¹' s) = 0 := by
    apply hν
    rw [← map_apply (by fun_prop) hs, IsMulLeftInvariant.map_mul_left_eq_self, h]
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : ρ.IsMulLeftInvariant
inst_4 : SFinite ν
hν : ν ≪ ρ
s : Set M
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h0 : ∀ (x : M), Eq (α := ℝ≥0∞) ((ν : (a : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (x : M), (ν : (a : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) ∂μ = 0

Tactic:
simp [h0]
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst : Monoid M
inst_1 : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst_2 : Monoid M'
inst_3 : MeasurableMul₂ M'
μ ν : Measure M
inst_4 : SFinite μ
inst_5 : SFinite ν
L : M →* M'
hL : Measurable.{u_2, u_3} (α := M) (β := M') (⇑L : (a : M) → M')
⊢ Measurable.{u_2, u_3} (α := M) (β := M') (⇑L : (a : M) → M')

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst : Monoid M
inst_1 : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst_2 : Monoid M'
inst_3 : MeasurableMul₂ M'
μ ν : Measure M
inst_4 : SFinite μ
inst_5 : SFinite ν
L : M →* M'
hL : Measurable.{u_2, u_3} (α := M) (β := M') (⇑L : (a : M) → M')
⊢ Measurable (β := M) fun (x : M × M) ↦ x.1 * x.2

Tactic:
fun_prop