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 α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsMarkovKernel η
h :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := Measure β) (((κ ∥ₖ η).fst ∘ₖ copy α : (a : α) → Measure β) a : Measure β)
      ((κ : (a : α) → Measure β) a : Measure β)
⊢ (κ ∥ₖ η).fst ∘ₖ copy α = κ

Tactic:
ext a : 1
-- 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 η
a : α
⊢ Measurable.{u_1, u_2} (α := α × α) (β := Measure β) (⇑(κ ∥ₖ η).fst : (a : α × α) → Measure β)

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 : IsMarkovKernel η
a : α
h :
  Eq.{u_2 + 1} (α := Measure β)
    (Measure.map (α := β × γ) Prod.fst
      (Measure.prod ((κ : (a : α) → Measure β) (a, a).1) ((η : (a : α) → Measure γ) (a, a).2)))
    ((κ : (a : α) → Measure β) a)
⊢ Eq.{u_2 + 1} (α := Measure β) (((κ ∥ₖ η).fst ∘ₖ copy α : (a : α) → Measure β) a : Measure β)
    ((κ : (a : α) → Measure β) a : Measure β)

Tactic:
rw [comp_apply, copy_apply, Measure.dirac_bind (by fun_prop), fst_apply, parallelComp_apply]

Premises used: MeasureTheory.Measure.dirac_bind, ProbabilityTheory.Kernel.fst_apply, ProbabilityTheory.Kernel.copy_apply, ProbabilityTheory.Kernel.comp_apply, 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 : IsMarkovKernel η
a : α
⊢ Eq.{u_2 + 1} (α := Measure β)
    (Measure.map (α := β × γ) Prod.fst
      (Measure.prod ((κ : (a : α) → Measure β) (a, a).1) ((η : (a : α) → Measure γ) (a, a).2)))
    ((κ : (a : α) → Measure β) a)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsMarkovKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
h :
  ∀ (x : α) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((((κ ×ₖ η).snd : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        ((((η : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (κ ×ₖ η).snd = η

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 γ
κ : Kernel α β
inst : IsMarkovKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
x : α
s : Set γ
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((((κ ×ₖ η).snd : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [snd_apply, prod_apply]

Premises used: ProbabilityTheory.Kernel.prod_apply, ProbabilityTheory.Kernel.snd_apply
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst : IsSFiniteKernel κ
η : Kernel β δ
inst_1 : IsSFiniteKernel η
f : α → β
hf : Measurable f
h :
  ∀ (x : α),
    Eq (α := Measure (γ × δ)) (((κ ×ₖ η).comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
      ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
⊢ (κ ×ₖ η).comap f hf = κ.comap f hf ×ₖ η.comap f hf

Tactic:
ext1 x
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
inst : IsSFiniteKernel κ
η : Kernel β δ
inst_1 : IsSFiniteKernel η
f : α → β
hf : Measurable f
x : α
h :
  Eq (α := Measure (γ × δ)) ((κ ×ₖ η : (a : β) → Measure (γ × δ)) (f x) : Measure (γ × δ))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
h₁ :
  Eq (α := Measure (γ × δ)) (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η : (a : β) → Measure δ) (f x)))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x)
h₂ :
  Eq (α := Measure (γ × δ)) (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η : (a : β) → Measure δ) (f x)))
    (Measure.prod ((κ.comap f hf : (a : α) → Measure γ) x) ((η.comap f hf : (a : α) → Measure δ) x))
h₃ :
  Eq (α := Measure (γ × δ)) (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η : (a : β) → Measure δ) (f x)))
    (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η.comap f hf : (a : α) → Measure δ) x))
h₄ h₅ :
  Eq (α := Measure (γ × δ)) (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η : (a : β) → Measure δ) (f x)))
    (Measure.prod ((κ : (a : β) → Measure γ) (f x)) ((η : (a : β) → Measure δ) (f x)))
⊢ Eq (α := Measure (γ × δ)) (((κ ×ₖ η).comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))
    ((κ.comap f hf ×ₖ η.comap f hf : (a : α) → Measure (γ × δ)) x : Measure (γ × δ))

Tactic:
rw [comap_apply, prod_apply, prod_apply, comap_apply, comap_apply]

Premises used: ProbabilityTheory.Kernel.prod_apply, ProbabilityTheory.Kernel.comap_apply
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α δ
inst_1 : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
h :
  ∀ (x : α),
    Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
      (((κ ×ₖ η).map (Prod.map f g) : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
⊢ Eq (α := Kernel α (γ × ε)) (κ.map f ×ₖ η.map g) ((κ ×ₖ η).map (Prod.map f g))

Tactic:
ext1 x
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ε : Type u_6
mε : MeasurableSpace ε
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α δ
inst_1 : IsSFiniteKernel η
f : β → γ
hf : Measurable f
g : δ → ε
hg : Measurable g
x : α
h :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.map (Prod.map f g) ((κ ×ₖ η : (a : α) → Measure (β × δ)) x) : Measure (γ × ε))
h₁ :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.map (Prod.map f g) (Measure.prod ((κ : (a : α) → Measure β) x) ((η : (a : α) → Measure δ) x)) :
      Measure (γ × ε))
h₂ :
  Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)) :
      Measure (γ × ε))
