awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl : ∀ f ∈ l, AEMeasurable f μ
nil :
  ∀ (hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → AEMeasurable f μ),
    AEMeasurable.{u_3, u_2} (β := M) (prod []) μ
⊢ AEMeasurable l.prod μ
have cons : ∀ (f : α → M) (l : List (α → M)) (ihl : ∀ (hl : ∀ f ∈ l, AEMeasurable f μ), AEMeasurable l.prod μ)
  (hl : ∀ f_1 ∈ f :: l, AEMeasurable f_1 μ), AEMeasurable (f :: l).prod μ
Tactic: induction l with
  | nil => exact aemeasurable_one
  | cons f l ihl =>
    rw [List.forall_mem_cons] at hl
    rw [List.prod_cons]
    exact hl.1.mul (ihl hl.2)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
M : Type u_2
α : Type u_4
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
l : Multiset (α → M)
hl : ∀ f ∈ l, Measurable f
⊢ Measurable l.prod
have mk : ∀ (l : List (α → M))
  (hl :
    ∀ (f : α → M),
      Membership.mem (γ := Multiset (α → M)) (Quot.mk (⇑(List.isSetoid (α → M)) : List (α → M) → List (α → M) → Prop) l)
          f →
        Measurable f),
  Measurable (prod (Quot.mk (⇑(List.isSetoid (α → M)) : List (α → M) → List (α → M) → Prop) l))
Tactic: rcases l with ⟨l⟩
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
M : Type u_2
α : Type u_4
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : Multiset (α → M)
hl : ∀ f ∈ l, AEMeasurable f μ
⊢ AEMeasurable l.prod μ
have mk : ∀ (l : List (α → M))
  (hl :
    ∀ (f : α → M),
      Membership.mem (γ := Multiset (α → M)) (Quot.mk (⇑(List.isSetoid (α → M)) : List (α → M) → List (α → M) → Prop) l)
          f →
        AEMeasurable f μ),
  AEMeasurable (prod (Quot.mk (⇑(List.isSetoid (α → M)) : List (α → M) → List (α → M) → Prop) l)) μ
