awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
hp : MeasurableSet.{u_2} (α := β) {z : β | p z}
h : ∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂((κ : (a : α) → Measure β) y : Measure β), p z
rw : ∀ᵐ (z : β) ∂((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β), p z
⊢ ∀ᵐ (z : β) ∂(⇑κ : (a : α) → Measure β) ∘ₘ μ, p z

Tactic:
rw [comp_eq_comp_const_apply]

Premises used: MeasureTheory.Measure.comp_eq_comp_const_apply
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
hp : MeasurableSet.{u_2} (α := β) {z : β | p z}
h : ∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂((κ : (a : α) → Measure β) y : Measure β), p z
⊢ ∀ᵐ (z : β) ∂((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β), p z

Tactic:
Kernel.ae_comp_of_ae_ae hp h

Premises used: ProbabilityTheory.Kernel.ae_comp_of_ae_ae
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
hp : MeasurableSet.{u_2} (α := β) {z : β | p z}
h : ∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂((κ : (a : α) → Measure β) y : Measure β), p z
⊢ ∀ᵐ (z : β) ∂((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β), p z

Tactic:
exact Kernel.ae_comp_of_ae_ae hp h

Premises used: ProbabilityTheory.Kernel.ae_comp_of_ae_ae
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
hp : MeasurableSet.{u_2} (α := β) {z : β | p z}
⊢ (∀ᵐ (z : β) ∂(⇑κ : (a : α) → Measure β) ∘ₘ μ, p z) ↔
    ∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂((κ : (a : α) → Measure β) y : Measure β), p z

Tactic:
⟨ae_ae_of_ae_comp, ae_comp_of_ae_ae hp⟩

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, MeasureTheory.Measure.ae_comp_of_ae_ae, Iff.intro
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
rw : SFinite (μ ⊗ₘ κ).snd
⊢ SFinite.{u_2} (α := β) (m0 := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)

Tactic:
rw [← snd_compProd]

Premises used: MeasureTheory.Measure.snd_compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
⊢ SFinite (μ ⊗ₘ κ).snd

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
rw : IsFiniteMeasure (μ ⊗ₘ κ).snd
⊢ IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)

Tactic:
rw [← snd_compProd]

Premises used: MeasureTheory.Measure.snd_compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
⊢ IsFiniteMeasure (μ ⊗ₘ κ).snd

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst : IsProbabilityMeasure μ
inst_1 : IsMarkovKernel κ
rw : IsProbabilityMeasure (μ ⊗ₘ κ).snd
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)

Tactic:
rw [← snd_compProd]

Premises used: MeasureTheory.Measure.snd_compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst : IsProbabilityMeasure μ
inst_1 : IsMarkovKernel κ
⊢ IsProbabilityMeasure (μ ⊗ₘ κ).snd

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst : IsZeroOrProbabilityMeasure μ
inst_1 : IsZeroOrMarkovKernel κ
rw : IsZeroOrProbabilityMeasure (μ ⊗ₘ κ).snd
⊢ IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ)

Tactic:
rw [← snd_compProd]

Premises used: MeasureTheory.Measure.snd_compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure α
κ η : Kernel α β
inst : IsZeroOrProbabilityMeasure μ
inst_1 : IsZeroOrMarkovKernel κ
⊢ IsZeroOrProbabilityMeasure (μ ⊗ₘ κ).snd

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
μ : Measure β
⊢ Eq (α := Kernel α γ) (κ ∘ₖ Kernel.const α μ) (Kernel.const α ((⇑κ : (a : β) → Measure γ) ∘ₘ μ))

Tactic:
rfl