h₃ :
  Eq (α := Measure (γ × ε))
    (Measure.prod (((κ.map f : Kernel α γ) : (a : α) → Measure γ) x) (((η.map g : Kernel α ε) : (a : α) → Measure ε) x))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)))
h₄ :
  Eq (α := Measure (γ × ε))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (((η.map g : Kernel α ε) : (a : α) → Measure ε) x))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)))
h₅ h₆ :
  Eq (α := Measure (γ × ε))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)))
    (Measure.prod (Measure.map f ((κ : (a : α) → Measure β) x)) (Measure.map g ((η : (a : α) → Measure δ) x)))
⊢ Eq (α := Measure (γ × ε)) ((κ.map f ×ₖ η.map g : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))
    (((κ ×ₖ η).map (Prod.map f g) : (a : α) → Measure (γ × ε)) x : Measure (γ × ε))

Tactic:
rw [map_apply _ (hf.prodMap hg), prod_apply κ, ← Measure.map_prod_map _ _ hf hg, prod_apply,
    map_apply _ hf, map_apply _ hg]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.prod_apply, MeasureTheory.Measure.map_prod_map, Measurable.prodMap
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
f : β → δ
hf : Measurable f
rw : Eq (α := Kernel α (δ × γ)) (κ.map f ×ₖ η) (κ.map f ×ₖ η.map id)
rw₁ rw₂ : Eq (α := Kernel α (δ × γ)) (κ.map f ×ₖ η) (κ.map f ×ₖ η)
⊢ Eq (α := Kernel α (δ × γ)) (κ.map f ×ₖ η) ((κ ×ₖ η).map (Prod.map f id))

Tactic:
rw [← map_prod_map _ _ hf measurable_id, map_id]

