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 δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α × γ
h₁ : (((κ : (a : α) → Measure β) a.1 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a.1 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      ((((η : (a : γ) → Measure δ) a.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    κ.bound * η.bound
have h₂ : (((η : (a : γ) → Measure δ) a.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) Set.univ ≤ η.bound
Tactic: gcongr
-- 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 : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α × γ
⊢ (((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) Set.univ ≤
    κ.bound * η.bound
have calc : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a.1 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((η : (a : γ) → Measure δ) a.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
  κ.bound * η.bound
Tactic: calc (κ ∥ₖ η) a Set.univ
  _ = κ a.1 Set.univ * η a.2 Set.univ := parallelComp_apply_univ
  _ ≤ κ.bound * η.bound := by
    gcongr
    · exact measure_le_bound κ a.1 Set.univ
    · exact measure_le_bound η a.2 Set.univ
-- 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 : α × γ
⊢ IsSFiniteKernel (κ ∥ₖ η)
have pos : ∀ (h : IsSFiniteKernel κ), IsSFiniteKernel (κ ∥ₖ η)
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 α β
η : Kernel γ δ
x : α × γ
pos : ∀ (h : IsSFiniteKernel κ), IsSFiniteKernel (κ ∥ₖ η)
⊢ IsSFiniteKernel (κ ∥ₖ η)
have neg : ∀ (h : ¬IsSFiniteKernel κ), IsSFiniteKernel (κ ∥ₖ η)
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 α β
η : Kernel γ δ
x : α × γ
h : ¬IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ ∥ₖ η)
have neg : IsSFiniteKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace) 0
Tactic: simp only [h, not_false_eq_true, parallelComp_of_not_isSFiniteKernel_left]
-- 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 : α × γ
h : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ ∥ₖ η)
have pos : ∀ (h : IsSFiniteKernel η), IsSFiniteKernel (κ ∥ₖ η)
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 α β
η : Kernel γ δ
x : α × γ
h : IsSFiniteKernel κ
pos : ∀ (h : IsSFiniteKernel η), IsSFiniteKernel (κ ∥ₖ η)
⊢ IsSFiniteKernel (κ ∥ₖ η)
have neg : ∀ (h : ¬IsSFiniteKernel η), IsSFiniteKernel (κ ∥ₖ η)
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 α β
η : Kernel γ δ
x : α × γ
h_1 : IsSFiniteKernel κ
h : ¬IsSFiniteKernel η
⊢ IsSFiniteKernel (κ ∥ₖ η)
have neg : IsSFiniteKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace) 0
Tactic: simp only [h, not_false_eq_true, parallelComp_of_not_isSFiniteKernel_right]
-- 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 : α × γ
h_1 : IsSFiniteKernel κ
h : IsSFiniteKernel η
⊢ IsSFiniteKernel (κ ∥ₖ η)
have pos : IsSFiniteKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
  (Kernel.sum fun (i : ℕ) ↦ Kernel.sum fun (i_1 : ℕ) ↦ κ.seq i ∥ₖ η.seq i_1)
Tactic: simp_rw [← kernel_sum_seq κ, ← kernel_sum_seq η, parallelComp_sum_left, parallelComp_sum_right]
-- 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 γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ (((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
have simp_rw : (((κ ∥ₖ η ∘ₖ copy α : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
  ∫⁻ (b : β),
    (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [prod, comp_apply, copy_apply, Measure.dirac_bind (Kernel.measurable _) (a, a),
    parallelComp_apply, Measure.prod_apply hs]
-- 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 γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
simp_rw :
  (((κ ∥ₖ η ∘ₖ copy α : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
⊢ (((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
have simp_rw₁ : (Measure.bind (α := α × α) (mα := Prod.instMeasurableSpace) ((copy α : (a : α) → Measure (α × α)) a)
        (⇑(κ ∥ₖ η) : (a : α × α) → Measure (β × γ)) :
      (a : Set (β × γ)) → ℝ≥0∞)
    s =
  ∫⁻ (b : β),
    (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [prod, comp_apply, copy_apply, Measure.dirac_bind (Kernel.measurable _) (a, a),
    parallelComp_apply, Measure.prod_apply hs]
-- 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 γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
simp_rw :
  (((κ ∥ₖ η ∘ₖ copy α : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
simp_rw₁ :
  (Measure.bind (α := α × α) (mα := Prod.instMeasurableSpace) ((copy α : (a : α) → Measure (α × α)) a)
          (⇑(κ ∥ₖ η) : (a : α × α) → Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
⊢ (((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
have simp_rw₂ : (Measure.bind (mα := Prod.instMeasurableSpace) (Measure.dirac (a, a)) (⇑(κ ∥ₖ η) : (a : α × α) → Measure (β × γ)) :
      (a : Set (β × γ)) → ℝ≥0∞)
    s =
  ∫⁻ (b : β),
    (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [prod, comp_apply, copy_apply, Measure.dirac_bind (Kernel.measurable _) (a, a),
    parallelComp_apply, Measure.prod_apply hs]
-- 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 γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
simp_rw :
  (((κ ∥ₖ η ∘ₖ copy α : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
simp_rw₁ :
  (Measure.bind (α := α × α) (mα := Prod.instMeasurableSpace) ((copy α : (a : α) → Measure (α × α)) a)
          (⇑(κ ∥ₖ η) : (a : α × α) → Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
simp_rw₂ :
  (Measure.bind (mα := Prod.instMeasurableSpace) (Measure.dirac (a, a)) (⇑(κ ∥ₖ η) : (a : α × α) → Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
⊢ (((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
have simp_rw₃ : (((κ ∥ₖ η : (a : α × α) → Measure (β × γ)) (a, a) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
  ∫⁻ (b : β),
    (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [prod, comp_apply, copy_apply, Measure.dirac_bind (Kernel.measurable _) (a, a),
    parallelComp_apply, Measure.prod_apply hs]
-- 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 γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
simp_rw :
  (((κ ∥ₖ η ∘ₖ copy α : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
simp_rw₁ :
  (Measure.bind (α := α × α) (mα := Prod.instMeasurableSpace) ((copy α : (a : α) → Measure (α × α)) a)
          (⇑(κ ∥ₖ η) : (a : α × α) → Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
simp_rw₂ :
  (Measure.bind (mα := Prod.instMeasurableSpace) (Measure.dirac (a, a)) (⇑(κ ∥ₖ η) : (a : α × α) → Measure (β × γ)) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
simp_rw₃ :
  (((κ ∥ₖ η : (a : α × α) → Measure (β × γ)) (a, a) : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
⊢ (((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
have simp_rw₄ : (Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) s =
  ∫⁻ (b : β),
    (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [prod, comp_apply, copy_apply, Measure.dirac_bind (Kernel.measurable _) (a, a),
    parallelComp_apply, Measure.prod_apply hs]
-- 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 γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
⊢ Eq (α := Measure (β × γ)) ((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ))
    (Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : Measure (β × γ))
have h : ∀ (s : Set (β × γ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- 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 γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (b : β),
    (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
  (Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) s
Tactic: rw [prod_apply' _ _ _ hs, Measure.prod_apply hs]
-- 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 γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    (Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∫⁻ (b : β),
    (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (x : β),
    (((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂(κ : (a : α) → Measure β) a
Tactic: rw [prod_apply' _ _ _ hs, Measure.prod_apply hs]
-- 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 γ
κ : Kernel α β
η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
a : α
⊢ (((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
have rw : (Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) (s ×ˢ t) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [prod_apply, Measure.prod_prod]
-- 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 γ
κ : Kernel α β
η : Kernel α γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
a : α
rw :
  (Measure.prod ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure γ) a) : (a : Set (β × γ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (((κ ×ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [prod_apply, Measure.prod_prod]
-- 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 γ
μ : Measure β
inst : SFinite μ
ν : Measure γ
inst_1 : SFinite ν
⊢ Eq (α := Kernel α (β × γ)) (const α μ ×ₖ const α ν) (const α (μ.prod ν))
have h : ∀ (x : α) (s : Set (β × γ)),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((const α μ ×ₖ const α ν : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((((const α (μ.prod ν) : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext x
-- 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 γ
μ : Measure β
inst : SFinite μ
ν : Measure γ
inst_1 : SFinite ν
x : α
s : Set (β × γ)
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((const α μ ×ₖ const α ν : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((const α (μ.prod ν) : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  ((((const α μ ×ₖ const α ν : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
  ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [const_apply, prod_apply, const_apply, const_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
mγ : MeasurableSpace γ
μ : Measure β
inst : SFinite μ
ν : Measure γ
inst_1 : SFinite ν
x : α
s : Set (β × γ)
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((((const α μ ×ₖ const α ν : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((const α μ ×ₖ const α ν : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((const α (μ.prod ν) : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞)
  ((Measure.prod (((const α μ : Kernel α β) : (a : α) → Measure β) x)
          (((const α ν : Kernel α γ) : (a : α) → Measure γ) x) :
        (a : Set (β × γ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [const_apply, prod_apply, const_apply, const_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
mγ : MeasurableSpace γ
μ : Measure β
inst : SFinite μ
ν : Measure γ
inst_1 : SFinite ν
x : α
s : Set (β × γ)
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((((const α μ ×ₖ const α ν : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.prod (((const α μ : Kernel α β) : (a : α) → Measure β) x)
            (((const α ν : Kernel α γ) : (a : α) → Measure γ) x) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((const α μ ×ₖ const α ν : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((const α (μ.prod ν) : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) ((μ.prod (((const α ν : Kernel α γ) : (a : α) → Measure γ) x) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
  ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [const_apply, prod_apply, const_apply, const_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
mγ : MeasurableSpace γ
μ : Measure β
inst : SFinite μ
ν : Measure γ
inst_1 : SFinite ν
x : α
s : Set (β × γ)
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((((const α μ ×ₖ const α ν : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.prod (((const α μ : Kernel α β) : (a : α) → Measure β) x)
            (((const α ν : Kernel α γ) : (a : α) → Measure γ) x) :
          (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((μ.prod (((const α ν : Kernel α γ) : (a : α) → Measure γ) x) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((const α μ ×ₖ const α ν : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((const α (μ.prod ν) : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞) ((μ.prod ν : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [const_apply, prod_apply, const_apply, const_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
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel α γ
inst_1 : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ ×ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(η : (a : α) → Measure γ) a ∂(κ : (a : α) → Measure β) a
have simp_rw : ∫⁻ (b : α × α), ∫⁻ (c : β × γ), g c ∂(κ ∥ₖ η : (a : α × α) → Measure (β × γ)) b ∂Measure.dirac (a, a) =
  ∫⁻ (b : β), ∫⁻ (c : γ), g (b, c) ∂(η : (a : α) → Measure γ) a ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [prod, lintegral_comp _ _ _ hg, copy_apply]