awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
b : β
h :
  Measurable (β := ℝ≥0∞) fun (x : α) ↦
    (((κ : (a : β) → Measure γ) (a, b).2 : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
    ((((Kernel.id ∥ₖ κ : (a : α × β) → Measure (α × γ)) (a, b) : Measure (α × γ)) : (a : Set (α × γ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Kernel.parallelComp_apply, Kernel.id_apply, Measure.prod_apply hs, lintegral_dirac']

Premises used: MeasureTheory.lintegral_dirac', MeasureTheory.Measure.prod_apply, ProbabilityTheory.Kernel.id_apply, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite ν
κ : Kernel β γ
inst_1 : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
b : β
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦
    (((κ : (a : β) → Measure γ) (a, b).2 : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s)

Tactic:
measurable_measure_prodMk_left hs

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

Tactic:
exact measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
rw rw₁ :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
⊢ Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))

Tactic:
rw [Measure.prod_swap]

Premises used: MeasureTheory.Measure.prod_swap
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
⊢ Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))

Tactic:
have h1 : (κ ∘ₘ μ).prod ν = (ν.prod (κ ∘ₘ μ)).map Prod.swap := by rw [Measure.prod_swap]
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
h1 :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
rw rw₁ :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
⊢ Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))

Tactic:
rw [Measure.prod_swap]

Premises used: MeasureTheory.Measure.prod_swap
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
h1 :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
rw :
  Eq (α := Measure (γ × β))
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.deterministic Prod.swap ⋯) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
rw₁ rw₂ :
  Eq (α := Measure (γ × β))
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
⊢ Eq (α := Measure (γ × β))
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))

Tactic:
rw [Kernel.swap, Measure.deterministic_comp_eq_map]

Premises used: MeasureTheory.Measure.deterministic_comp_eq_map, ProbabilityTheory.Kernel.swap
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
h1 :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
rw :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
rw₁ :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
    ((⇑(Kernel.swap β γ ∘ₖ (Kernel.id ∥ₖ κ)) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
rw₂ rw₃ :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
    ((⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) : (a : β × α) → Measure (γ × β)) ∘ₘ ν.prod μ)
⊢ Eq (α := Measure (γ × β))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))

Tactic:
rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]

Premises used: MeasureTheory.Measure.comp_assoc, ProbabilityTheory.Kernel.swap_parallelComp
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
h1 :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
rw :
  Eq (α := Measure (γ × β))
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.deterministic Prod.swap ⋯) : (a : β × γ) → Measure (γ × β)))
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
rw₁ rw₂ :
  Eq (α := Measure (γ × β)) (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
⊢ Eq (α := Measure (γ × β))
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))

Tactic:
rw [Kernel.swap, Measure.deterministic_comp_eq_map]

Premises used: MeasureTheory.Measure.deterministic_comp_eq_map, ProbabilityTheory.Kernel.swap
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
h1 :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
calc :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
calc₁ :
  Eq (α := Measure (γ × β))
    (bind (mα := Prod.instMeasurableSpace) (map Prod.swap (ν.prod μ))
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
calc₂ :
  Eq (α := Measure (γ × β))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap β α) : (a : β × α) → Measure (α × β)) ∘ₘ ν.prod μ)
      (⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)))
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
calc₃ :
  Eq (α := Measure (γ × β))
    (bind (α := β × γ) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ)
      (⇑(Kernel.swap β γ) : (a : β × γ) → Measure (γ × β)))
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
⊢ Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))

Tactic:
calc (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
    _ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
      rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
    _ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]

Premises used: MeasureTheory.Measure.bind, ProbabilityTheory.Kernel.id, ProbabilityTheory.Kernel.swap, MeasureTheory.Measure.prod, ProbabilityTheory.Kernel.parallelComp, MeasureTheory.Measure.map, Prod.swap, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
h1 :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
⊢ Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))

Tactic:
have h2 : (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν) = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
    calc (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
    _ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
      rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
    _ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
h1 :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
h2 :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (map Prod.swap ((⇑(Kernel.id ∥ₖ κ) : (a : β × α) → Measure (β × γ)) ∘ₘ ν.prod μ))
⊢ Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)

Tactic:
rw [← Measure.prod_comp_right, ← h1] at h2

Premises used: MeasureTheory.Measure.prod_comp_right
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
h1 :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
h2 :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
⊢ Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)

Tactic:
h2.symm

Premises used: Eq.symm
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α γ
inst_2 : IsSFiniteKernel κ
h1 :
  Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    (map Prod.swap (ν.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ)))
h2 :
  Eq (α := Measure (γ × β)) ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)
    (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
⊢ Eq (α := Measure (γ × β)) (Measure.prod ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ν)
    ((⇑(κ ∥ₖ Kernel.id) : (a : α × β) → Measure (γ × β)) ∘ₘ μ.prod ν)

Tactic:
exact h2.symm

Premises used: Eq.symm
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
pos : ∀ (hμ : SFinite μ), (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
neg : ∀ (hμ : ¬SFinite μ), (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)
⊢ (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)

Tactic:
by_cases hμ : SFinite μ

Premises used: MeasureTheory.SFinite
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
hμ : ¬SFinite μ
⊢ (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)

Tactic:
simp [hμ]
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
hμ : SFinite μ
pos :
  bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) =
    μ ⊗ₘ (η ∘ₖ κ)
pos₁ :
  Eq (α := Measure (α × γ))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)))
    ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