Premises used: measurable_id, ProbabilityTheory.Kernel.map_prod_map, ProbabilityTheory.Kernel.map_id
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
rw :
  ∀ (a : α × γ) (f : δ × β → ℝ≥0∞),
    Measurable f →
      ∫⁻ (b : δ × β), f b ∂((prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯ : (a : α × γ) → Measure (δ × β)) a =
        ∫⁻ (b : δ × β), f b ∂((prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap : (a : α × γ) → Measure (δ × β)) a
⊢ (prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯ = (prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap

Tactic:
rw [ext_fun_iff]

Premises used: ProbabilityTheory.Kernel.ext_fun_iff
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
rw :
  ∫⁻ (b : δ),
      ∫⁻ (c : β),
        f
          (b,
            c) ∂(prodMkLeft γ κ : (a : γ × α) → Measure β) x.swap ∂(prodMkRight α η : (a : γ × α) → Measure δ) x.swap =
    ∫⁻ (b : β),
      ∫⁻ (c : δ),
        f (b, c).swap ∂(prodMkLeft α η : (a : α × γ) → Measure δ) x ∂(prodMkRight γ κ : (a : α × γ) → Measure β) x
hg : Measurable (β := ℝ≥0∞) fun (a : β × δ) ↦ f a.swap
⊢ ∫⁻ (b : δ × β), f b ∂((prodMkRight α η ×ₖ prodMkLeft γ κ).comap Prod.swap ⋯ : (a : α × γ) → Measure (δ × β)) x =
    ∫⁻ (b : δ × β), f b ∂((prodMkRight γ κ ×ₖ prodMkLeft α η).map Prod.swap : (a : α × γ) → Measure (δ × β)) x

Tactic:
rw [lintegral_comap, lintegral_map _ measurable_swap _ hf, lintegral_prod _ _ _ hf,
    lintegral_prod]

Premises used: ProbabilityTheory.Kernel.lintegral_map, ProbabilityTheory.Kernel.lintegral_prod, ProbabilityTheory.Kernel.lintegral_comap, measurable_swap
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (a : β × δ) ↦ f a.swap

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
simp :
  ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(κ : (a : α) → Measure β) x.1 ∂(η : (a : γ) → Measure δ) x.2 =
    ∫⁻ (b : β), ∫⁻ (c : δ), f (c, b) ∂(η : (a : γ) → Measure δ) x.2 ∂(κ : (a : α) → Measure β) x.1
⊢ ∫⁻ (b : δ),
      ∫⁻ (c : β),
        f
          (b,
            c) ∂(prodMkLeft γ κ : (a : γ × α) → Measure β) x.swap ∂(prodMkRight α η : (a : γ × α) → Measure δ) x.swap =
    ∫⁻ (b : β),
      ∫⁻ (c : δ),
        f (b, c).swap ∂(prodMkLeft α η : (a : α × γ) → Measure δ) x ∂(prodMkRight γ κ : (a : α × γ) → Measure β) x

Tactic:
simp only [prodMkRight_apply, Prod.fst_swap, Prod.swap_prod_mk, lintegral_prodMkLeft,
    Prod.snd_swap]

Premises used: Prod.fst_swap, Prod.swap_prod_mk, ProbabilityTheory.Kernel.prodMkRight_apply, Prod.snd_swap, ProbabilityTheory.Kernel.lintegral_prodMkLeft
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(κ : (a : α) → Measure β) x.1 ∂(η : (a : γ) → Measure δ) x.2 =
    ∫⁻ (b : β), ∫⁻ (c : δ), f (c, b) ∂(η : (a : γ) → Measure δ) x.2 ∂(κ : (a : α) → Measure β) x.1

Tactic:
(lintegral_lintegral_swap ?_).symm

Premises used: MeasureTheory.lintegral_lintegral_swap, Eq.symm
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
refine :
  AEMeasurable (α := β × δ) (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (Function.uncurry fun (c : β) (b : δ) ↦ f (b, c))
    (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2))
⊢ ∫⁻ (b : δ), ∫⁻ (c : β), f (b, c) ∂(κ : (a : α) → Measure β) x.1 ∂(η : (a : γ) → Measure δ) x.2 =
    ∫⁻ (b : β), ∫⁻ (c : δ), f (c, b) ∂(η : (a : γ) → Measure δ) x.2 ∂(κ : (a : α) → Measure β) x.1

Tactic:
refine (lintegral_lintegral_swap ?_).symm

Premises used: MeasureTheory.lintegral_lintegral_swap, Eq.symm
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α × γ
f : δ × β → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (α := β × δ) (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (Function.uncurry fun (c : β) (b : δ) ↦ f (b, c))
    (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2))

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 α β
η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
rw :
  ∀ (a : α) (f : γ × β → ℝ≥0∞),
    Measurable f →
      ∫⁻ (b : γ × β), f b ∂((κ ×ₖ η).map Prod.swap : (a : α) → Measure (γ × β)) a =
        ∫⁻ (b : γ × β), f b ∂(η ×ₖ κ : (a : α) → Measure (γ × β)) a
⊢ (κ ×ₖ η).map Prod.swap = η ×ₖ κ

Tactic:
rw [ext_fun_iff]

Premises used: ProbabilityTheory.Kernel.ext_fun_iff
-- 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 η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
rw :
  ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c).swap ∂(η : (a : α) → Measure γ) x ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : γ), ∫⁻ (c : β), f (b, c) ∂(κ : (a : α) → Measure β) x ∂(η : (a : α) → Measure γ) x
hg : Measurable (β := ℝ≥0∞) fun (a : β × γ) ↦ f a.swap
⊢ ∫⁻ (b : γ × β), f b ∂((κ ×ₖ η).map Prod.swap : (a : α) → Measure (γ × β)) x =
    ∫⁻ (b : γ × β), f b ∂(η ×ₖ κ : (a : α) → Measure (γ × β)) x

Tactic:
rw [lintegral_map _ measurable_swap _ hf, lintegral_prod, lintegral_prod _ _ _ hf]

Premises used: ProbabilityTheory.Kernel.lintegral_map, ProbabilityTheory.Kernel.lintegral_prod, measurable_swap
-- 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 η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (a : β × γ) ↦ f a.swap

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 α β
η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c).swap ∂(η : (a : α) → Measure γ) x ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : γ), ∫⁻ (c : β), f (b, c) ∂(κ : (a : α) → Measure β) x ∂(η : (a : α) → Measure γ) x

Tactic:
(lintegral_lintegral_swap ?_).symm

