awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ Eq (α := Kernel (α × β) (α × β)) Kernel.id (deterministic Prod.fst ⋯ ×ₖ deterministic Prod.snd ⋯)
have rw : Eq (α := Kernel (α × β) (α × β)) Kernel.id (deterministic (fun (a : α × β) ↦ (a.1, a.2)) sorry)
Tactic: rw [deterministic_prod_deterministic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
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 ξ
⊢ (κ ×ₖ ξ ×ₖ η).map (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ) = κ ×ₖ (ξ ×ₖ η)
have h : ∀ (a : α),
  Eq (α := Measure (β × δ × γ))
    (((κ ×ₖ ξ ×ₖ η).map (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ) : (a : α) → Measure (β × δ × γ))
        a :
      Measure (β × δ × γ))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a : Measure (β × δ × γ))
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
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 : α
⊢ Eq (α := Measure (β × δ × γ))
    (((κ ×ₖ ξ ×ₖ η).map (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ) : (a : α) → Measure (β × δ × γ))
        a :
      Measure (β × δ × γ))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a : Measure (β × δ × γ))
have h : Eq (α := Measure (β × δ × γ))
  (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
    ((κ ×ₖ ξ ×ₖ η : (a : α) → Measure ((β × δ) × γ)) a))
  ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
Tactic: rw [map_apply _ (by fun_prop), prod_apply, prod_apply, Measure.prodAssoc_prod, prod_apply,
    prod_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
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 : α
h :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      ((κ ×ₖ ξ ×ₖ η : (a : α) → Measure ((β × δ) × γ)) a))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
⊢ Eq (α := Measure (β × δ × γ))
    (((κ ×ₖ ξ ×ₖ η).map (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ) : (a : α) → Measure (β × δ × γ))
        a :
      Measure (β × δ × γ))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a : Measure (β × δ × γ))
have h₁ : Eq (α := Measure (β × δ × γ))
  (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
    (Measure.prod ((κ ×ₖ ξ : (a : α) → Measure (β × δ)) a) ((η : (a : α) → Measure γ) a)))
  ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
Tactic: rw [map_apply _ (by fun_prop), prod_apply, prod_apply, Measure.prodAssoc_prod, prod_apply,
    prod_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
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 : α
h :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      ((κ ×ₖ ξ ×ₖ η : (a : α) → Measure ((β × δ) × γ)) a))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₁ :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      (Measure.prod ((κ ×ₖ ξ : (a : α) → Measure (β × δ)) a) ((η : (a : α) → Measure γ) a)))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
⊢ Eq (α := Measure (β × δ × γ))
    (((κ ×ₖ ξ ×ₖ η).map (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ) : (a : α) → Measure (β × δ × γ))
        a :
      Measure (β × δ × γ))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a : Measure (β × δ × γ))
have h₂ : Eq (α := Measure (β × δ × γ))
  (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
    (Measure.prod (Measure.prod ((κ : (a : α) → Measure β) a) ((ξ : (a : α) → Measure δ) a))
      ((η : (a : α) → Measure γ) a)))
  ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
Tactic: rw [map_apply _ (by fun_prop), prod_apply, prod_apply, Measure.prodAssoc_prod, prod_apply,
    prod_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
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 : α
h :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      ((κ ×ₖ ξ ×ₖ η : (a : α) → Measure ((β × δ) × γ)) a))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₁ :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      (Measure.prod ((κ ×ₖ ξ : (a : α) → Measure (β × δ)) a) ((η : (a : α) → Measure γ) a)))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₂ :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      (Measure.prod (Measure.prod ((κ : (a : α) → Measure β) a) ((ξ : (a : α) → Measure δ) a))
        ((η : (a : α) → Measure γ) a)))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
⊢ Eq (α := Measure (β × δ × γ))
    (((κ ×ₖ ξ ×ₖ η).map (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ) : (a : α) → Measure (β × δ × γ))
        a :
      Measure (β × δ × γ))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a : Measure (β × δ × γ))
have h₃ : Eq (α := Measure (β × δ × γ))
  (Measure.prod ((κ : (a : α) → Measure β) a)
    (Measure.prod ((ξ : (a : α) → Measure δ) a) ((η : (a : α) → Measure γ) a)))
  ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
