awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G₀ : Type u_3
β : Type u_5
α : Type u_6
inst : MeasurableSpace β
inst_1 : MeasurableSpace α
f : α → β
μ : Measure α
inst_2 : GroupWithZero G₀
inst_3 : MulAction G₀ β
inst_4 : MeasurableConstSMul G₀ β
c : G₀
hc : c ≠ 0
⊢ AEMeasurable.{u_6, u_5} (β := β) (fun (x : α) ↦ c • f x) μ ↔ AEMeasurable f μ

Tactic:
(IsUnit.mk0 c hc).aemeasurable_const_smul_iff

Premises used: IsUnit.aemeasurable_const_smul_iff, IsUnit.mk0
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_2
inst : MeasurableSpace α
⊢ Measurable.{u_2, u_2} (α := α) op

Tactic:
fun _ =>
  id

Premises used: MeasurableSet, MulOpposite, Measurable, setOf, id, Set.preimage
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_2
inst : MeasurableSpace α
⊢ Measurable.{u_2, u_2} (α := αᵐᵒᵖ) unop

Tactic:
fun _ => id

Premises used: MeasurableSet, Set.Mem, MulOpposite, Measurable, setOf, id, Set.preimage, MulOpposite.unop
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
M : Type u_2
inst : Mul M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul M
⊢ MeasurableMul.{u_2} Mᵐᵒᵖ

Tactic:
⟨fun _ => measurable_mul_op.comp (measurable_mul_unop.mul_const _), fun _ =>
    measurable_mul_op.comp (measurable_mul_unop.const_mul _)⟩

Premises used: measurable_mul_op, Measurable.comp, MeasurableMul.mk, MulOpposite.unop, Measurable.const_mul, Measurable.mul_const, measurable_mul_unop
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
M : Type u_2
inst : Mul M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
⊢ MeasurableMul₂.{u_2} Mᵐᵒᵖ

Tactic:
⟨measurable_mul_op.comp
      ((measurable_mul_unop.comp measurable_snd).mul (measurable_mul_unop.comp measurable_fst))⟩

Premises used: Measurable.mul, measurable_mul_op, Measurable.comp, measurable_snd, MeasurableMul₂.mk, measurable_fst, measurable_mul_unop
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M : Type u_2
α : Type u_3
inst : MeasurableSpace M
inst_1 : MeasurableSpace α
inst_2 : SMul M α
inst_3 : SMul.{u_2, u_3} Mᵐᵒᵖ α
inst_4 : IsCentralScalar M α
inst_5 : MeasurableSMul M α
x : α
⊢ Measurable.{u_2, u_3} (β := α) fun (c : Mᵐᵒᵖ) ↦ MulOpposite.op (unop c) • x

Tactic:
simpa only [op_smul_eq_smul] using (measurable_smul_const x).comp measurable_mul_unop

Premises used: Measurable.comp, MeasurableSMul.measurable_smul_const, IsCentralScalar.op_smul_eq_smul, measurable_mul_unop
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M : Type u_2
α : Type u_3
inst : MeasurableSpace M
inst_1 : MeasurableSpace α
inst_2 : SMul M α
inst_3 : SMul.{u_2, u_3} Mᵐᵒᵖ α
inst_4 : IsCentralScalar M α
inst_5 : MeasurableSMul₂ M α
simp_rw : Measurable (β := α) fun (x : Prod.{u_2, u_3} Mᵐᵒᵖ α) ↦ unop x.1 • x.2
⊢ Measurable (β := α) fun (x : Prod.{u_2, u_3} Mᵐᵒᵖ α) ↦ MulOpposite.op (unop x.1) • x.2

Tactic:
simp_rw [op_smul_eq_smul]

Premises used: IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M : Type u_2
α : Type u_3
inst : MeasurableSpace M
inst_1 : MeasurableSpace α
inst_2 : SMul M α
inst_3 : SMul.{u_2, u_3} Mᵐᵒᵖ α
inst_4 : IsCentralScalar M α
inst_5 : MeasurableSMul₂ M α
⊢ Measurable (β := α) fun (x : Prod.{u_2, u_3} Mᵐᵒᵖ α) ↦ unop x.1 • x.2

Tactic:
(measurable_mul_unop.comp measurable_fst).smul measurable_snd

Premises used: Measurable.comp, measurable_snd, Measurable.smul, measurable_fst, measurable_mul_unop
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M : Type u_2
α : Type u_3
inst : MeasurableSpace M
inst_1 : MeasurableSpace α
inst_2 : SMul M α
inst_3 : SMul.{u_2, u_3} Mᵐᵒᵖ α
inst_4 : IsCentralScalar M α
inst_5 : MeasurableSMul₂ M α
⊢ Measurable (β := α) fun (x : Prod.{u_2, u_3} Mᵐᵒᵖ α) ↦ unop x.1 • x.2

