awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
pos :
  (Kernel.const Unit (μ + ν) ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () =
    HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
      ((Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
pos₁ :
  (HAdd.hAdd (α := Kernel Unit α) (Kernel.const Unit μ) (Kernel.const Unit ν) ⊗ₖ Kernel.prodMkLeft Unit κ :
        (a : Unit) → Measure (α × β))
      () =
    HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
      ((Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
pos₂ :
  (HAdd.hAdd (α := Kernel Unit (α × β)) (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ)
          (Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ) :
        (a : Unit) → Measure (α × β))
      () =
    HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
      ((Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

Tactic:
simp_rw [Measure.compProd, Kernel.const_add, Kernel.compProd_add_left, Kernel.add_apply]

Premises used: ProbabilityTheory.Kernel.add_apply, ProbabilityTheory.Kernel.const_add, ProbabilityTheory.Kernel.compProd_add_left, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α β
hκ : ¬IsSFiniteKernel κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

Tactic:
simp [hκ]
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
pos : ∀ (hμ : SFinite μ), μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
neg : ∀ (hμ : ¬SFinite μ), μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

Tactic:
by_cases hμ : SFinite μ

Premises used: MeasureTheory.SFinite
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
hμ : SFinite μ
pos :
  (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (κ + η) : (a : Unit) → Measure (α × β)) () =
    HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η : (a : Unit) → Measure (α × β)) () : Measure (α × β))
pos₁ :
  (Kernel.const Unit μ ⊗ₖ
          HAdd.hAdd (α := Kernel.{u_1, u_2} (Unit × α) β) (Kernel.prodMkLeft Unit κ) (Kernel.prodMkLeft Unit η) :
        (a : Unit) → Measure (α × β))
      () =
    HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η : (a : Unit) → Measure (α × β)) () : Measure (α × β))
pos₂ :
  (HAdd.hAdd (α := Kernel Unit (α × β)) (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ)
          (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η) :
        (a : Unit) → Measure (α × β))
      () =
    HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η : (a : Unit) → Measure (α × β)) () : Measure (α × β))
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

Tactic:
simp_rw [Measure.compProd, Kernel.prodMkLeft_add, Kernel.compProd_add_right, Kernel.add_apply]

Premises used: ProbabilityTheory.Kernel.prodMkLeft_add, ProbabilityTheory.Kernel.add_apply, ProbabilityTheory.Kernel.compProd_add_right, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
hμ : ¬SFinite μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

Tactic:
simp [hμ]
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
ι : Type u_3
inst : Countable ι
μ : ι → Measure α
inst_1 : ∀ (i : ι), SFinite (μ i)
rw :
  Eq (α := Measure (α × β))
    ((Kernel.sum fun (i : ι) ↦ Kernel.const Unit (μ i) ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () :
      Measure (α × β))
    (sum fun (i : ι) ↦ μ i ⊗ₘ κ : Measure (α × β))
⊢ sum μ ⊗ₘ κ = sum fun (i : ι) ↦ μ i ⊗ₘ κ

Tactic:
rw [compProd, ← Kernel.sum_const, Kernel.compProd_sum_left]

Premises used: ProbabilityTheory.Kernel.sum_const, ProbabilityTheory.Kernel.compProd_sum_left, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
ι : Type u_3
inst : Countable ι
μ : ι → Measure α
inst_1 : ∀ (i : ι), SFinite (μ i)
⊢ Eq (α := Measure (α × β))
    ((Kernel.sum fun (i : ι) ↦ Kernel.const Unit (μ i) ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () :
      Measure (α × β))
    (sum fun (i : ι) ↦ μ i ⊗ₘ κ : Measure (α × β))

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ι : Type u_3
inst : Countable ι
κ : ι → Kernel α β
h : ∀ (i : ι), IsSFiniteKernel (κ i)
rw :
  Eq (α := Measure (α × β))
    ((Kernel.sum fun (i : ι) ↦ Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (κ i) : (a : Unit) → Measure (α × β)) () :
      Measure (α × β))
    (sum fun (i : ι) ↦ μ ⊗ₘ κ i : Measure (α × β))
⊢ μ ⊗ₘ Kernel.sum κ = sum fun (i : ι) ↦ μ ⊗ₘ κ i

Tactic:
rw [compProd, ← Kernel.sum_prodMkLeft, Kernel.compProd_sum_right]

Premises used: MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.compProd_sum_right, ProbabilityTheory.Kernel.sum_prodMkLeft
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ι : Type u_3
inst : Countable ι
κ : ι → Kernel α β
h : ∀ (i : ι), IsSFiniteKernel (κ i)
⊢ Eq (α := Measure (α × β))
    ((Kernel.sum fun (i : ι) ↦ Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (κ i) : (a : Unit) → Measure (α × β)) () :
      Measure (α × β))
    (sum fun (i : ι) ↦ μ ⊗ₘ κ i : Measure (α × β))

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsMarkovKernel κ
h :
  ∀ (s : Set α),
    MeasurableSet s → Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ ⊗ₘ κ).fst = μ

Tactic:
ext s
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsMarkovKernel κ
s : Set α
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((fst.{u_1, u_2} (β := β) ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    (((map (α := α × β) Prod.fst ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞)
    ((((Kernel.fst (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) : (a : Unit) → Measure α) () : Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₃ :
  Eq (α := ℝ≥0∞) ((((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₄ h₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [compProd, Measure.fst, ← Kernel.fst_apply, Kernel.fst_compProd, Kernel.const_apply]

Premises used: ProbabilityTheory.Kernel.fst_apply, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.const_apply, ProbabilityTheory.Kernel.fst_compProd, MeasureTheory.Measure.fst
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
a : ℝ≥0∞
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h :
  ∀ (s : Set (α × β)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((a • μ) ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
      ((a • μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (a • μ) ⊗ₘ κ = a • μ ⊗ₘ κ

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
a : ℝ≥0∞
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((a • μ) ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((a • μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [compProd_apply hs, lintegral_smul_measure, smul_apply, smul_eq_mul]

Premises used: MeasureTheory.lintegral_smul_measure, MeasureTheory.Measure.compProd_apply, MeasureTheory.Measure.smul_apply, smul_eq_mul
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
rw :
  ∫⁻ (b : α),
      ∫⁻ (c : β),
        f
          (b,
            c) ∂((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β)
          ((), b) ∂(Kernel.const Unit μ : (a : Unit) → Measure α) () =
    ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a ∂μ
⊢ ∫⁻ (x : α × β), f x ∂μ ⊗ₘ κ = ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a ∂μ

Tactic:
rw [compProd, Kernel.lintegral_compProd _ _ _ hf]

Premises used: MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.lintegral_compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : α),
      ∫⁻ (c : β),
        f
          (b,
            c) ∂((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β)
          ((), b) ∂(Kernel.const Unit μ : (a : Unit) → Measure α) () =
    ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a ∂μ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
rw :
  ∫⁻ (x : α) in s,
      ∫⁻ (y : β) in t,
        f
          (x,
            y) ∂((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β)
          ((), x) ∂(Kernel.const Unit μ : (a : Unit) → Measure α) () =
    ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂(κ : (a : α) → Measure β) a ∂μ
⊢ ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂(κ : (a : α) → Measure β) a ∂μ

Tactic:
rw [compProd, Kernel.setLIntegral_compProd _ _ _ hf hs ht]

Premises used: ProbabilityTheory.Kernel.setLIntegral_compProd, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ ∫⁻ (x : α) in s,
      ∫⁻ (y : β) in t,
        f
          (x,
            y) ∂((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β)
          ((), x) ∂(Kernel.const Unit μ : (a : Unit) → Measure α) () =
    ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂(κ : (a : α) → Measure β) a ∂μ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : MeasurableSingletonClass α
a : α
inst_1 : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
rw :
  ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂dirac a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((dirac a ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [compProd_apply hs, lintegral_dirac]

Premises used: MeasureTheory.Measure.compProd_apply, MeasureTheory.lintegral_dirac
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
β : Type u_2
mβ : MeasurableSpace β
κ : Kernel Unit β
inst : IsSFiniteKernel κ
h :
  ∀ (s : Set (Unit × β)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((dirac () ⊗ₘ κ : (a : Set (Unit × β)) → ℝ≥0∞) s : ℝ≥0∞)
      (((map (Prod.mk ()) ((κ : (a : Unit) → Measure β) ()) : Measure (Unit × β)) : (a : Set (Unit × β)) → ℝ≥0∞) s :
        ℝ≥0∞)
⊢ dirac () ⊗ₘ κ = map (Prod.mk ()) ((κ : (a : Unit) → Measure β) ())

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
β : Type u_2
mβ : MeasurableSpace β
κ : Kernel Unit β
inst : IsSFiniteKernel κ
s : Set (Unit × β)
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((κ : (a : Unit) → Measure β) () : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk () ⁻¹' s) : ℝ≥0∞)
    (((map (Prod.mk ()) ((κ : (a : Unit) → Measure β) ()) : Measure (Unit × β)) : (a : Set (Unit × β)) → ℝ≥0∞) s : ℝ≥0∞)
h₁ h₂ :
  Eq (α := ℝ≥0∞) ((((κ : (a : Unit) → Measure β) () : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk () ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : Unit) → Measure β) () : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk () ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((dirac () ⊗ₘ κ : (a : Set (Unit × β)) → ℝ≥0∞) s : ℝ≥0∞)
    (((map (Prod.mk ()) ((κ : (a : Unit) → Measure β) ()) : Measure (Unit × β)) : (a : Set (Unit × β)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [dirac_compProd_apply hs, Measure.map_apply measurable_prodMk_left hs]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.dirac_compProd_apply, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
inst : SFinite μ
rw :
  Eq (α := Measure (Unit × β)) (map (Prod.mk ()) ((Kernel.const Unit μ : (a : Unit) → Measure β) ()))
    (map (Prod.mk ()) μ)
rw₁ rw₂ : Eq (α := Measure (Unit × β)) (map (Prod.mk ()) μ) (map (Prod.mk ()) μ)
⊢ Eq (α := Measure (Unit × β)) (dirac () ⊗ₘ Kernel.const Unit μ) (map (Prod.mk ()) μ)

Tactic:
rw [dirac_unit_compProd, Kernel.const_apply]

Premises used: ProbabilityTheory.Kernel.const_apply, MeasureTheory.Measure.dirac_unit_compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
inst : SFinite μ
⊢ snd (dirac () ⊗ₘ Kernel.const Unit μ) = μ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
⊢ SFinite (α := α × β) (m0 := Prod.instMeasurableSpace)
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ())

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
⊢ IsFiniteMeasure (α := α × β) (m0 := Prod.instMeasurableSpace)
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ())

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsProbabilityMeasure μ
inst_1 : IsMarkovKernel κ
⊢ IsProbabilityMeasure (α := α × β) (m0 := Prod.instMeasurableSpace)
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ())

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsZeroOrProbabilityMeasure μ
inst_1 : IsZeroOrMarkovKernel κ
⊢ IsZeroOrProbabilityMeasure (α := α × β) (m0 := Prod.instMeasurableSpace)
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ())

Tactic:
IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure ()

Premises used: Unit.unit, ProbabilityTheory.IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsZeroOrProbabilityMeasure μ
inst_1 : IsZeroOrMarkovKernel κ
⊢ IsZeroOrProbabilityMeasure (α := α × β) (m0 := Prod.instMeasurableSpace)
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ())

Tactic:
exact IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure ()

Premises used: Unit.unit, ProbabilityTheory.IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
pos :
  ∀ (hμ : SFinite μ),
    map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) =
      μ ⊗ₘ κ ⊗ₘ η
neg :
  ∀ (hμ : ¬SFinite μ),
    map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) =
      μ ⊗ₘ κ ⊗ₘ η
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
by_cases hμ : SFinite μ

Premises used: MeasureTheory.SFinite
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : ¬SFinite μ
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
simp [hμ]
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
pos :
  ∀ (hκ : IsSFiniteKernel κ),
    map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) =
      μ ⊗ₘ κ ⊗ₘ η
neg :
  ∀ (hκ : ¬IsSFiniteKernel κ),
    map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) =
      μ ⊗ₘ κ ⊗ₘ η
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
by_cases hκ : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : ¬IsSFiniteKernel κ
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
simp [hκ]
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
pos :
  ∀ (hη : IsSFiniteKernel η),
    map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) =
      μ ⊗ₘ κ ⊗ₘ η
neg :
  ∀ (hη : ¬IsSFiniteKernel η),
    map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) =
      μ ⊗ₘ κ ⊗ₘ η
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
by_cases hη : IsSFiniteKernel η

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
simp [hη]
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
pos :
  ∀ (s : Set ((α × β) × γ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) :
            (a : Set ((α × β) × γ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((μ ⊗ₘ κ ⊗ₘ η : (a : Set ((α × β) × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
⊢ Measurable (α := α × β × γ) (β := (α × β) × γ)
    (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ)

Tactic:
fun_prop