Tactic: rw [map_apply _ (by fun_prop), prod_apply, prod_apply, Measure.prodAssoc_prod, prod_apply,
    prod_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
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 : α
h :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      ((κ ×ₖ ξ ×ₖ η : (a : α) → Measure ((β × δ) × γ)) a))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₁ :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      (Measure.prod ((κ ×ₖ ξ : (a : α) → Measure (β × δ)) a) ((η : (a : α) → Measure γ) a)))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₂ :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      (Measure.prod (Measure.prod ((κ : (a : α) → Measure β) a) ((ξ : (a : α) → Measure δ) a))
        ((η : (a : α) → Measure γ) a)))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₃ :
  Eq (α := Measure (β × δ × γ))
    (Measure.prod ((κ : (a : α) → Measure β) a)
      (Measure.prod ((ξ : (a : α) → Measure δ) a) ((η : (a : α) → Measure γ) a)))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
⊢ Eq (α := Measure (β × δ × γ))
    (((κ ×ₖ ξ ×ₖ η).map (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ) : (a : α) → Measure (β × δ × γ))
        a :
      Measure (β × δ × γ))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a : Measure (β × δ × γ))
have h₄ : Eq (α := Measure (β × δ × γ))
  (Measure.prod ((κ : (a : α) → Measure β) a)
    (Measure.prod ((ξ : (a : α) → Measure δ) a) ((η : (a : α) → Measure γ) a)))
  (Measure.prod ((κ : (a : α) → Measure β) a) ((ξ ×ₖ η : (a : α) → Measure (δ × γ)) a))
Tactic: rw [map_apply _ (by fun_prop), prod_apply, prod_apply, Measure.prodAssoc_prod, prod_apply,
    prod_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
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 : α
h :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      ((κ ×ₖ ξ ×ₖ η : (a : α) → Measure ((β × δ) × γ)) a))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₁ :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      (Measure.prod ((κ ×ₖ ξ : (a : α) → Measure (β × δ)) a) ((η : (a : α) → Measure γ) a)))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₂ :
  Eq (α := Measure (β × δ × γ))
    (Measure.map (α := (β × δ) × γ) (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)
      (Measure.prod (Measure.prod ((κ : (a : α) → Measure β) a) ((ξ : (a : α) → Measure δ) a))
        ((η : (a : α) → Measure γ) a)))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₃ :
  Eq (α := Measure (β × δ × γ))
    (Measure.prod ((κ : (a : α) → Measure β) a)
      (Measure.prod ((ξ : (a : α) → Measure δ) a) ((η : (a : α) → Measure γ) a)))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a)
h₄ :
  Eq (α := Measure (β × δ × γ))
    (Measure.prod ((κ : (a : α) → Measure β) a)
      (Measure.prod ((ξ : (a : α) → Measure δ) a) ((η : (a : α) → Measure γ) a)))
    (Measure.prod ((κ : (a : α) → Measure β) a) ((ξ ×ₖ η : (a : α) → Measure (δ × γ)) a))
⊢ Eq (α := Measure (β × δ × γ))
    (((κ ×ₖ ξ ×ₖ η).map (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ) : (a : α) → Measure (β × δ × γ))
        a :
      Measure (β × δ × γ))
    ((κ ×ₖ (ξ ×ₖ η) : (a : α) → Measure (β × δ × γ)) a : Measure (β × δ × γ))
have h₅ : Eq (α := Measure (β × δ × γ))
  (Measure.prod ((κ : (a : α) → Measure β) a)
    (Measure.prod ((ξ : (a : α) → Measure δ) a) ((η : (a : α) → Measure γ) a)))
  (Measure.prod ((κ : (a : α) → Measure β) a)
    (Measure.prod ((ξ : (a : α) → Measure δ) a) ((η : (a : α) → Measure γ) a)))
Tactic: rw [map_apply _ (by fun_prop), prod_apply, prod_apply, Measure.prodAssoc_prod, prod_apply,
    prod_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
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 ξ
⊢ (κ ×ₖ (ξ ×ₖ η)).map (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × δ × γ) → (β × δ) × γ) = κ ×ₖ ξ ×ₖ η
have rw : (κ ×ₖ ξ ×ₖ η).map
    (Function.comp (β := β × δ × γ) (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × δ × γ) → (β × δ) × γ)
      (⇑MeasurableEquiv.prodAssoc : (a : (β × δ) × γ) → β × δ × γ)) =
  κ ×ₖ ξ ×ₖ η
