awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
hμ : IsSFiniteKernel μ
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  ∫⁻ (b : β),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
        ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) :
          ℝ≥0∞) ∂(μ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
        (((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(μ : (a : α) → Measure β) a +
      ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(μ : (a : α) → Measure β) a
⊢ Eq (α := ℝ≥0∞)
    ((((μ ⊗ₖ (κ + η) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((μ ⊗ₖ κ + μ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [compProd_apply hs, coe_add, Pi.add_apply, Measure.coe_add]

Premises used: ProbabilityTheory.Kernel.coe_add, MeasureTheory.Measure.coe_add, Pi.add_apply, ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
hμ : IsSFiniteKernel μ
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
⊢ ∫⁻ (b : β),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
        ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) :
          ℝ≥0∞) ∂(μ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
        (((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(μ : (a : α) → Measure β) a +
      ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(μ : (a : α) → Measure β) a

Tactic:
rw [lintegral_add_left]

Premises used: MeasureTheory.lintegral_add_left
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
hμ : IsSFiniteKernel μ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
measurable_kernel_prodMk_left' hs a

Premises used: ProbabilityTheory.Kernel.measurable_kernel_prodMk_left'
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
hμ : IsSFiniteKernel μ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
exact measurable_kernel_prodMk_left' hs a

Premises used: ProbabilityTheory.Kernel.measurable_kernel_prodMk_left'
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
pos : ∀ (hη : IsSFiniteKernel η), Kernel.sum κ ⊗ₖ η = Kernel.sum fun (i : ι) ↦ κ i ⊗ₖ η
neg : ∀ (hη : ¬IsSFiniteKernel η), Kernel.sum κ ⊗ₖ η = Kernel.sum fun (i : ι) ↦ κ i ⊗ₖ η
⊢ Kernel.sum κ ⊗ₖ η = Kernel.sum fun (i : ι) ↦ κ i ⊗ₖ η

Tactic:
by_cases hη : IsSFiniteKernel η

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
pos :
  ∀ (a : α) (s : Set (β × γ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((Kernel.sum κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((((Kernel.sum fun (i : ι) ↦ κ i ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
            (a : Set (β × γ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Kernel.sum κ ⊗ₖ η = Kernel.sum fun (i : ι) ↦ κ i ⊗ₖ η

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
pos₁ :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(Kernel.sum κ : (a : α) → Measure β) a =
    (Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s
pos₂ :
  (∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a) =
    (Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s
pos₃ :
  Eq (α := ℝ≥0∞)
    (∑' (i : ι),
        ∫⁻ (b : β),
          (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (Prod.mk b ⁻¹' s) ∂(κ i : (a : α) → Measure β) a :
      ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
pos₄ :
  Eq (α := ℝ≥0∞)
    (∑' (i : ι),
      ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(κ i : (a : α) → Measure β) a)
    (∑' (i : ι), (((κ i ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ i ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp_rw [sum_apply, compProd_apply hs, sum_apply, lintegral_sum_measure, Measure.sum_apply _ hs,
    compProd_apply hs]

Premises used: MeasureTheory.Measure.sum_apply, ProbabilityTheory.Kernel.sum_apply, ProbabilityTheory.Kernel.compProd_apply, MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : ¬IsSFiniteKernel η
⊢ Kernel.sum κ ⊗ₖ η = Kernel.sum fun (i : ι) ↦ κ i ⊗ₖ η

Tactic:
simp [hη]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
pos : ∀ (hκ : IsSFiniteKernel κ), κ ⊗ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i
neg : ∀ (hκ : ¬IsSFiniteKernel κ), κ ⊗ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i
⊢ κ ⊗ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i

Tactic:
by_cases hκ : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : ¬IsSFiniteKernel κ
⊢ κ ⊗ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i

Tactic:
simp [hκ]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
pos :
  ∀ (a : α) (s : Set (β × γ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((κ ⊗ₖ Kernel.sum η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((((Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
            (a : Set (β × γ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ κ ⊗ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  ∫⁻ (b : β),
      ((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∑' (i : ι),
      ∫⁻ (b : β),
        (((η i : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ Kernel.sum η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp_rw [sum_apply, compProd_apply hs, Measure.sum_apply _ hs, sum_apply, compProd_apply hs]

Premises used: MeasureTheory.Measure.sum_apply, ProbabilityTheory.Kernel.sum_apply, ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  ∫⁻ (b : β),
      ((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (a_1 : β),
      ∑' (i : ι),
        (((η i : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a
pos₁ :
  ∀ (i : ι),
    AEMeasurable (β := ℝ≥0∞) (_m := mβ)
      (fun (b : β) ↦ (((η i : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))
      ((κ : (a : α) → Measure β) a)
⊢ ∫⁻ (b : β),
      ((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∑' (i : ι),
      ∫⁻ (b : β),
        (((η i : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [← lintegral_tsum]

Premises used: MeasureTheory.lintegral_tsum
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  ∀ (i : β),
    Eq (α := ℝ≥0∞)
      (((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, i) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk i ⁻¹' s) :
        ℝ≥0∞)
      (∑' (i_1 : ι), (((η i_1 : (a : α × β) → Measure γ) (a, i) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk i ⁻¹' s) :
        ℝ≥0∞)
⊢ ∫⁻ (b : β),
      ((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (a_1 : β),
      ∑' (i : ι),
        (((η i : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a

Tactic:
congr with i
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
i : β
pos : MeasurableSet (Prod.mk i ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, i) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk i ⁻¹' s) :
      ℝ≥0∞)
    (∑' (i_1 : ι), (((η i_1 : (a : α × β) → Measure γ) (a, i) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk i ⁻¹' s) :
      ℝ≥0∞)

Tactic:
rw [Measure.sum_apply]

Premises used: MeasureTheory.Measure.sum_apply
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
i : β
⊢ MeasurableSet (Prod.mk i ⁻¹' s)

Tactic:
measurable_prodMk_left hs

Premises used: measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
i : β
⊢ MeasurableSet (Prod.mk i ⁻¹' s)

Tactic:
exact measurable_prodMk_left hs

Premises used: measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∀ (i : ι),
    AEMeasurable (β := ℝ≥0∞) (_m := mβ)
      (fun (b : β) ↦ (((η i : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))
      ((κ : (a : α) → Measure β) a)

Tactic:
fun _ ↦ (measurable_kernel_prodMk_left' hs a).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left'
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∀ (i : ι),
    AEMeasurable (β := ℝ≥0∞) (_m := mβ)
      (fun (b : β) ↦ (((η i : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))
      ((κ : (a : α) → Measure β) a)

Tactic:
exact fun _ ↦ (measurable_kernel_prodMk_left' hs a).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left'
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
h :
  ∀ (a : α) (t : Set (β × δ)) (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞)
      (((((κ ⊗ₖ η).comapRight ⋯ : (a : α) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) t : ℝ≥0∞)
      ((((κ ⊗ₖ η.comapRight hf : (a : α) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (κ ⊗ₖ η).comapRight ⋯ = κ ⊗ₖ η.comapRight hf

Tactic:
ext a t ht
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
h :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Prod.map id f '' t) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η.comapRight hf : (a : α × β) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(κ : (a : α) → Measure β) a
h₁ : MeasurableSet (Prod.map id f '' t)
⊢ Eq (α := ℝ≥0∞)
    (((((κ ⊗ₖ η).comapRight ⋯ : (a : α) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ ⊗ₖ η.comapRight hf : (a : α) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [comapRight_apply' _ _ _ ht, compProd_apply, compProd_apply ht]

Premises used: ProbabilityTheory.Kernel.comapRight_apply', ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Prod.map id f '' t) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η.comapRight hf : (a : α × β) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(κ : (a : α) → Measure β) a

Tactic:
lintegral_congr fun b ↦ ?_

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
h :
  ∀ (b : β),
    Eq (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' Prod.map id f '' t) :
        ℝ≥0∞)
      ((((η.comapRight hf : (a : α × β) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' t) : ℝ≥0∞)
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Prod.map id f '' t) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η.comapRight hf : (a : α × β) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(κ : (a : α) → Measure β) a

Tactic:
refine lintegral_congr fun b ↦ ?_

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
b : β
h :
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' Prod.map id f '' t) :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (f '' Prod.mk b ⁻¹' t) : ℝ≥0∞)
h₁ : MeasurableSet (Prod.mk b ⁻¹' t)
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' Prod.map id f '' t) :
      ℝ≥0∞)
    ((((η.comapRight hf : (a : α × β) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' t) : ℝ≥0∞)

Tactic:
rw [comapRight_apply']

Premises used: ProbabilityTheory.Kernel.comapRight_apply'
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
b : β
h : ∀ (x : γ), x ∈ Prod.mk b ⁻¹' Prod.map id f '' t ↔ x ∈ f '' Prod.mk b ⁻¹' t
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' Prod.map id f '' t) :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (f '' Prod.mk b ⁻¹' t) : ℝ≥0∞)

Tactic:
congr with x
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
b : β
x : γ
⊢ x ∈ Prod.mk b ⁻¹' Prod.map id f '' t ↔ x ∈ f '' Prod.mk b ⁻¹' t

Tactic:
grind
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
b : β
⊢ MeasurableSet (Prod.mk b ⁻¹' t)

Tactic:
measurable_prodMk_left ht

Premises used: measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
b : β
⊢ MeasurableSet (Prod.mk b ⁻¹' t)

Tactic:
exact measurable_prodMk_left ht

Premises used: measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
⊢ MeasurableSet (Prod.map id f '' t)

Tactic:
(MeasurableEmbedding.id.prodMap hf).measurableSet_image.mpr ht

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image, MeasurableEmbedding.prodMap, MeasurableEmbedding.id