awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
have rw : ∫⁻ (y : β),
    (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                  deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
                (Kernel.id ∥ₖ copy β) :
              (a : α × β) → Measure (β × γ))
            ((a, a).1, y) :
          Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s ∂(κ : (a : α) → Measure β) (a, a).2 =
  ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
Tactic: rw [compProd, comp_apply, copy_apply, Measure.dirac_bind (by fun_prop), comp_apply,
    parallelComp_apply, Kernel.id_apply, Measure.bind_apply hs (by fun_prop),
    lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable, lintegral_dirac']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
rw :
  ∫⁻ (y : β),
      (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                    deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)
                      ⋯ ∘ₖ
                  (Kernel.id ∥ₖ copy β) :
                (a : α × β) → Measure (β × γ))
              ((a, a).1, y) :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) (a, a).2 =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
have hf : Measurable (β := ℝ≥0∞) fun (x : α) ↦
  ∫⁻ (y : β),
    (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                  deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
                (Kernel.id ∥ₖ copy β) :
              (a : α × β) → Measure (β × γ))
            (x, y) :
          Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s ∂(κ : (a : α) → Measure β) (a, a).2
Tactic: rw [compProd, comp_apply, copy_apply, Measure.dirac_bind (by fun_prop), comp_apply,
    parallelComp_apply, Kernel.id_apply, Measure.bind_apply hs (by fun_prop),
    lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable, lintegral_dirac']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦
    ∫⁻ (y : β),
      (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                    deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)
                      ⋯ ∘ₖ
                  (Kernel.id ∥ₖ copy β) :
                (a : α × β) → Measure (β × γ))
              (x, y) :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) (a, a).2
have hf : Measurable (β := ℝ≥0∞) fun (p : α × β) ↦
  (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) sorry ∘ₖ
              (Kernel.id ∥ₖ copy β) :
            (a : α × β) → Measure (β × γ))
          p :
        Measure (β × γ)) :
      (a : Set (β × γ)) → ℝ≥0∞)
    s
Tactic: suffices Measurable fun p : α × β ↦
      (swap γ β ∘ₖ (η ∥ₖ Kernel.id)
        ∘ₖ deterministic MeasurableEquiv.prodAssoc.symm (MeasurableEquiv.measurable _)
        ∘ₖ (Kernel.id ∥ₖ copy β)) p s by fun_prop
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
⊢ ∫⁻ (y : β),
      (((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                    deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)
                      ⋯ ∘ₖ
                  (Kernel.id ∥ₖ copy β) :
                (a : α × β) → Measure (β × γ))
              ((a, a).1, y) :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) (a, a).2 =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