Tactic: rw [← prodAssoc_prod, ← Kernel.map_comp_right _ (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
μ : Measure δ
inst_2 : SFinite μ
⊢ η ×ₖ const β μ ∘ₖ κ = η ∘ₖ κ ×ₖ const α μ
have h : ∀ (x : α) (s : Set (γ × δ)) (ms : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((η ×ₖ const β μ ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η ∘ₖ κ ×ₖ const α μ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext x s ms
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
μ : Measure δ
inst_2 : SFinite μ
x : α
s : Set (γ × δ)
ms : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((η ×ₖ const β μ ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η ∘ₖ κ ×ₖ const α μ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (b : β),
    (((η ×ₖ const β μ : (a : β) → Measure (γ × δ)) b : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞)
      s ∂(κ : (a : α) → Measure β) x =
  (((η ∘ₖ κ ×ₖ const α μ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s
Tactic: simp_rw [comp_apply' _ _ _ ms, prod_apply' _ _ _ ms, const_apply,
  lintegral_comp _ _ _ (measurable_measure_prodMk_left ms)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
μ : Measure δ
inst_2 : SFinite μ
x : α
s : Set (γ × δ)
ms : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((η ×ₖ const β μ : (a : β) → Measure (γ × δ)) b : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (((η ∘ₖ κ ×ₖ const α μ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞)
    ((((η ×ₖ const β μ ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η ∘ₖ κ ×ₖ const α μ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∫⁻ (b : β),
    ∫⁻ (b_1 : γ),
      ((((const β μ : Kernel β δ) : (a : β) → Measure δ) b : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹' s) ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) x =
  ∫⁻ (b : γ),
    ((((const α μ : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(η ∘ₖ κ : (a : α) → Measure γ) x
Tactic: simp_rw [comp_apply' _ _ _ ms, prod_apply' _ _ _ ms, const_apply,
  lintegral_comp _ _ _ (measurable_measure_prodMk_left ms)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel β γ
inst_1 : IsSFiniteKernel η
μ : Measure δ
inst_2 : SFinite μ
x : α
s : Set (γ × δ)
ms : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((η ×ₖ const β μ : (a : β) → Measure (γ × δ)) b : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (((η ∘ₖ κ ×ₖ const α μ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s
h₁ :
  ∫⁻ (b : β),
      ∫⁻ (b_1 : γ),
        ((((const β μ : Kernel β δ) : (a : β) → Measure δ) b : Measure δ) : (a : Set δ) → ℝ≥0∞)
          (Prod.mk b_1 ⁻¹' s) ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : γ),
      ((((const α μ : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(η ∘ₖ κ : (a : α) → Measure γ) x
⊢ Eq (α := ℝ≥0∞)
    ((((η ×ₖ const β μ ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η ∘ₖ κ ×ₖ const α μ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : ∫⁻ (b : β),
    ∫⁻ (b : γ), (μ : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) x =
  ∫⁻ (b : γ), (μ : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(η ∘ₖ κ : (a : α) → Measure γ) x
Tactic: simp_rw [comp_apply' _ _ _ ms, prod_apply' _ _ _ ms, const_apply,
  lintegral_comp _ _ _ (measurable_measure_prodMk_left ms)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
μ : Measure γ
inst_1 : SFinite μ
η : Kernel β δ
inst_2 : IsSFiniteKernel η
⊢ const β μ ×ₖ η ∘ₖ κ = const α μ ×ₖ (η ∘ₖ κ)
have h : ∀ (x : α) (s : Set (γ × δ)) (ms : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((const β μ ×ₖ η ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((const α μ ×ₖ (η ∘ₖ κ) : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext x s ms
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
μ : Measure γ
inst_1 : SFinite μ
η : Kernel β δ
inst_2 : IsSFiniteKernel η
x : α
s : Set (γ × δ)
ms : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((const β μ ×ₖ η ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((const α μ ×ₖ (η ∘ₖ κ) : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (b : β),
    (((const β μ ×ₖ η : (a : β) → Measure (γ × δ)) b : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞)
      s ∂(κ : (a : α) → Measure β) x =
  (((const α μ ×ₖ (η ∘ₖ κ) : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s
Tactic: simp_rw [comp_apply' _ _ _ ms, prod_apply, Measure.prod_apply_symm ms, const_apply,
  lintegral_comp _ _ _ (measurable_measure_prodMk_right ms)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
μ : Measure γ
inst_1 : SFinite μ
η : Kernel β δ
inst_2 : IsSFiniteKernel η
x : α
s : Set (γ × δ)
ms : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((const β μ ×ₖ η : (a : β) → Measure (γ × δ)) b : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (((const α μ ×ₖ (η ∘ₖ κ) : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞)
    ((((const β μ ×ₖ η ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((const α μ ×ₖ (η ∘ₖ κ) : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∫⁻ (b : β),
    (Measure.prod (((const β μ : Kernel β γ) : (a : β) → Measure γ) b) ((η : (a : β) → Measure δ) b) :
        (a : Set (γ × δ)) → ℝ≥0∞)
      s ∂(κ : (a : α) → Measure β) x =
  (Measure.prod (((const α μ : Kernel α γ) : (a : α) → Measure γ) x) ((η ∘ₖ κ : (a : α) → Measure δ) x) :
      (a : Set (γ × δ)) → ℝ≥0∞)
    s
Tactic: simp_rw [comp_apply' _ _ _ ms, prod_apply, Measure.prod_apply_symm ms, const_apply,
  lintegral_comp _ _ _ (measurable_measure_prodMk_right ms)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
μ : Measure γ
inst_1 : SFinite μ
η : Kernel β δ
inst_2 : IsSFiniteKernel η
x : α
s : Set (γ × δ)
ms : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((const β μ ×ₖ η : (a : β) → Measure (γ × δ)) b : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (((const α μ ×ₖ (η ∘ₖ κ) : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s
h₁ :
  ∫⁻ (b : β),
      (Measure.prod (((const β μ : Kernel β γ) : (a : β) → Measure γ) b) ((η : (a : β) → Measure δ) b) :
          (a : Set (γ × δ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (Measure.prod (((const α μ : Kernel α γ) : (a : α) → Measure γ) x) ((η ∘ₖ κ : (a : α) → Measure δ) x) :
        (a : Set (γ × δ)) → ℝ≥0∞)
      s
⊢ Eq (α := ℝ≥0∞)
    ((((const β μ ×ₖ η ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((const α μ ×ₖ (η ∘ₖ κ) : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : ∫⁻ (b : β),
    ∫⁻ (y : δ),
      ((((const β μ : Kernel β γ) : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
        ((fun (x : γ) ↦ (x, y)) ⁻¹' s) ∂(η : (a : β) → Measure δ) b ∂(κ : (a : α) → Measure β) x =
  ∫⁻ (y : δ),
    ((((const α μ : Kernel α γ) : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞)
      ((fun (x : γ) ↦ (x, y)) ⁻¹' s) ∂(η ∘ₖ κ : (a : α) → Measure δ) x
Tactic: simp_rw [comp_apply' _ _ _ ms, prod_apply, Measure.prod_apply_symm ms, const_apply,
  lintegral_comp _ _ _ (measurable_measure_prodMk_right ms)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
δ : Type u_6
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
μ : Measure γ
inst_1 : SFinite μ
η : Kernel β δ
inst_2 : IsSFiniteKernel η
x : α
s : Set (γ × δ)
ms : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((const β μ ×ₖ η : (a : β) → Measure (γ × δ)) b : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (((const α μ ×ₖ (η ∘ₖ κ) : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s
h₁ :
  ∫⁻ (b : β),
      (Measure.prod (((const β μ : Kernel β γ) : (a : β) → Measure γ) b) ((η : (a : β) → Measure δ) b) :
          (a : Set (γ × δ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (Measure.prod (((const α μ : Kernel α γ) : (a : α) → Measure γ) x) ((η ∘ₖ κ : (a : α) → Measure δ) x) :
        (a : Set (γ × δ)) → ℝ≥0∞)
      s
h₂ :
  ∫⁻ (b : β),
      ∫⁻ (y : δ),
        ((((const β μ : Kernel β γ) : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
          ((fun (x : γ) ↦ (x, y)) ⁻¹' s) ∂(η : (a : β) → Measure δ) b ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (y : δ),
      ((((const α μ : Kernel α γ) : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞)
        ((fun (x : γ) ↦ (x, y)) ⁻¹' s) ∂(η ∘ₖ κ : (a : α) → Measure δ) x
⊢ Eq (α := ℝ≥0∞)
    ((((const β μ ×ₖ η ∘ₖ κ : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((const α μ ×ₖ (η ∘ₖ κ) : (a : α) → Measure (γ × δ)) x : Measure (γ × δ)) : (a : Set (γ × δ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : ∫⁻ (b : β),
    ∫⁻ (y : δ),
      (μ : (a : Set γ) → ℝ≥0∞)
        ((fun (x : γ) ↦ (x, y)) ⁻¹' s) ∂(η : (a : β) → Measure δ) b ∂(κ : (a : α) → Measure β) x =
  ∫⁻ (y : δ), (μ : (a : Set γ) → ℝ≥0∞) ((fun (x : γ) ↦ (x, y)) ⁻¹' s) ∂(η ∘ₖ κ : (a : α) → Measure δ) x
Tactic: simp_rw [comp_apply' _ _ _ ms, prod_apply, Measure.prod_apply_symm ms, const_apply,
  lintegral_comp _ _ _ (measurable_measure_prodMk_right ms)]