Premises used: MeasureTheory.lintegral_lintegral_swap, Prod.swap, Eq.symm
-- 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 η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
refine :
  AEMeasurable (α := γ × β) (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (Function.uncurry fun (c : γ) (b : β) ↦ f (b, c).swap)
    (Measure.prod ((η : (a : α) → Measure γ) x) ((κ : (a : α) → Measure β) x))
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c).swap ∂(η : (a : α) → Measure γ) x ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : γ), ∫⁻ (c : β), f (b, c) ∂(κ : (a : α) → Measure β) x ∂(η : (a : α) → Measure γ) x

Tactic:
refine (lintegral_lintegral_swap ?_).symm

Premises used: MeasureTheory.lintegral_lintegral_swap, Eq.symm
-- 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 η
x : α
f : γ × β → ℝ≥0∞
hf : Measurable f
⊢ AEMeasurable (α := γ × β) (β := ℝ≥0∞) (_m := Prod.instMeasurableSpace)
    (Function.uncurry fun (c : γ) (b : β) ↦ f (b, c).swap)
    (Measure.prod ((η : (a : α) → Measure γ) x) ((κ : (a : α) → Measure β) x))

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 η
⊢ (κ ×ₖ η).map (⇑MeasurableEquiv.prodComm : (a : β × γ) → γ × β) = η ×ₖ κ

Tactic:
map_prod_swap κ η

Premises used: Prod.swap, ProbabilityTheory.Kernel.map_prod_swap
-- 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 η
rw : (κ ×ₖ η).map Prod.swap = η ×ₖ κ
rw₁ rw₂ : η ×ₖ κ = η ×ₖ κ
⊢ swap β γ ∘ₖ (κ ×ₖ η) = η ×ₖ κ

Tactic:
rw [swap_comp_eq_map, map_prod_swap]

Premises used: ProbabilityTheory.Kernel.swap_comp_eq_map, ProbabilityTheory.Kernel.map_prod_swap
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ (a : α) (s : Set (β × γ)),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((deterministic f hf ×ₖ deterministic g hg : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
              (a : Set (β × γ)) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        ((((deterministic (fun (a : α) ↦ (f a, g a)) ⋯ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
              (a : Set (β × γ)) → ℝ≥0∞)
            s :
          ℝ≥0∞)
⊢ deterministic f hf ×ₖ deterministic g hg = deterministic (fun (a : α) ↦ (f a, g a)) ⋯

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
a : α
s : Set (β × γ)
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((Measure.prod ((deterministic f hf : (a : α) → Measure β) a) ((deterministic g hg : (a : α) → Measure γ) a) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((deterministic (fun (a : α) ↦ (f a, g a)) ⋯ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((Measure.prod (Measure.dirac (f a)) (Measure.dirac (g a)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.dirac (f a, g a) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((deterministic f hf ×ₖ deterministic g hg : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((deterministic (fun (a : α) ↦ (f a, g a)) ⋯ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp_rw [prod_apply, deterministic_apply, Measure.dirac_prod_dirac]

Premises used: ProbabilityTheory.Kernel.prod_apply, ProbabilityTheory.Kernel.deterministic_apply, MeasureTheory.Measure.dirac_prod_dirac
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
rw : Eq (α := Kernel (α × β) (α × β)) Kernel.id (deterministic (fun (a : α × β) ↦ (a.1, a.2)) ⋯)
⊢ Eq (α := Kernel (α × β) (α × β)) Kernel.id (deterministic Prod.fst ⋯ ×ₖ deterministic Prod.snd ⋯)

Tactic:
rw [deterministic_prod_deterministic]

Premises used: ProbabilityTheory.Kernel.deterministic_prod_deterministic
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ Eq (α := Kernel (α × β) (α × β)) Kernel.id (deterministic (fun (a : α × β) ↦ (a.1, a.2)) ⋯)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
ξ : Kernel α δ
inst_2 : IsSFiniteKernel ξ
h :
  ∀ (a : α),
    Eq (α := Measure (β × δ × γ))
      (((κ ×ₖ ξ ×ₖ η).map (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ) : (a : α) → Measure (β × δ × γ))
          a :
        Measure (β × δ × γ))
      ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a : Measure (β × δ × γ))
⊢ (κ ×ₖ ξ ×ₖ η).map (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ) = κ ×ₖ (ξ ×ₖ η)

Tactic:
ext1 a
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
ξ : Kernel α δ
inst_2 : IsSFiniteKernel ξ
a : α
⊢ Measurable (α := (β × δ) × γ) (β := β × δ × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)

Tactic:
fun_prop