pos₂ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∥ₖ η ∘ₖ (Kernel.id ×ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
    ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
pos₃ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∘ₖ Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
    ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
pos₄ pos₅ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
    ((⇑(Kernel.id ×ₖ (η ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
⊢ (⇑(Kernel.id ∥ₖ η) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)

Tactic:
rw [Measure.compProd_eq_comp_prod, Measure.compProd_eq_comp_prod, Measure.comp_assoc,
    Kernel.parallelComp_comp_prod, Kernel.id_comp]

Premises used: ProbabilityTheory.Kernel.parallelComp_comp_prod, MeasureTheory.Measure.compProd_eq_comp_prod, MeasureTheory.Measure.comp_assoc, ProbabilityTheory.Kernel.id_comp
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
rw :
  Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf ∘ₖ (Kernel.id ×ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
rw₁ :
  Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    ((⇑(Kernel.id ∘ₖ Kernel.id ×ₖ (Kernel.deterministic f hf ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
rw₂ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ×ₖ κ.map f) : (a : α) → Measure (α × γ)) ∘ₘ μ)
    ((⇑(Kernel.id ∘ₖ Kernel.id ×ₖ (Kernel.deterministic f hf ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
rw₃ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ×ₖ κ.map f) : (a : α) → Measure (α × γ)) ∘ₘ μ)
    ((⇑(Kernel.id ×ₖ (Kernel.deterministic f hf ∘ₖ κ)) : (a : α) → Measure (α × γ)) ∘ₘ μ)
rw₄ rw₅ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ×ₖ κ.map f) : (a : α) → Measure (α × γ)) ∘ₘ μ)
    ((⇑(Kernel.id ×ₖ κ.map f) : (a : α) → Measure (α × γ)) ∘ₘ μ)
⊢ Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))

Tactic:
rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
      Kernel.id_comp, Kernel.deterministic_comp_eq_map]

Premises used: ProbabilityTheory.Kernel.parallelComp_comp_prod, ProbabilityTheory.Kernel.deterministic_comp_eq_map, MeasureTheory.Measure.compProd_eq_comp_prod, MeasureTheory.Measure.comp_assoc, ProbabilityTheory.Kernel.id_comp
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
rw rw₁ :
  Eq (α := Measure (α × γ))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
⊢ Eq (α := Measure (α × γ))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
    ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)

Tactic:
rw [compProd_eq_comp_prod]

Premises used: MeasureTheory.Measure.compProd_eq_comp_prod
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
rw :
  Eq (α := Measure (α × γ))
    ((⇑(Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
    (map (Prod.map id f) (μ ⊗ₘ κ))
rw₁ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.deterministic (Prod.map id f) ⋯) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
    (map (Prod.map id f) (μ ⊗ₘ κ))
rw₂ rw₃ : Eq (α := Measure (α × γ)) (map (Prod.map id f) (μ ⊗ₘ κ)) (map (Prod.map id f) (μ ⊗ₘ κ))
⊢ Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
    (map (Prod.map id f) (μ ⊗ₘ κ))

Tactic:
rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map]

Premises used: ProbabilityTheory.Kernel.id, MeasureTheory.Measure.deterministic_comp_eq_map, ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic
-- Module: Mathlib.Probability.Kernel.Composition.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
calc :
  Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f)
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
calc₁ :
  Eq (α := Measure (α × γ))
    (bind (α := α × β) (mα := Prod.instMeasurableSpace) ((⇑(Kernel.id ×ₖ κ) : (a : α) → Measure (α × β)) ∘ₘ μ)
      (⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)))
    ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
calc₂ :
  Eq (α := Measure (α × γ)) ((⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) : (a : α × β) → Measure (α × γ)) ∘ₘ μ ⊗ₘ κ)
    (map (Prod.map id f) (μ ⊗ₘ κ))
⊢ Eq (α := Measure (α × γ)) (μ ⊗ₘ κ.map f) (map (Prod.map id f) (μ ⊗ₘ κ))

Tactic:
calc μ ⊗ₘ (κ.map f)
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ×ₖ κ) ∘ₘ μ := by
    rw [comp_assoc, Kernel.parallelComp_comp_prod, compProd_eq_comp_prod,
      Kernel.id_comp, Kernel.deterministic_comp_eq_map]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (μ ⊗ₘ κ) := by rw [compProd_eq_comp_prod]
  _ = (μ ⊗ₘ κ).map (Prod.map id f) := by
    rw [Kernel.id, Kernel.deterministic_parallelComp_deterministic, deterministic_comp_eq_map]

Premises used: ProbabilityTheory.Kernel.map, id, ProbabilityTheory.Kernel.deterministic, Prod.map, ProbabilityTheory.Kernel.id, ProbabilityTheory.Kernel.parallelComp, MeasureTheory.Measure.map, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.prod
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
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 δ
f_1 : β → γ
g : γ → α
κ : Kernel α β
f : β → γ
hf : Measurable f
⊢ Measurable.{u_1, u_4} (β := Measure γ) fun (a : α) ↦ Measure.map f ((κ : (a : α) → Measure β) a)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β → γ
hf : ¬Measurable f
⊢ Eq (α := Kernel α γ) (κ.map f) 0

Tactic:
simp [map, hf]

Premises used: ProbabilityTheory.Kernel.map