Tactic:
exact (measurable_mul_unop.comp measurable_fst).smul measurable_snd

Premises used: Measurable.comp, measurable_snd, Measurable.smul, measurable_fst, measurable_mul_unop
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
M : Type u_2
inst : Mul M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
⊢ MeasurableSMul₂ Mᵐᵒᵖ M

Tactic:
⟨measurable_snd.mul (measurable_mul_unop.comp measurable_fst)⟩

Premises used: Measurable.mul, Measurable.comp, measurable_snd, MeasurableSMul₂.mk, measurable_fst, measurable_mul_unop
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → Measurable f
⊢ Measurable.{u_3, u_2} (α := α) (β := M) (prod [])

Tactic:
measurable_one

Premises used: measurable_one, List.foldr, List.prod
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → Measurable f
⊢ Measurable.{u_3, u_2} (α := α) (β := M) (prod [])

Tactic:
exact measurable_one

Premises used: measurable_one
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, Measurable f), Measurable l.prod
hl : ∀ f_1 ∈ f :: l, Measurable f_1
⊢ Measurable f ∧ ∀ x ∈ l, Measurable x

Tactic:
rw [List.forall_mem_cons] at hl

Premises used: List.forall_mem_cons
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, Measurable f), Measurable l.prod
hl : Measurable f ∧ ∀ x ∈ l, Measurable x
cons : Measurable (f * l.prod)
⊢ Measurable (f :: l).prod

Tactic:
rw [List.prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, Measurable f), Measurable l.prod
hl : Measurable f ∧ ∀ x ∈ l, Measurable x
⊢ Measurable (f * l.prod)

Tactic:
hl.1.mul (ihl hl.2)

Premises used: Measurable.mul, And.right, And.left
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, Measurable f), Measurable l.prod
hl : Measurable f ∧ ∀ x ∈ l, Measurable x
⊢ Measurable (f * l.prod)

Tactic:
exact hl.1.mul (ihl hl.2)

Premises used: Measurable.mul, And.right, And.left
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, Measurable f
nil :
  ∀ (hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → Measurable f),
    Measurable.{u_3, u_2} (α := α) (β := M) (prod [])
cons :
  ∀ (f : α → M) (l : List (α → M)) (ihl : ∀ (hl : ∀ f ∈ l, Measurable f), Measurable l.prod)
    (hl : ∀ f_1 ∈ f :: l, Measurable f_1), Measurable (f :: l).prod
⊢ Measurable l.prod

Tactic:
induction l with
  | nil => exact measurable_one
  | cons f l ihl =>
    rw [List.forall_mem_cons] at hl
    rw [List.prod_cons]
    exact hl.1.mul (ihl hl.2)

Premises used: List.cons, measurable_one, List.forall_mem_cons, List.prod_cons, List.nil
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → AEMeasurable f μ
⊢ AEMeasurable.{u_3, u_2} (β := M) (prod []) μ

Tactic:
aemeasurable_one

Premises used: aemeasurable_one, List.foldr, List.prod
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → AEMeasurable f μ
⊢ AEMeasurable.{u_3, u_2} (β := M) (prod []) μ

Tactic:
exact aemeasurable_one

Premises used: aemeasurable_one
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, AEMeasurable f μ), AEMeasurable l.prod μ
hl : ∀ f_1 ∈ f :: l, AEMeasurable f_1 μ
⊢ AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ

Tactic:
rw [List.forall_mem_cons] at hl

Premises used: List.forall_mem_cons
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, AEMeasurable f μ), AEMeasurable l.prod μ
hl : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ
cons : AEMeasurable (f * l.prod) μ
⊢ AEMeasurable (f :: l).prod μ

Tactic:
rw [List.prod_cons]

Premises used: List.prod_cons
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, AEMeasurable f μ), AEMeasurable l.prod μ
hl : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ
⊢ AEMeasurable (f * l.prod) μ

Tactic:
hl.1.mul (ihl hl.2)

Premises used: AEMeasurable.mul, And.right, And.left
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, AEMeasurable f μ), AEMeasurable l.prod μ
hl : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ
⊢ AEMeasurable (f * l.prod) μ

Tactic:
exact hl.1.mul (ihl hl.2)

Premises used: AEMeasurable.mul, And.right, And.left
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
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 []) μ
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 μ
⊢ AEMeasurable 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)

