awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
η : Kernel α γ
⊢ Eq (α := Kernel α (β × γ)) (0 ×ₖ η) 0

Tactic:
simp [prod]

Premises used: ProbabilityTheory.Kernel.prod
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
⊢ Eq (α := Kernel α (β × γ)) (κ ×ₖ 0) 0

Tactic:
simp [prod]

Premises used: ProbabilityTheory.Kernel.prod
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
h : ¬IsSFiniteKernel κ
⊢ κ ×ₖ η = 0

Tactic:
simp [prod, h]

Premises used: ProbabilityTheory.Kernel.prod
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
h : ¬IsSFiniteKernel η
⊢ κ ×ₖ η = 0

Tactic:
simp [prod, h]

Premises used: ProbabilityTheory.Kernel.prod
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
simp_rw :
  (((κ ∥ₖ η ∘ₖ copy α : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
simp_rw₁ :
  (Measure.bind (α := α × α) (mα := Prod.instMeasurableSpace) ((copy α : (a : α) → Measure (α × α)) a)
          (⇑(κ ∥ₖ η) : (a : α × α) → Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
simp_rw₂ :
  (Measure.bind (mα := Prod.instMeasurableSpace) (Measure.dirac (a, a)) (⇑(κ ∥ₖ η) : (a : α × α) → Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
simp_rw₃ :
  (((κ ∥ₖ η : (a : α × α) → Measure (β × γ)) (a, a) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
simp_rw₄ :
  (Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
⊢ (((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [prod, comp_apply, copy_apply, Measure.dirac_bind (Kernel.measurable _) (a, a),
    parallelComp_apply, Measure.prod_apply hs]

Premises used: MeasureTheory.Measure.dirac_bind, ProbabilityTheory.Kernel.copy_apply, MeasureTheory.Measure.prod_apply, Prod.mk, ProbabilityTheory.Kernel.comp_apply, ProbabilityTheory.Kernel.measurable, ProbabilityTheory.Kernel.parallelComp_apply, ProbabilityTheory.Kernel.prod
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
h :
  ∀ (s : Set (β × γ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure (β × γ)) ((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ))
    (Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : Measure (β × γ))

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    (Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) s
h₁ h₂ :
  ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (x : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂(κ : (a : α) → Measure β) a
⊢ Eq (α := ℝ≥0∞) ((((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [prod_apply' _ _ _ hs, Measure.prod_apply hs]

Premises used: ProbabilityTheory.Kernel.prod_apply', MeasureTheory.Measure.prod_apply
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
a : α
rw :
  (Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ rw₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [prod_apply, Measure.prod_prod]

Premises used: ProbabilityTheory.Kernel.prod_apply, MeasureTheory.Measure.prod_prod
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure β
inst : SFinite μ
ν : Measure γ
inst_1 : SFinite ν
h :
  ∀ (x : α) (s : Set (β × γ)),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((const α μ ×ₖ const α ν : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s :
          ℝ≥0∞)
        ((((const α (μ.prod ν) : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel α (β × γ)) (const α μ ×ₖ const α ν) (const α (μ.prod ν))

Tactic:
ext x
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure β
inst : SFinite μ
ν : Measure γ
inst_1 : SFinite ν
x : α
s : Set (β × γ)
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((((const α μ ×ₖ const α ν : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.prod (((const α μ : Kernel α β) : (a : α) → Measure β) x)
            (((const α ν : Kernel α γ) : (a : α) → Measure γ) x) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((μ.prod (((const α ν : Kernel α γ) : (a : α) → Measure γ) x) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
h₃ h₄ : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞) ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((const α μ ×ₖ const α ν : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((const α (μ.prod ν) : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [const_apply, prod_apply, const_apply, const_apply]

Premises used: ProbabilityTheory.Kernel.prod_apply, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
simp_rw :
  ∫⁻ (b : α × α), ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η : (a : α × α) → Measure (β × γ)) b ∂Measure.dirac (a, a) =
    ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(η : (a : α) → Measure γ) a ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (c : β × γ), g c ∂(κ ×ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(η : (a : α) → Measure γ) a ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [prod, lintegral_comp _ _ _ hg, copy_apply]

Premises used: ProbabilityTheory.Kernel.copy_apply, ProbabilityTheory.Kernel.lintegral_comp, ProbabilityTheory.Kernel.prod
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ Measurable (β := ℝ≥0∞) fun (b : α × α) ↦ ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η : (a : α × α) → Measure (β × γ)) b

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η : (a : α × α) → Measure (β × γ)) (a, a) =
    ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(η : (a : α) → Measure γ) a ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (b : α × α), ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η : (a : α × α) → Measure (β × γ)) b ∂Measure.dirac (a, a) =
    ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(η : (a : α) → Measure γ) a ∂(κ : (a : α) → Measure β) a

Tactic:
rw [lintegral_dirac' _ (by fun_prop)]

Premises used: MeasureTheory.lintegral_dirac'
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
simp_rw :
  ∫⁻ (c : β × γ), g c ∂Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) =
    ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(η : (a : α) → Measure γ) a ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η : (a : α × α) → Measure (β × γ)) (a, a) =
    ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(η : (a : α) → Measure γ) a ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [parallelComp_apply, MeasureTheory.lintegral_prod _ hg.aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_prod, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (c : β × γ), g c ∂Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) =
    ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂(κ : (a : α) → Measure β) a ∂(η : (a : α) → Measure γ) a
rw₁ rw₂ :
  ∫⁻ (y : γ), ∫⁻ (x : β), g (x, y) ∂(κ : (a : α) → Measure β) a ∂(η : (a : α) → Measure γ) a =
    ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂(κ : (a : α) → Measure β) a ∂(η : (a : α) → Measure γ) a
⊢ ∫⁻ (c : β × γ), g c ∂(κ ×ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂(κ : (a : α) → Measure β) a ∂(η : (a : α) → Measure γ) a

Tactic:
rw [prod_apply, MeasureTheory.lintegral_prod_symm _ hg.aemeasurable]

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.prod_apply, MeasureTheory.lintegral_prod_symm
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
κ : Kernel α γ
inst : IsSFiniteKernel κ
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(κ : (a : α) → Measure γ) a ∂(deterministic f hf : (a : α) → Measure β) a =
    ∫⁻ (c : γ), g (f a, c) ∂(κ : (a : α) → Measure γ) a
rw₁ rw₂ : ∫⁻ (y : γ), g (f a, y) ∂(κ : (a : α) → Measure γ) a = ∫⁻ (c : γ), g (f a, c) ∂(κ : (a : α) → Measure γ) a
⊢ ∫⁻ (p : β × γ), g p ∂(deterministic f hf ×ₖ κ : (a : α) → Measure (β × γ)) a =
    ∫⁻ (c : γ), g (f a, c) ∂(κ : (a : α) → Measure γ) a

Tactic:
rw [lintegral_prod _ _ _ hg, lintegral_deterministic' _ hg.lintegral_prod_right']

Premises used: Measurable.lintegral_prod_right', ProbabilityTheory.Kernel.lintegral_prod, ProbabilityTheory.Kernel.lintegral_deterministic'
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → γ
hf : Measurable f
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂(κ : (a : α) → Measure β) a ∂(deterministic f hf : (a : α) → Measure γ) a =
    ∫⁻ (b : β), g (b, f a) ∂(κ : (a : α) → Measure β) a
rw₁ rw₂ : ∫⁻ (x : β), g (x, f a) ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), g (b, f a) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (p : β × γ), g p ∂(κ ×ₖ deterministic f hf : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), g (b, f a) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [lintegral_prod_symm _ _ _ hg, lintegral_deterministic' _ hg.lintegral_prod_left']

Premises used: ProbabilityTheory.Kernel.lintegral_prod_symm, Measurable.lintegral_prod_left', ProbabilityTheory.Kernel.lintegral_deterministic'
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
rw :
  ∫⁻ (p : α × β), f p ∂(deterministic id ⋯ ×ₖ κ : (a : α) → Measure (α × β)) a =
    ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a
rw₁ : ∫⁻ (c : β), f (id a, c) ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a
rw₂ rw₃ : ∫⁻ (c : β), f (a, c) ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (p : α × β), f p ∂(Kernel.id ×ₖ κ : (a : α) → Measure (α × β)) a =
    ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [Kernel.id, lintegral_deterministic_prod _ _ _ hf, id_eq]

Premises used: ProbabilityTheory.Kernel.id, ProbabilityTheory.Kernel.lintegral_deterministic_prod, id_eq
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel β α
inst : IsSFiniteKernel κ
b : β
rw :
  ∫⁻ (p : α × β), f p ∂(κ ×ₖ deterministic id ⋯ : (a : β) → Measure (α × β)) b =
    ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b
rw₁ : ∫⁻ (b_1 : α), f (b_1, id b) ∂(κ : (a : β) → Measure α) b = ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b
rw₂ rw₃ : ∫⁻ (b_1 : α), f (b_1, b) ∂(κ : (a : β) → Measure α) b = ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b
⊢ ∫⁻ (p : α × β), f p ∂(κ ×ₖ Kernel.id : (a : β) → Measure (α × β)) b =
    ∫⁻ (a : α), f (a, b) ∂(κ : (a : β) → Measure α) b

Tactic:
rw [Kernel.id, lintegral_prod_deterministic _ _ _ hf, id_eq]

Premises used: ProbabilityTheory.Kernel.id, ProbabilityTheory.Kernel.lintegral_prod_deterministic, id_eq
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
hf :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    ((((deterministic f mf ×ₖ κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [prod_apply' _ _ _ hs, lintegral_deterministic']

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

Tactic:
measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
exact measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
a : α
s : Set (α × β)
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞)
    ((((deterministic id ⋯ ×ₖ κ : (a : α) → Measure (α × β)) a : Measure (α × β)) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk (id a) ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
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∞)
    ((((Kernel.id ×ₖ κ : (a : α) → Measure (α × β)) a : Measure (α × β)) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [Kernel.id, deterministic_prod_apply' _ _ _ hs, id_eq]

Premises used: ProbabilityTheory.Kernel.deterministic_prod_apply', ProbabilityTheory.Kernel.id, id_eq
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsMarkovKernel κ
η : Kernel α γ
inst_1 : IsMarkovKernel η
⊢ IsMarkovKernel (κ ∥ₖ η ∘ₖ copy α)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : IsZeroOrMarkovKernel κ
η : Kernel α γ
inst : IsZeroOrMarkovKernel η
inl :
  ∀ [h : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    IsZeroOrMarkovKernel (β := β × γ) (mβ := Prod.instMeasurableSpace) (0 ×ₖ η)
inr : ∀ (h : IsMarkovKernel κ), IsZeroOrMarkovKernel (κ ×ₖ η)
⊢ IsZeroOrMarkovKernel (κ ×ₖ η)

Tactic:
rcases eq_zero_or_isMarkovKernel κ with rfl | h

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel α γ
inst : IsZeroOrMarkovKernel η
h : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
⊢ IsZeroOrMarkovKernel (β := β × γ) (mβ := Prod.instMeasurableSpace) (0 ∥ₖ η ∘ₖ copy α)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h_1 : IsZeroOrMarkovKernel κ
η : Kernel α γ
inst : IsZeroOrMarkovKernel η
h : IsMarkovKernel κ
inr :
  ∀ [IsZeroOrMarkovKernel.{u_1, u_4} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0],
    IsZeroOrMarkovKernel (β := β × γ) (mβ := Prod.instMeasurableSpace) (κ ×ₖ 0)
inr₁ : ∀ (h' : IsMarkovKernel η), IsZeroOrMarkovKernel (κ ×ₖ η)
⊢ IsZeroOrMarkovKernel (κ ×ₖ η)

Tactic:
rcases eq_zero_or_isMarkovKernel η with rfl | h'

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h_1 : IsZeroOrMarkovKernel κ
h : IsMarkovKernel κ
inst : IsZeroOrMarkovKernel.{u_1, u_4} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0
⊢ IsZeroOrMarkovKernel (β := β × γ) (mβ := Prod.instMeasurableSpace) (κ ∥ₖ 0 ∘ₖ copy α)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h_1 : IsZeroOrMarkovKernel κ
η : Kernel α γ
inst : IsZeroOrMarkovKernel η
h : IsMarkovKernel κ
h' : IsMarkovKernel η
⊢ IsZeroOrMarkovKernel (κ ×ₖ η)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsFiniteKernel κ
η : Kernel α γ
inst_1 : IsFiniteKernel η
⊢ IsFiniteKernel (κ ∥ₖ η ∘ₖ copy α)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel α γ
⊢ IsSFiniteKernel (κ ∥ₖ η ∘ₖ copy α)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsMarkovKernel η
rw : (κ ∥ₖ η).fst ∘ₖ copy α = κ
⊢ (κ ×ₖ η).fst = κ

Tactic:
rw [prod, fst_comp]

Premises used: ProbabilityTheory.Kernel.fst_comp, ProbabilityTheory.Kernel.prod