Tactic: rcases l with ⟨l⟩
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
M : Type u_2
ι : Type u_3
α : Type u_4
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable.{u_4, u_2} (β := M) fun (a : α) ↦ ∏ i ∈ s, f i a
have simp_rw : Measurable.{u_4, u_2} (β := M) fun (a : α) ↦ (∏ c ∈ s, f c) a
Tactic: simp_rw [← Finset.prod_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
M : Type u_2
ι : Type u_3
α : Type u_4
β : Type u_5
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
mβ : MeasurableSpace β
f : ι → α → β → M
g : α → β
s : Finset ι
hf : ∀ i ∈ s, Measurable ↿(f i)
hg : Measurable g
⊢ Measurable.{u_4, u_2} (β := M) fun (a : α) ↦ (∏ i ∈ s, f i a) (g a)
have simp : Measurable.{u_4, u_2} (β := M) fun (a : α) ↦ ∏ c ∈ s, f c a (g a)
Tactic: simp only [prod_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
M : Type u_2
ι : Type u_3
α : Type u_4
β : Type u_5
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
mβ : MeasurableSpace β
f : ι → α → β → M
g : α → β
s : Finset ι
hf : ∀ i ∈ s, Measurable ↿(f i)
hg : Measurable g
⊢ Measurable.{u_4, u_2} (β := M) fun (a : α) ↦ ∏ c ∈ s, f c a (g a)
have funProp : ∀ i ∈ s, i ∈ s
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν : Measure M
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (z : M), f z ∂μ ∗ₘ ν = ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν
have rw : ∫⁻ (z : M), f z ∂map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν) = ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν
Tactic: rw [mconv, lintegral_map hf measurable_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν : Measure M
f : M → ℝ≥0∞
hf : Measurable f
rw : ∫⁻ (z : M), f z ∂map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν) = ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν
⊢ ∫⁻ (z : M), f z ∂μ ∗ₘ ν = ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν
have rw₁ : ∫⁻ (a : M × M), f (a.1 * a.2) ∂μ.prod ν = ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν
Tactic: rw [mconv, lintegral_map hf measurable_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν : Measure M
inst_3 : SFinite ν
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (z : M), f z ∂μ ∗ₘ ν = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∂μ
have rw : ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∂μ
Tactic: rw [lintegral_mconv_eq_lintegral_prod hf, lintegral_prod _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν : Measure M
inst_3 : SFinite ν
f : M → ℝ≥0∞
hf : Measurable f
rw : ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∂μ
⊢ ∫⁻ (z : M), f z ∂μ ∗ₘ ν = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∂μ
have rw₁ : ∫⁻ (x : M), ∫⁻ (y : M), f ((x, y).1 * (x, y).2) ∂ν ∂μ = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∂μ
Tactic: rw [lintegral_mconv_eq_lintegral_prod hf, lintegral_prod _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
x : M
μ : Measure M
inst_3 : SFinite μ
⊢ Eq (α := Measure M) (map (fun (x : M × M) ↦ x.1 * x.2) (Measure.prod (dirac x) μ)) (map (fun (y : M) ↦ x * y) μ)
have rw : Eq (α := Measure M) (map ((fun (x : M × M) ↦ x.1 * x.2) ∘ Prod.mk x) μ) (map (fun (y : M) ↦ x * y) μ)
Tactic: rw [dirac_prod, map_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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) (μ.prod (dirac x))) (map (fun (y : M) ↦ y * x) μ)
have rw : 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: rw [prod_dirac, map_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
x y : M
⊢ Eq (α := Measure M) (dirac x ∗ₘ dirac y) (dirac (x * y))
have rw : Eq (α := Measure M) (map (fun (y_1 : M) ↦ y_1 * y) (dirac x)) (dirac (x * y))
Tactic: rw [mconv_dirac, map_dirac' (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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))
⊢ Eq (α := Measure M) (dirac x ∗ₘ dirac y) (dirac (x * y))
have rw₁ : Eq (α := Measure M) (dirac (x * y)) (dirac (x * y))
Tactic: rw [mconv_dirac, map_dirac' (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
μ ν : Measure M
inst_2 : SFinite ν
s : ℝ≥0∞
⊢ 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 ν))
have 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 ν))
Tactic: rw [← Measure.map_smul, Measure.prod_smul_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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 ν))
⊢ 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 ν))
have 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 ν))
Tactic: rw [← Measure.map_smul, Measure.prod_smul_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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 ρ
⊢ 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 ρ))
have hf : Measurable (β := M) fun (x : M × M) ↦ x.1 * x.2
Tactic: rw [prod_add, Measure.map_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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 ρ
⊢ 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 ρ))
have hf : Measurable (β := M) fun (x : M × M) ↦ x.1 * x.2
Tactic: rw [add_prod, Measure.map_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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 ν)) (map (fun (x : M × M) ↦ x.1 * x.2) (ν.prod μ))
have 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 μ))
Tactic: rw [← prod_swap, map_map (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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 μ))
⊢ Eq (α := Measure M) (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν)) (map (fun (x : M × M) ↦ x.1 * x.2) (ν.prod μ))
have rw₁ : Measurable.{u_2, u_2} (α := M × M) Prod.swap
Tactic: rw [← prod_swap, map_map (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (hypothesis)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
μ ν : Measure M
inst_2 : IsFiniteMeasure μ
inst_3 : IsFiniteMeasure ν
⊢ IsFiniteMeasure (μ ∗ₘ ν)
have h : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
μ ν ρ : Measure M
inst_3 : SFinite ν
inst_4 : SFinite ρ
⊢ (μ ∗ₘ ν) ∗ₘ ρ = μ ∗ₘ ν ∗ₘ ρ
have refine : ∀ (f : M → ℝ≥0∞) (hf : Measurable f), ∫⁻ (a : M), f a ∂(μ ∗ₘ ν) ∗ₘ ρ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ
Tactic: refine ext_of_lintegral _ fun f hf ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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
⊢ ∫⁻ (a : M), f a ∂(μ ∗ₘ ν) ∗ₘ ρ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ
have rw : ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ρ ∂μ ∗ₘ ν = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ
Tactic: rw [lintegral_mconv (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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), f (x * y) ∂ρ ∂μ ∗ₘ ν = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ
have rw : ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ
Tactic: rw [lintegral_mconv (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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) ∂ρ ∂ν ∂μ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ
have rw : ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ ∂μ
Tactic: rw [lintegral_mconv (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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
⊢ ∫⁻ (a : M), f a ∂(μ ∗ₘ ν) ∗ₘ ρ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ
have repeat : ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ ∂μ
Tactic: repeat rw [lintegral_mconv (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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) ∂ν ∗ₘ ρ ∂μ
have refine : ∀ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν = ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ
Tactic: refine lintegral_congr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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) ∂ρ ∂ν = ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ
have rw : ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν = ∫⁻ (x_1 : M), ∫⁻ (y : M), f (x * (x_1 * y)) ∂ρ ∂ν
Tactic: rw [lintegral_mconv (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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)) ∂ρ ∂ν
have refine : ∀ (x_1 : M), ∫⁻ (y : M), f (x * x_1 * y) ∂ρ = ∫⁻ (y : M), f (x * (x_1 * y)) ∂ρ
Tactic: refine lintegral_congr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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)) ∂ρ
have refine : ∀ (x_2 : M), f (x_1 * x * x_2) = f (x_1 * (x * x_2))
Tactic: refine lintegral_congr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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)) ∂ρ ∂ν
have repeat : ∀ (x_1 x_2 : M), f (x * x_1 * x_2) = f (x * (x_1 * x_2))
Tactic: repeat refine lintegral_congr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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ν : ν ≪ ρ
⊢ μ ∗ₘ ν ≪ ρ
have 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 ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ ∗ₘ ν : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : ∫⁻ (x : M), ∫⁻ (y : M), s.indicator 1 (x * y) ∂ν ∂μ = 0
Tactic: rw [← lintegral_indicator_one hs, lintegral_mconv (by measurability)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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), ∫⁻ (y : M), s.indicator 1 ((fun (y : M) ↦ x * y) y) ∂ν ∂μ = 0
have simp : ∫⁻ (x : M), ∫⁻ (y : M), Set.indicator (HMul.hMul x ⁻¹' s) 1 y ∂ν ∂μ = 0
Tactic: simp only [← Set.indicator_comp_right, Pi.one_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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
| ∫⁻ (y : M), Set.indicator (HMul.hMul x ⁻¹' s) 1 y ∂ν
have rw : ((ν : (a : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) : ℝ≥0∞)
Tactic: rw [lintegral_indicator_one (by apply MeasurableSet.preimage hs (by fun_prop))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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), ∫⁻ (y : M), Set.indicator (HMul.hMul x ⁻¹' s) 1 y ∂ν ∂μ = 0
have conv : ∫⁻ (x : M), (ν : (a : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) ∂μ = 0
Tactic: conv in ∫⁻ _, _ ∂ν =>
    rw [lintegral_indicator_one (by apply MeasurableSet.preimage hs (by fun_prop))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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∞)
have a : Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply hν
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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∞)
have a : Eq (α := ℝ≥0∞) (((map (HMul.hMul x) ρ : Measure M) : (a : Set M) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← map_apply (by fun_prop) hs, IsMulLeftInvariant.map_mul_left_eq_self, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have a₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [← map_apply (by fun_prop) hs, IsMulLeftInvariant.map_mul_left_eq_self, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (hypothesis)
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 : Set M) → ℝ≥0∞) (HMul.hMul x ⁻¹' s) ∂μ = 0
have h0 : ∀ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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')
⊢ Eq.{u_3 + 1} (α := Measure M') (map (α := M) (⇑L : (a : M) → M') (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν)))
    (map (fun (x : M' × M') ↦ x.1 * x.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
have rw : Eq.{u_3 + 1} (α := Measure M') (map (Function.comp (β := M) (⇑L : (a : M) → M') fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν))
  (map (fun (x : M' × M') ↦ x.1 * x.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
Tactic: rw [map_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
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')
⊢ Eq (α := M × M → M') (Function.comp (β := M) (⇑L : (a : M) → M') fun (p : M × M) ↦ p.1 * p.2)
    ((fun (p : M' × M') ↦ p.1 * p.2) ∘ Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M'))
have h : ∀ (x : M × M),
  Eq.{u_3 + 1} (α := M') (Function.comp (β := M) (⇑L : (a : M) → M') (fun (p : M × M) ↦ p.1 * p.2) x)
    (((fun (p : M' × M') ↦ p.1 * p.2) ∘ Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M')) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (hypothesis)
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')
⊢ Eq.{u_3 + 1} (α := Measure M')
    (map (Function.comp (β := M) (⇑L : (a : M) → M') fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν))
    (map (fun (x : M' × M') ↦ x.1 * x.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
have this : Eq (α := M × M → M') (Function.comp (β := M) (⇑L : (a : M) → M') fun (p : M × M) ↦ p.1 * p.2)
  ((fun (p : M' × M') ↦ p.1 * p.2) ∘ Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M'))
Tactic: have : (L ∘ fun p : M × M ↦ p.1 * p.2) = (fun p : M' × M' ↦ p.1 * p.2) ∘ (Prod.map L L) := by
    ext; simp