Premises used: List.cons, List.forall_mem_cons, aemeasurable_one, List.prod_cons, List.nil
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, Measurable f
⊢ Measurable.{u_3, u_2} (β := M) fun (x : α) ↦ prod (map (fun (f : α → M) ↦ f x) l)

Tactic:
simpa only [← Pi.list_prod_apply] using l.measurable_prod hl

Premises used: Pi.list_prod_apply, List.measurable_prod
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
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 μ
⊢ AEMeasurable.{u_3, u_2} (β := M) (fun (x : α) ↦ prod (map (fun (f : α → M) ↦ f x) l)) μ

Tactic:
simpa only [← Pi.list_prod_apply] using l.aemeasurable_prod hl

Premises used: List.aemeasurable_prod, Pi.list_prod_apply
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
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
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))
⊢ Measurable l.prod

Tactic:
rcases l with ⟨l⟩
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_4
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
l_1 : Multiset (α → M)
l : List (α → M)
hl :
  ∀ (f : α → M),
    Membership.mem (γ := Multiset (α → M)) (Quot.mk (⇑(List.isSetoid (α → M)) : List (α → M) → List (α → M) → Prop) l)
        f →
      Measurable f
⊢ ∀ f ∈ l, Measurable f

Tactic:
simpa using hl
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_4
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
l_1 : Multiset (α → M)
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:
simpa using l.measurable_prod (by simpa using hl)

Premises used: List.measurable_prod
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
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 μ
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)) μ
⊢ AEMeasurable l.prod μ

Tactic:
rcases l with ⟨l⟩
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_4
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l_1 : Multiset (α → M)
l : List (α → M)
hl :
  ∀ (f : α → M),
    Membership.mem (γ := Multiset (α → M)) (Quot.mk (⇑(List.isSetoid (α → M)) : List (α → M) → List (α → M) → Prop) l)
        f →
      AEMeasurable f μ
⊢ ∀ f ∈ l, AEMeasurable f μ

Tactic:
simpa using hl
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_4
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l_1 : Multiset (α → M)
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:
simpa using l.aemeasurable_prod (by simpa using hl)

Premises used: List.aemeasurable_prod
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_4
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
s : Multiset (α → M)
hs : ∀ f ∈ s, Measurable f
⊢ Measurable.{u_4, u_2} (β := M) fun (x : α) ↦ prod (map (fun (f : α → M) ↦ f x) s)

Tactic:
simpa only [← Pi.multiset_prod_apply] using s.measurable_prod hs

Premises used: Pi.multiset_prod_apply, Multiset.measurable_prod
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_4
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
s : Multiset (α → M)
hs : ∀ f ∈ s, AEMeasurable f μ
⊢ AEMeasurable.{u_4, u_2} (β := M) (fun (x : α) ↦ prod (map (fun (f : α → M) ↦ f x) s)) μ

Tactic:
simpa only [← Pi.multiset_prod_apply] using s.aemeasurable_prod hs

Premises used: Multiset.aemeasurable_prod, Pi.multiset_prod_apply
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
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)
simp_rw : Measurable.{u_4, u_2} (β := M) fun (a : α) ↦ (∏ c ∈ s, f c) a
⊢ Measurable.{u_4, u_2} (β := M) fun (a : α) ↦ ∏ i ∈ s, f i a

Tactic:
simp_rw [← Finset.prod_apply]

Premises used: Finset.prod_apply
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
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 : α) ↦ (∏ c ∈ s, f c) a

Tactic:
Finset.prod_induction _ _ (fun _ _ => Measurable.mul) (@measurable_one M _ _ _ _) hf

Premises used: Finset.prod_induction, measurable_one
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
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 : α) ↦ (∏ c ∈ s, f c) a

Tactic:
exact Finset.prod_induction _ _ (fun _ _ => Measurable.mul) (@measurable_one M _ _ _ _) hf

Premises used: Finset.prod_induction, measurable_one
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
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
simp : Measurable.{u_4, u_2} (β := M) fun (a : α) ↦ ∏ c ∈ s, f c a (g a)
⊢ Measurable.{u_4, u_2} (β := M) fun (a : α) ↦ (∏ i ∈ s, f i a) (g a)

Tactic:
simp only [prod_apply]

Premises used: Finset.prod_apply
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
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
funProp : ∀ i ∈ s, i ∈ s
⊢ Measurable.{u_4, u_2} (β := M) fun (a : α) ↦ ∏ c ∈ s, f c a (g a)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
ι : Type u_3
α : Type u_4
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, AEMeasurable (f i) μ
⊢ AEMeasurable.{u_4, u_2} (β := M) (∏ i ∈ s, f i) μ

