awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ Measurable (β := Measure (β × δ)) fun (x : α × γ) ↦
    Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2)
have refine : ∀ (s : Set (β × δ)) (hs : MeasurableSet s),
  Measurable (β := ℝ≥0∞) fun (b : α × γ) ↦
    (Measure.prod ((κ : (a : α) → Measure β) b.1) ((η : (a : γ) → Measure δ) b.2) : (a : Set (β × δ)) → ℝ≥0∞) s
Tactic: refine Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α × γ) ↦
    (Measure.prod ((κ : (a : α) → Measure β) b.1) ((η : (a : γ) → Measure δ) b.2) : (a : Set (β × δ)) → ℝ≥0∞) s
have simp_rw : Measurable (β := ℝ≥0∞) fun (b : α × γ) ↦
  ∫⁻ (x : β),
    (((η : (a : γ) → Measure δ) b.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂(κ : (a : α) → Measure β) b.1
Tactic: simp_rw [Measure.prod_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α × γ) ↦
    ∫⁻ (x : β),
      (((η : (a : γ) → Measure δ) b.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ : (a : α) → Measure β) b.1
have refine : Measurable (β := ℝ≥0∞) fun (y : (α × γ) × β) ↦
  (((prodMkLeft α η : (a : α × γ) → Measure δ) y.1 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk y.2 ⁻¹' s)
Tactic: refine Measurable.lintegral_kernel_prod_right'
        (f := fun y ↦ prodMkLeft α η y.1 (Prod.mk y.2 ⁻¹' s)) (κ := prodMkRight γ κ) ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (y : (α × γ) × β) ↦
    (((prodMkLeft α η : (a : α × γ) → Measure δ) y.1 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk y.2 ⁻¹' s)
have this : Eq (α := (y : (α × γ) × β) → ℝ≥0∞)
  (fun (y : (α × γ) × β) ↦
    (((prodMkLeft α η : (a : α × γ) → Measure δ) y.1 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk y.2 ⁻¹' s))
  fun (y : (α × γ) × β) ↦
  (((prodMkRight β (prodMkLeft α η) : (a : (α × γ) × β) → Measure δ) y : Measure δ) : (a : Set δ) → ℝ≥0∞)
    (Prod.mk y.2 ⁻¹' s)
Tactic: have : (fun y ↦ prodMkLeft α η y.1 (Prod.mk y.2 ⁻¹' s))
          = fun y ↦ prodMkRight β (prodMkLeft α η) y (Prod.mk y.2 ⁻¹' s) := rfl
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ_1 : Kernel α β
η_1 : Kernel γ δ
x : α × γ
κ : Kernel α β
η : Kernel γ δ
h : IsSFiniteKernel κ ∧ IsSFiniteKernel η
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
this :
  Eq (α := (y : (α × γ) × β) → ℝ≥0∞)
    (fun (y : (α × γ) × β) ↦
      (((prodMkLeft α η : (a : α × γ) → Measure δ) y.1 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk y.2 ⁻¹' s))
    fun (y : (α × γ) × β) ↦
    (((prodMkRight β (prodMkLeft α η) : (a : (α × γ) × β) → Measure δ) y : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk y.2 ⁻¹' s)
⊢ Measurable (β := ℝ≥0∞) fun (y : (α × γ) × β) ↦
    (((prodMkLeft α η : (a : α × γ) → Measure δ) y.1 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk y.2 ⁻¹' s)
have rw : Measurable (β := ℝ≥0∞) fun (y : (α × γ) × β) ↦
  (((prodMkRight β (prodMkLeft α η) : (a : (α × γ) × β) → Measure δ) y : Measure δ) : (a : Set δ) → ℝ≥0∞)
    (Prod.mk y.2 ⁻¹' s)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
h : ¬IsSFiniteKernel κ
⊢ κ ∥ₖ η = 0
have rw : Eq (α := Kernel (α × γ) (β × δ))
  (if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then
    { toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
      measurable' := sorry }
  else 0)
  0
Tactic: rw [parallelComp, dif_neg (not_and_of_not_left _ h)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
h : ¬IsSFiniteKernel κ
rw :
  Eq (α := Kernel (α × γ) (β × δ))
    (if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then
      { toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
        measurable' := ⋯ }
    else 0)
    0
⊢ κ ∥ₖ η = 0
have rw₁ : Eq (α := Kernel (α × γ) (β × δ)) 0 0
Tactic: rw [parallelComp, dif_neg (not_and_of_not_left _ h)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
κ : Kernel α β
h : ¬IsSFiniteKernel η
⊢ κ ∥ₖ η = 0
have rw : Eq (α := Kernel (α × γ) (β × δ))
  (if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then
    { toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
      measurable' := sorry }
  else 0)
  0
Tactic: rw [parallelComp, dif_neg (not_and_of_not_right _ h)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
κ : Kernel α β
h : ¬IsSFiniteKernel η
rw :
  Eq (α := Kernel (α × γ) (β × δ))
    (if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then
      { toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
        measurable' := ⋯ }
    else 0)
    0
⊢ κ ∥ₖ η = 0
have rw₁ : Eq (α := Kernel (α × γ) (β × δ)) 0 0
Tactic: rw [parallelComp, dif_neg (not_and_of_not_right _ h)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel γ δ
inst_1 : IsSFiniteKernel η
x : α × γ
⊢ Eq (α := Measure (β × δ)) ((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ))
    (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : Measure (β × δ))
have rw : Eq (α := Measure (β × δ))
  ((if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then
          { toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
            measurable' := sorry }
        else 0 :
        (a : α × γ) → Measure (β × δ))
      x :
    Measure (β × δ))
  (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : Measure (β × δ))
Tactic: rw [parallelComp, dif_pos ⟨inferInstance, inferInstance⟩, coe_mk]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel γ δ
inst_1 : IsSFiniteKernel η
x : α × γ
rw :
  Eq (α := Measure (β × δ))
    ((if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then
            { toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
              measurable' := ⋯ }
          else 0 :
          (a : α × γ) → Measure (β × δ))
        x :
      Measure (β × δ))
    (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : Measure (β × δ))
⊢ Eq (α := Measure (β × δ)) ((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ))
    (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : Measure (β × δ))
have rw₁ : Eq (α := Measure (β × δ))
  (({ toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
          measurable' := sorry : Kernel (α × γ) (β × δ) } :
        (a : α × γ) → Measure (β × δ))
      x :
    Measure (β × δ))
  (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : Measure (β × δ))
Tactic: rw [parallelComp, dif_pos ⟨inferInstance, inferInstance⟩, coe_mk]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel γ δ
inst_1 : IsSFiniteKernel η
x : α × γ
rw :
  Eq (α := Measure (β × δ))
    ((if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then
            { toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
              measurable' := ⋯ }
          else 0 :
          (a : α × γ) → Measure (β × δ))
        x :
      Measure (β × δ))
    (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : Measure (β × δ))
rw₁ :
  Eq (α := Measure (β × δ))
    (({ toFun := fun (x : α × γ) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2),
            measurable' := ⋯ : Kernel (α × γ) (β × δ) } :
          (a : α × γ) → Measure (β × δ))
        x :
      Measure (β × δ))
    (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : Measure (β × δ))
⊢ Eq (α := Measure (β × δ)) ((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ))
    (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : Measure (β × δ))
have rw₂ : Eq (α := Measure (β × δ)) (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2))
  (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2))
Tactic: rw [parallelComp, dif_pos ⟨inferInstance, inferInstance⟩, coe_mk]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
⊢ (((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) x.1
have rw : (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : (a : Set (β × δ)) → ℝ≥0∞) s =
  ∫⁻ (b : β),
    (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) x.1
Tactic: rw [parallelComp_apply, Measure.prod_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
s : Set (β × δ)
hs : MeasurableSet s
rw :
  (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : (a : Set (β × δ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) x.1
⊢ (((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) x.1
have rw₁ : ∫⁻ (x_1 : β),
    (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk x_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) x.1 =
  ∫⁻ (b : β),
    (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) x.1
Tactic: rw [parallelComp_apply, Measure.prod_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set δ
⊢ (((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞)
have rw : (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : (a : Set (β × δ)) → ℝ≥0∞) (s ×ˢ t) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [parallelComp_apply, Measure.prod_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set δ
rw :
  (Measure.prod ((κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : (a : Set (β × δ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [parallelComp_apply, Measure.prod_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
⊢ (((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) Set.univ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have rw : ∫⁻ (x_1 : β),
    (((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk x_1 ⁻¹' Set.univ) ∂(κ : (a : α) → Measure β) x.1 =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : γ) → Measure δ) x.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x.1 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: rw [parallelComp_apply, Measure.prod_apply .univ, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
⊢ Eq (α := Kernel (α × γ) (β × δ)) (0 ∥ₖ η) 0
have pos : ∀ (h : IsSFiniteKernel η), Eq (α := Kernel (α × γ) (β × δ)) (0 ∥ₖ η) 0
Tactic: by_cases h : IsSFiniteKernel η
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
pos : ∀ (h : IsSFiniteKernel η), Eq (α := Kernel (α × γ) (β × δ)) (0 ∥ₖ η) 0
⊢ Eq (α := Kernel (α × γ) (β × δ)) (0 ∥ₖ η) 0
have neg : ∀ (h : ¬IsSFiniteKernel η), Eq (α := Kernel (α × γ) (β × δ)) (0 ∥ₖ η) 0
Tactic: by_cases h : IsSFiniteKernel η
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
η : Kernel γ δ
h : IsSFiniteKernel η
⊢ Eq (α := Kernel (α × γ) (β × δ)) (0 ∥ₖ η) 0
have pos : ∀ (a : α × γ) (s : Set (β × δ)),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((0 ∥ₖ η : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((((0 : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
⊢ Eq (α := Kernel (α × γ) (β × δ)) (κ ∥ₖ 0) 0
have pos : ∀ (h : IsSFiniteKernel κ), Eq (α := Kernel (α × γ) (β × δ)) (κ ∥ₖ 0) 0
Tactic: by_cases h : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
pos : ∀ (h : IsSFiniteKernel κ), Eq (α := Kernel (α × γ) (β × δ)) (κ ∥ₖ 0) 0
⊢ Eq (α := Kernel (α × γ) (β × δ)) (κ ∥ₖ 0) 0
have neg : ∀ (h : ¬IsSFiniteKernel κ), Eq (α := Kernel (α × γ) (β × δ)) (κ ∥ₖ 0) 0
Tactic: by_cases h : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
h : IsSFiniteKernel κ
⊢ Eq (α := Kernel (α × γ) (β × δ)) (κ ∥ₖ 0) 0
have pos : ∀ (a : α × γ) (s : Set (β × δ)),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((κ ∥ₖ 0 : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((((0 : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ Eq (α := Kernel (α × β) (α × β)) (Kernel.id ∥ₖ Kernel.id) Kernel.id
have h : ∀ (a : α × β),
  Eq (α := Measure (α × β)) ((Kernel.id ∥ₖ Kernel.id : (a : α × β) → Measure (α × β)) a : Measure (α × β))
    ((Kernel.id : (a : α × β) → Measure (α × β)) a : Measure (α × β))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
⊢ deterministic f hf ∥ₖ deterministic g hg = deterministic (Prod.map f g) ⋯
have h : ∀ (x : α × β),
  Eq (α := Measure (γ × δ))
    ((deterministic f hf ∥ₖ deterministic g hg : (a : α × β) → Measure (γ × δ)) x : Measure (γ × δ))
    ((deterministic (Prod.map f g) sorry : (a : α × β) → Measure (γ × δ)) x : Measure (γ × δ))
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α × β
⊢ Eq (α := Measure (γ × δ))
    ((deterministic f hf ∥ₖ deterministic g hg : (a : α × β) → Measure (γ × δ)) x : Measure (γ × δ))
    ((deterministic (Prod.map f g) ⋯ : (a : α × β) → Measure (γ × δ)) x : Measure (γ × δ))
have h : Eq (α := Measure (γ × δ))
  (Measure.prod ((deterministic f hf : (a : α) → Measure γ) x.1) ((deterministic g hg : (a : β) → Measure δ) x.2))
  ((deterministic (Prod.map f g) sorry : (a : α × β) → Measure (γ × δ)) x)
Tactic: simp_rw [parallelComp_apply, deterministic_apply, Prod.map, Measure.dirac_prod_dirac]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α × β
h :
  Eq (α := Measure (γ × δ))
    (Measure.prod ((deterministic f hf : (a : α) → Measure γ) x.1) ((deterministic g hg : (a : β) → Measure δ) x.2))
    ((deterministic (Prod.map f g) ⋯ : (a : α × β) → Measure (γ × δ)) x)
⊢ Eq (α := Measure (γ × δ))
    ((deterministic f hf ∥ₖ deterministic g hg : (a : α × β) → Measure (γ × δ)) x : Measure (γ × δ))
    ((deterministic (Prod.map f g) ⋯ : (a : α × β) → Measure (γ × δ)) x : Measure (γ × δ))
have h₁ : Eq (α := Measure (γ × δ)) (Measure.prod (Measure.dirac (f x.1)) (Measure.dirac (g x.2)))
  (Measure.dirac (Prod.map f g x))
Tactic: simp_rw [parallelComp_apply, deterministic_apply, Prod.map, Measure.dirac_prod_dirac]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.ParallelComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → γ
g : β → δ
hf : Measurable f
hg : Measurable g
x : α × β
h :
  Eq (α := Measure (γ × δ))
    (Measure.prod ((deterministic f hf : (a : α) → Measure γ) x.1) ((deterministic g hg : (a : β) → Measure δ) x.2))
    ((deterministic (Prod.map f g) ⋯ : (a : α × β) → Measure (γ × δ)) x)
h₁ :
  Eq (α := Measure (γ × δ)) (Measure.prod (Measure.dirac (f x.1)) (Measure.dirac (g x.2)))
    (Measure.dirac (Prod.map f g x))
⊢ Eq (α := Measure (γ × δ))
    ((deterministic f hf ∥ₖ deterministic g hg : (a : α × β) → Measure (γ × δ)) x : Measure (γ × δ))
    ((deterministic (Prod.map f g) ⋯ : (a : α × β) → Measure (γ × δ)) x : Measure (γ × δ))
have h₂ : Eq (α := Measure (γ × δ)) (Measure.prod (Measure.dirac (f x.1)) (Measure.dirac (g x.2))) (Measure.dirac (f x.1, g x.2))
Tactic: simp_rw [parallelComp_apply, deterministic_apply, Prod.map, Measure.dirac_prod_dirac]