Premises used: ProbabilityTheory.Kernel.comp, ProbabilityTheory.Kernel.const, rfl
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
h :
  ∀ (s : Set γ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((map f ((⇑κ : (a : α) → Measure β) ∘ₘ μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((⇑(κ.map f) : (a : α) → Measure γ) ∘ₘ μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure γ) (map f ((⇑κ : (a : α) → Measure β) ∘ₘ μ)) ((⇑(κ.map f) : (a : α) → Measure γ) ∘ₘ μ)

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
s : Set γ
hs : MeasurableSet s
h :
  ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) ∂μ =
    ∫⁻ (a : α), ((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂μ
⊢ Eq (α := ℝ≥0∞) (((map f ((⇑κ : (a : α) → Measure β) ∘ₘ μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((⇑(κ.map f) : (a : α) → Measure γ) ∘ₘ μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.map_apply hf hs, Measure.bind_apply (hf hs) κ.aemeasurable,
    Measure.bind_apply hs (Kernel.aemeasurable _)]

Premises used: MeasureTheory.Measure.bind_apply, MeasureTheory.Measure.map_apply, ProbabilityTheory.Kernel.aemeasurable
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) ∂μ =
    ∫⁻ (a : α), ((((κ.map f : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂μ

Tactic:
simp_rw [Kernel.map_apply' _ hf _ hs]

Premises used: ProbabilityTheory.Kernel.map_apply'
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h :
  ∀ (s : Set PUnit.{1}) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((⇑(Kernel.discard α) : (a : α) → Measure PUnit.{1}) ∘ₘ μ : (a : Set PUnit.{1}) → ℝ≥0∞) s : ℝ≥0∞)
      ((HSMul.hSMul (α := ℝ≥0∞) (β := Measure Unit) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (dirac ()) :
            (a : Set PUnit.{1}) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ (⇑(Kernel.discard α) : (a : α) → Measure PUnit.{1}) ∘ₘ μ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure Unit) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (dirac ())

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set PUnit.{1}
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((⇑(Kernel.discard α) : (a : α) → Measure PUnit.{1}) ∘ₘ μ : (a : Set PUnit.{1}) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (β := Measure Unit) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (dirac ()) :
          (a : Set PUnit.{1}) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp [Measure.bind_apply hs (Kernel.aemeasurable _), mul_comm]

Premises used: MeasureTheory.Measure.bind_apply, ProbabilityTheory.Kernel.aemeasurable, mul_comm
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ AEMeasurable (β := β × β) (_m := mβ) (fun (x : β) ↦ (x, x)) (map f μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
rw : Eq (α := Measure (β × β)) (map ((fun (x : β) ↦ (x, x)) ∘ f) μ) (map (fun (a : α) ↦ (f a, f a)) μ)
⊢ Eq (α := Measure (β × β)) (bind (mα := mβ) (map f μ) (⇑(Kernel.copy β) : (a : β) → Measure (β × β)))
    (map (fun (a : α) ↦ (f a, f a)) μ)

Tactic:
rw [Kernel.copy, deterministic_comp_eq_map, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]

Premises used: MeasureTheory.Measure.deterministic_comp_eq_map, AEMeasurable.map_map_of_aemeasurable, ProbabilityTheory.Kernel.copy
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ Eq (α := Measure (β × β)) (map ((fun (x : β) ↦ (x, x)) ∘ f) μ) (map (fun (a : α) ↦ (f a, f a)) μ)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
rw :
  Eq (α := Measure (α × β))
    ((Kernel.id ×ₖ κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
    ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ : Measure (α × β))
⊢ μ ⊗ₘ κ = (⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ

Tactic:
rw [compProd, Kernel.compProd_prodMkLeft_eq_comp]

Premises used: ProbabilityTheory.Kernel.compProd_prodMkLeft_eq_comp, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
⊢ Eq (α := Measure (α × β))
    ((Kernel.id ×ₖ κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
    ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ : Measure (α × β))

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
rw : Eq (α := Measure (α × α)) (map (fun (x : α) ↦ (x, x)) μ) ((⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ)
rw₁ :
  Eq (α := Measure (α × α)) (map (fun (x : α) ↦ (x, x)) μ)
    ((⇑(Kernel.deterministic (fun (x : α) ↦ (x, x)) ⋯) : (a : α) → Measure (α × α)) ∘ₘ μ)
rw₂ rw₃ : Eq (α := Measure (α × α)) (map (fun (x : α) ↦ (x, x)) μ) (map (fun (x : α) ↦ (x, x)) μ)
⊢ μ ⊗ₘ Kernel.id = (⇑(Kernel.copy α) : (a : α) → Measure (α × α)) ∘ₘ μ

Tactic:
rw [compProd_id, Kernel.copy, deterministic_comp_eq_map]

Premises used: MeasureTheory.Measure.compProd_id, MeasureTheory.Measure.deterministic_comp_eq_map, ProbabilityTheory.Kernel.copy
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
pos :
  ∀ (hκ : IsSFiniteKernel κ),
    Eq.{u_3 + 1} (α := Measure γ) ((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
      (snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ))
neg :
  ∀ (hκ : ¬IsSFiniteKernel κ),
    Eq.{u_3 + 1} (α := Measure γ) ((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
      (snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ))
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ))

Tactic:
by_cases hκ : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : ¬IsSFiniteKernel κ
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ))

Tactic:
simp [compProd_of_not_isSFiniteKernel _ _ hκ,
      Kernel.compProd_of_not_isSFiniteKernel_left _ _ hκ]

Premises used: ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left, MeasureTheory.Measure.compProd_of_not_isSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
pos :
  ∀ (s : Set γ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      (((snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s :
        ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ))

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
pos :
  ∫⁻ (a : α),
      ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a ∂μ =
    ∫⁻ (a : α),
      (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) ∂μ
rw : MeasurableSet (α := β × γ) (Prod.snd ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) ((((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
rw [Measure.bind_apply hs η.aemeasurable, Measure.snd_apply hs,
    Measure.bind_apply _ (Kernel.aemeasurable _), Measure.lintegral_compProd (η.measurable_coe hs)]

Premises used: MeasureTheory.Measure.bind_apply, ProbabilityTheory.Kernel.aemeasurable, ProbabilityTheory.Kernel.measurable_coe, MeasureTheory.Measure.snd_apply, MeasureTheory.Measure.lintegral_compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (α := β × γ) (Prod.snd ⁻¹' s)

Tactic:
measurable_snd hs

Premises used: measurable_snd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (α := β × γ) (Prod.snd ⁻¹' s)

Tactic:
exact measurable_snd hs

Premises used: measurable_snd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
pos :
  ∀ (a : α),
    ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
      (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s)
⊢ ∫⁻ (a : α),
      ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a ∂μ =
    ∫⁻ (a : α),
      (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) ∂μ

Tactic:
congr with a
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
pos :
  ∫⁻ (b : β), (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂(κ : (a : α) → Measure β) a
pos₁ : MeasurableSet (α := β × γ) (Prod.snd ⁻¹' s)
⊢ ∫⁻ (b : β), (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
    (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s)

Tactic:
rw [Kernel.compProd_apply]

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

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
⊢ MeasurableSet (α := β × γ) (Prod.snd ⁻¹' s)

Tactic:
measurable_snd hs

Premises used: measurable_snd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
⊢ MeasurableSet (α := β × γ) (Prod.snd ⁻¹' s)

Tactic:
exact measurable_snd hs

Premises used: measurable_snd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
rw :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
rw₁ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
rw₂ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind (mα := mβ) (map Prod.snd (μ ⊗ₘ κ)) (⇑η : (a : β) → Measure γ))
rw₃ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind.{u_2, u_3} (α := β) (mα := mβ) ((⇑(Kernel.deterministic Prod.snd ⋯) : (a : α × β) → Measure β) ∘ₘ μ ⊗ₘ κ)
      (⇑η : (a : β) → Measure γ))
rw₄ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑(η ∘ₖ Kernel.deterministic Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
rw₅ rw₆ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind.{u_2, u_3} (α := β) (mα := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) (⇑η : (a : β) → Measure γ))

Tactic:
rw [← snd_compProd μ κ, Kernel.prodMkLeft, snd, ← deterministic_comp_eq_map measurable_snd,
    comp_assoc, Kernel.comp_deterministic_eq_comap]

Premises used: MeasureTheory.Measure.snd_compProd, MeasureTheory.Measure.snd, MeasureTheory.Measure.deterministic_comp_eq_map, measurable_snd, MeasureTheory.Measure.comp_assoc, ProbabilityTheory.Kernel.comp_deterministic_eq_comap, ProbabilityTheory.Kernel.prodMkLeft
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
f : α → β
hf : Measurable f
rw : Eq (α := Measure (α × β)) (map (fun (a : α) ↦ (id a, f a)) μ) (map (fun (a : α) ↦ (a, f a)) μ)
⊢ μ ⊗ₘ Kernel.deterministic f hf = map (fun (a : α) ↦ (a, f a)) μ

Tactic:
rw [compProd_eq_comp_prod, Kernel.id, Kernel.deterministic_prod_deterministic,
    deterministic_comp_eq_map]

Premises used: ProbabilityTheory.Kernel.id, MeasureTheory.Measure.compProd_eq_comp_prod, MeasureTheory.Measure.deterministic_comp_eq_map, ProbabilityTheory.Kernel.deterministic_prod_deterministic
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
f : α → β
hf : Measurable f
⊢ Eq (α := Measure (α × β)) (map (fun (a : α) ↦ (id a, f a)) μ) (map (fun (a : α) ↦ (a, f a)) μ)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Composition.MeasureComp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
simp_rw :
  (κ ∘ₖ Kernel.const Unit (μ + ν) : (a : Unit) → Measure β) () =
    HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
      ((κ ∘ₖ Kernel.const Unit ν : (a : Unit) → Measure β) () : Measure β)
simp_rw₁ :
  (κ ∘ₖ HAdd.hAdd (α := Kernel Unit α) (Kernel.const Unit μ) (Kernel.const Unit ν) : (a : Unit) → Measure β) () =
    HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
      ((κ ∘ₖ Kernel.const Unit ν : (a : Unit) → Measure β) () : Measure β)
simp_rw₂ :
  (HAdd.hAdd (α := Kernel Unit β) (κ ∘ₖ Kernel.const Unit μ) (κ ∘ₖ Kernel.const Unit ν) : (a : Unit) → Measure β) () =
    HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
      ((κ ∘ₖ Kernel.const Unit ν : (a : Unit) → Measure β) () : Measure β)
⊢ (⇑κ : (a : α) → Measure β) ∘ₘ (μ + ν) =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν)

Tactic:
simp_rw [comp_eq_comp_const_apply, Kernel.const_add, Kernel.comp_add_right, Kernel.add_apply]

Premises used: MeasureTheory.Measure.comp_eq_comp_const_apply, ProbabilityTheory.Kernel.add_apply, ProbabilityTheory.Kernel.const_add, ProbabilityTheory.Kernel.comp_add_right