Tactic:
Multiset.aemeasurable_prod _ fun _g hg =>
    let ⟨_i, hi, hg⟩ := Multiset.mem_map.1 hg
    hg ▸ hf _ hi

Premises used: AEMeasurable, Multiset.mem_map, Multiset.aemeasurable_prod, Eq.rec, Finset.prod, Iff.mp, _private.0.Finset.aemeasurable_prod.match_1
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
ι : Type u_3
α : Type u_4
inst : CommMonoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, AEMeasurable (f i) μ
⊢ AEMeasurable.{u_4, u_2} (β := M) (fun (a : α) ↦ ∏ i ∈ s, f i a) μ

Tactic:
simpa only [← Finset.prod_apply] using s.aemeasurable_prod hf

Premises used: Finset.prod_apply, Finset.aemeasurable_prod
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Mul α
inst_2 : Div α
inst_3 : Inv α
inst_4 : DiscreteMeasurableSpace.{u_1} (α × α)
⊢ MeasurableMul₂ α

Tactic:
⟨.of_discrete⟩

Premises used: Measurable.of_discrete, MeasurableMul₂.mk
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Mul α
inst_2 : Div α
inst_3 : Inv α
inst_4 : DiscreteMeasurableSpace α
⊢ MeasurableInv α

Tactic:
⟨.of_discrete⟩

Premises used: Measurable.of_discrete, MeasurableInv.mk
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Mul α
inst_2 : Div α
inst_3 : Inv α
inst_4 : DiscreteMeasurableSpace.{u_1} (α × α)
⊢ MeasurableDiv₂ α

Tactic:
⟨.of_discrete⟩

Premises used: MeasurableDiv₂.mk, Measurable.of_discrete
-- Module: Mathlib.MeasureTheory.Group.Convolution
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 ν
rw₁ rw₂ : ∫⁻ (a : M × M), f (a.1 * a.2) ∂μ.prod ν = ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν
⊢ ∫⁻ (z : M), f z ∂μ ∗ₘ ν = ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν

Tactic:
rw [mconv, lintegral_map hf measurable_mul]

Premises used: MeasurableMul₂.measurable_mul, MeasureTheory.lintegral_map, MeasureTheory.Measure.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 ν
f : M → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : M × M) ↦ f (z.1 * z.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 : SFinite ν
f : M → ℝ≥0∞
hf : Measurable f
rw : ∫⁻ (z : M × M), f (z.1 * z.2) ∂μ.prod ν = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∂μ
rw₁ rw₂ : ∫⁻ (x : M), ∫⁻ (y : M), f ((x, y).1 * (x, y).2) ∂ν ∂μ = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∂μ
⊢ ∫⁻ (z : M), f z ∂μ ∗ₘ ν = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∂μ

Tactic:
rw [lintegral_mconv_eq_lintegral_prod hf, lintegral_prod _ (by fun_prop)]

Premises used: MeasureTheory.lintegral_prod, MeasureTheory.Measure.lintegral_mconv_eq_lintegral_prod
-- Module: Mathlib.MeasureTheory.Group.Convolution
Goal:
M : Type u_1
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
x : M
μ : Measure M
inst_3 : 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
x : M
μ : Measure M
inst_3 : SFinite μ
⊢ Measurable (α := M) (Prod.mk 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
x : M
μ : Measure M
inst_3 : SFinite μ
rw : Eq (α := Measure M) (map ((fun (x : M × M) ↦ x.1 * x.2) ∘ Prod.mk x) μ) (map (fun (y : M) ↦ x * y) μ)
⊢ Eq (α := Measure M) (map (fun (x : M × M) ↦ x.1 * x.2) (Measure.prod (dirac x) μ)) (map (fun (y : M) ↦ x * y) μ)

Tactic:
rw [dirac_prod, map_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.Measure.dirac_prod, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Group.Convolution
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) ∘ Prod.mk x) μ) (map (fun (y : M) ↦ x * y) μ)

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
μ : Measure M
inst_3 : SFinite μ
x : M
⊢ 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 μ
x : M
⊢ Measurable (β := M × M) fun (x_1 : M) ↦ (x_1, 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 : SFinite μ
x : M
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) μ)
⊢ Eq (α := Measure M) (map (fun (x : M × M) ↦ x.1 * x.2) (μ.prod (dirac x))) (map (fun (y : M) ↦ y * x) μ)

Tactic:
rw [prod_dirac, map_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.Measure.prod_dirac, MeasureTheory.Measure.map_map