have e_f : ∀ (b : β),
  Eq (α := ℝ≥0∞)
    ((((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                    deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)
                      sorry ∘ₖ
                  (Kernel.id ∥ₖ copy β) :
                (a : α × β) → Measure (β × γ))
              ((a, a).1, b) :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
Tactic: congr with b
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
b : β
⊢ Eq (α := ℝ≥0∞)
    ((((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
                    deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β)
                      ⋯ ∘ₖ
                  (Kernel.id ∥ₖ copy β) :
                (a : α × β) → Measure (β × γ))
              ((a, a).1, b) :
            Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
have e_f : Eq (α := ℝ≥0∞)
  ((Measure.bind (α := γ × β) (mα := Prod.instMeasurableSpace)
          ((η ∥ₖ Kernel.id : (a : (α × β) × β) → Measure (γ × β))
            ((MeasurableEquiv.symm MeasurableEquiv.prodAssoc : (a : α × β × β) → (α × β) × β)
              (((a, a).1, b).1, ((a, a).1, b).2, ((a, a).1, b).2)))
          (⇑(swap γ β) : (a : γ × β) → Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
Tactic: rw [comp_apply, parallelComp_apply, Kernel.id_apply, copy_apply, Measure.dirac_prod_dirac,
    Measure.dirac_bind (by fun_prop), comp_apply, deterministic_apply (by fun_prop),
    Measure.dirac_bind (by fun_prop), comp_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
b : β
⊢ Eq (α := ℝ≥0∞)
    ((Measure.bind (α := γ × β) (mα := Prod.instMeasurableSpace)
            ((η ∥ₖ Kernel.id : (a : (α × β) × β) → Measure (γ × β))
              ((MeasurableEquiv.symm MeasurableEquiv.prodAssoc : (a : α × β × β) → (α × β) × β)
                (((a, a).1, b).1, ((a, a).1, b).2, ((a, a).1, b).2)))
            (⇑(swap γ β) : (a : γ × β) → Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
have e_f : Eq (α := ℝ≥0∞)
  ((Measure.bind (α := γ × β) (mα := Prod.instMeasurableSpace)
          ((η ∥ₖ Kernel.id : (a : (α × β) × β) → Measure (γ × β)) ((a, b), b))
          (⇑(swap γ β) : (a : γ × β) → Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
Tactic: simp only [MeasurableEquiv.prodAssoc, MeasurableEquiv.symm_mk, MeasurableEquiv.coe_mk,
    Equiv.prodAssoc_symm_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
b : β
⊢ Eq (α := ℝ≥0∞)
    ((Measure.bind (α := γ × β) (mα := Prod.instMeasurableSpace)
            ((η ∥ₖ Kernel.id : (a : (α × β) × β) → Measure (γ × β)) ((a, b), b))
            (⇑(swap γ β) : (a : γ × β) → Measure (β × γ)) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
have e_f : ∫⁻ (x : γ),
    ∫⁻ (y : β),
      (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
  (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: rw [parallelComp_apply, Kernel.id_apply, Measure.bind_apply hs (by fun_prop),
    lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
b : β
x : γ
⊢ ∫⁻ (y : β),
      (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s ∂Measure.dirac b =
    (Prod.mk b ⁻¹' s).indicator 1 x
have rw : Eq (α := ℝ≥0∞)
  ((((swap γ β : (a : γ × β) → Measure (β × γ)) (x, b) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
  ((Prod.mk b ⁻¹' s).indicator 1 x : ℝ≥0∞)
Tactic: rw [lintegral_dirac']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
b : β
x : γ
rw :
  Eq (α := ℝ≥0∞)
    ((((swap γ β : (a : γ × β) → Measure (β × γ)) (x, b) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Prod.mk b ⁻¹' s).indicator 1 x : ℝ≥0∞)
⊢ ∫⁻ (y : β),
      (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s ∂Measure.dirac b =
    (Prod.mk b ⁻¹' s).indicator 1 x
have hf : Measurable (β := ℝ≥0∞) fun (y : β) ↦
  (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s
Tactic: rw [lintegral_dirac']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
b : β
⊢ ∫⁻ (x : γ),
      ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
have h_int : ∀ (x : γ),
  ∫⁻ (y : β),
      (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s ∂Measure.dirac b =
    (Prod.mk b ⁻¹' s).indicator 1 x
Tactic: have h_int x : ∫⁻ y, swap γ β (x, y) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x := by
    rw [lintegral_dirac']
    · simp [swap_apply' _ hs, Set.indicator_apply]
    · simpa [swap_apply' _ hs, Prod.swap_prod_mk] using
        measurable_const.indicator (measurable_prodMk_right hs)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
b : β
h_int :
  ∀ (x : γ),
    ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac b =
      (Prod.mk b ⁻¹' s).indicator 1 x
⊢ ∫⁻ (x : γ),
      ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
have e_f : ∫⁻ (x : γ), (Prod.mk b ⁻¹' s).indicator 1 x ∂(η : (a : α × β) → Measure γ) (a, b) =
  (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: simp_rw [h_int]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
b : β
h_int :
  ∀ (x : γ),
    ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac b =
      (Prod.mk b ⁻¹' s).indicator 1 x
⊢ ∫⁻ (x : γ), (Prod.mk b ⁻¹' s).indicator 1 x ∂(η : (a : α × β) → Measure γ) (a, b) =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
have e_f : MeasurableSet (Prod.mk b ⁻¹' s)
Tactic: rw [lintegral_indicator_one]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
b : β
⊢ ∫⁻ (x : γ),
      ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
have have : ∀ (x : γ),
  ∫⁻ (y : β),
      (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s ∂Measure.dirac b =
    (Prod.mk b ⁻¹' s).indicator 1 x
Tactic: classical
  have h_int x : ∫⁻ y, swap γ β (x, y) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x := by
    rw [lintegral_dirac']
    · simp [swap_apply' _ hs, Set.indicator_apply]
    · simpa [swap_apply' _ hs, Prod.swap_prod_mk] using
        measurable_const.indicator (measurable_prodMk_right hs)
  simp_rw [h_int]
  rw [lintegral_indicator_one]
  exact measurable_prodMk_left hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
b : β
have :
  ∀ (x : γ),
    ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac b =
      (Prod.mk b ⁻¹' s).indicator 1 x
⊢ ∫⁻ (x : γ),
      ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
have e_f : ∀
  (h_int :
    ∀ (x : γ),
      ∫⁻ (y : β),
          (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
            s ∂Measure.dirac b =
        (Prod.mk b ⁻¹' s).indicator 1 x),
  ∫⁻ (x : γ),
      ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: classical
  have h_int x : ∫⁻ y, swap γ β (x, y) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x := by
    rw [lintegral_dirac']
    · simp [swap_apply' _ hs, Set.indicator_apply]
    · simpa [swap_apply' _ hs, Prod.swap_prod_mk] using
        measurable_const.indicator (measurable_prodMk_right hs)
  simp_rw [h_int]
  rw [lintegral_indicator_one]
  exact measurable_prodMk_left hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
b : β
have :
  ∀ (x : γ),
    ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac b =
      (Prod.mk b ⁻¹' s).indicator 1 x
e_f :
  ∀
    (h_int :
      ∀ (x : γ),
        ∫⁻ (y : β),
            (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
              s ∂Measure.dirac b =
          (Prod.mk b ⁻¹' s).indicator 1 x),
    ∫⁻ (x : γ),
        ∫⁻ (y : β),
          (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
            s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
have₁ :
  ∀ (x : γ),
    ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac b =
      (Prod.mk b ⁻¹' s).indicator 1 x
e_f₁ e_f₂ :
  ∀
    (h_int :
      ∀ (x : γ),
        ∫⁻ (y : β),
            (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
              s ∂Measure.dirac b =
          (Prod.mk b ⁻¹' s).indicator 1 x),
    ∫⁻ (x : γ),
        ∫⁻ (y : β),
          (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
            s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
⊢ ∫⁻ (x : γ),
      ∫⁻ (y : β),
        (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
          s ∂Measure.dirac ((a, b), b).2 ∂(η : (a : α × β) → Measure γ) ((a, b), b).1 =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
have e_f₃ : ∀
  (h_int :
    ∀ (x : γ),
      ∫⁻ (y : β),
          (((swap γ β : (a : γ × β) → Measure (β × γ)) (x, y) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
            s ∂Measure.dirac b =
        (Prod.mk b ⁻¹' s).indicator 1 x),
  ∫⁻ (x : γ), (Prod.mk b ⁻¹' s).indicator 1 x ∂(η : (a : α × β) → Measure γ) (a, b) =
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: classical
  have h_int x : ∫⁻ y, swap γ β (x, y) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x := by
    rw [lintegral_dirac']
    · simp [swap_apply' _ hs, Set.indicator_apply]
    · simpa [swap_apply' _ hs, Prod.swap_prod_mk] using
        measurable_const.indicator (measurable_prodMk_right hs)
  simp_rw [h_int]
  rw [lintegral_indicator_one]
  exact measurable_prodMk_left hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
a : α
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have rw : ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' Set.univ) ∂(κ : (a : α) → Measure β) a =
  (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ
Tactic: rw [compProd_apply MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (s ×ˢ t) =
    ∫⁻ (b : β) in s,
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t ∂(κ : (a : α) → Measure β) a
have rw : ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s ×ˢ t) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (a_1 : β),
    s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t)
      a_1 ∂(κ : (a : α) → Measure β) a
Tactic: rw [compProd_apply (hs.prod ht), ← lintegral_indicator hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s ×ˢ t) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (a_1 : β),
      s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t)
        a_1 ∂(κ : (a : α) → Measure β) a
have e_f : ∀ (a_1 : β),
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' s ×ˢ t) : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) a_1 : ℝ≥0∞)
Tactic: congr with a