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 γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
ac : α × γ
g : β × δ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (bd : β × δ), g bd ∂(κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) ac =
    ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂(η : (a : γ) → Measure δ) ac.2 ∂(κ : (a : α) → Measure β) ac.1
have rw : ∫⁻ (bd : β × δ), g bd ∂Measure.prod ((κ : (a : α) → Measure β) ac.1) ((η : (a : γ) → Measure δ) ac.2) =
  ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂(η : (a : γ) → Measure δ) ac.2 ∂(κ : (a : α) → Measure β) ac.1
Tactic: rw [parallelComp_apply, MeasureTheory.lintegral_prod _ hg.aemeasurable]
-- 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 γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
ac : α × γ
g : β × δ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (bd : β × δ), g bd ∂Measure.prod ((κ : (a : α) → Measure β) ac.1) ((η : (a : γ) → Measure δ) ac.2) =
    ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂(η : (a : γ) → Measure δ) ac.2 ∂(κ : (a : α) → Measure β) ac.1
⊢ ∫⁻ (bd : β × δ), g bd ∂(κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) ac =
    ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂(η : (a : γ) → Measure δ) ac.2 ∂(κ : (a : α) → Measure β) ac.1
have rw₁ : ∫⁻ (x : β), ∫⁻ (y : δ), g (x, y) ∂(η : (a : γ) → Measure δ) ac.2 ∂(κ : (a : α) → Measure β) ac.1 =
  ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂(η : (a : γ) → Measure δ) ac.2 ∂(κ : (a : α) → Measure β) ac.1
Tactic: rw [parallelComp_apply, MeasureTheory.lintegral_prod _ hg.aemeasurable]
-- 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 γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
ac : α × γ
g : β × δ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (bd : β × δ), g bd ∂(κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) ac =
    ∫⁻ (d : δ), ∫⁻ (b : β), g (b, d) ∂(κ : (a : α) → Measure β) ac.1 ∂(η : (a : γ) → Measure δ) ac.2
have rw : ∫⁻ (bd : β × δ), g bd ∂Measure.prod ((κ : (a : α) → Measure β) ac.1) ((η : (a : γ) → Measure δ) ac.2) =
  ∫⁻ (d : δ), ∫⁻ (b : β), g (b, d) ∂(κ : (a : α) → Measure β) ac.1 ∂(η : (a : γ) → Measure δ) ac.2
Tactic: rw [parallelComp_apply, MeasureTheory.lintegral_prod_symm _ hg.aemeasurable]
-- 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 γ δ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
ac : α × γ
g : β × δ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (bd : β × δ), g bd ∂Measure.prod ((κ : (a : α) → Measure β) ac.1) ((η : (a : γ) → Measure δ) ac.2) =
    ∫⁻ (d : δ), ∫⁻ (b : β), g (b, d) ∂(κ : (a : α) → Measure β) ac.1 ∂(η : (a : γ) → Measure δ) ac.2
⊢ ∫⁻ (bd : β × δ), g bd ∂(κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) ac =
    ∫⁻ (d : δ), ∫⁻ (b : β), g (b, d) ∂(κ : (a : α) → Measure β) ac.1 ∂(η : (a : γ) → Measure δ) ac.2
have rw₁ : ∫⁻ (y : δ), ∫⁻ (x : β), g (x, y) ∂(κ : (a : α) → Measure β) ac.1 ∂(η : (a : γ) → Measure δ) ac.2 =
  ∫⁻ (d : δ), ∫⁻ (b : β), g (b, d) ∂(κ : (a : α) → Measure β) ac.1 ∂(η : (a : γ) → Measure δ) ac.2
Tactic: rw [parallelComp_apply, MeasureTheory.lintegral_prod_symm _ hg.aemeasurable]
-- 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 δ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η
have pos : ∀ (h : IsSFiniteKernel η), Kernel.sum κ ∥ₖ η = Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η
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 δ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
pos : ∀ (h : IsSFiniteKernel η), Kernel.sum κ ∥ₖ η = Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η
have neg : ∀ (h : ¬IsSFiniteKernel η), Kernel.sum κ ∥ₖ η = Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η
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 δ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : IsSFiniteKernel η
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η
have pos : ∀ (x : α × γ) (s : Set (β × δ)),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((Kernel.sum κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((((Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) :
            (a : Set (β × δ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
Tactic: ext x
-- 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 δ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : IsSFiniteKernel η
x : α × γ
s : Set (β × δ)
h_1 : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) :
          (a : Set (β × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞)
  ((((Kernel.sum κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
  ((Measure.sum fun (n : ι) ↦ (κ n ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [Kernel.sum_apply, parallelComp_apply, Kernel.sum_apply, Measure.prod_sum_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 δ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : IsSFiniteKernel η
x : α × γ
s : Set (β × δ)
h_1 : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ (κ n ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) :
          (a : Set (β × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have pos₁ : Eq (α := ℝ≥0∞)
  ((Measure.prod ((Kernel.sum κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) : (a : Set (β × δ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((Measure.sum fun (n : ι) ↦ Measure.prod ((κ n : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) :
        (a : Set (β × δ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: simp_rw [Kernel.sum_apply, parallelComp_apply, Kernel.sum_apply, Measure.prod_sum_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 δ
ι : Type u_5
inst : Countable ι
κ : ι → Kernel α β
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
η : Kernel γ δ
h : IsSFiniteKernel η
x : α × γ
s : Set (β × δ)
h_1 : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ (κ n ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
pos₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.prod ((Kernel.sum κ : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) :
          (a : Set (β × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ Measure.prod ((κ n : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) :
          (a : Set (β × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) :
          (a : Set (β × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have pos₂ : Eq (α := ℝ≥0∞)
  ((Measure.prod (Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) :
        (a : Set (β × δ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((Measure.sum fun (n : ι) ↦ Measure.prod ((κ n : (a : α) → Measure β) x.1) ((η : (a : γ) → Measure δ) x.2) :
        (a : Set (β × δ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: simp_rw [Kernel.sum_apply, parallelComp_apply, Kernel.sum_apply, Measure.prod_sum_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 δ
ι : Type u_5
inst : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i
have pos : ∀ (h : IsSFiniteKernel κ), κ ∥ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i
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 δ
ι : Type u_5
inst : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
pos : ∀ (h : IsSFiniteKernel κ), κ ∥ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i
have neg : ∀ (h : ¬IsSFiniteKernel κ), κ ∥ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i
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 δ
ι : Type u_5
inst : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
h : IsSFiniteKernel κ
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i
have pos : ∀ (x : α × γ) (s : Set (β × δ)),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((κ ∥ₖ Kernel.sum η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((((Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) :
            (a : Set (β × δ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
Tactic: ext x
-- 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 δ
ι : Type u_5
inst : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
h : IsSFiniteKernel κ
x : α × γ
s : Set (β × δ)
h_1 : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((κ ∥ₖ Kernel.sum η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) :
          (a : Set (β × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞)
  ((((κ ∥ₖ Kernel.sum η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
  ((Measure.sum fun (n : ι) ↦ (κ ∥ₖ η n : (a : α × γ) → Measure (β × δ)) x : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [Kernel.sum_apply, parallelComp_apply, Kernel.sum_apply, Measure.prod_sum_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 δ
ι : Type u_5
inst : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
h : IsSFiniteKernel κ
x : α × γ
s : Set (β × δ)
h_1 : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞)
    ((((κ ∥ₖ Kernel.sum η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ (κ ∥ₖ η n : (a : α × γ) → Measure (β × δ)) x : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((κ ∥ₖ Kernel.sum η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) :
          (a : Set (β × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have pos₁ : Eq (α := ℝ≥0∞)
  ((Measure.prod ((κ : (a : α) → Measure β) x.1) ((Kernel.sum η : (a : γ) → Measure δ) x.2) : (a : Set (β × δ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((Measure.sum fun (n : ι) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η n : (a : γ) → Measure δ) x.2) :
        (a : Set (β × δ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: simp_rw [Kernel.sum_apply, parallelComp_apply, Kernel.sum_apply, Measure.prod_sum_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 δ
ι : Type u_5
inst : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
h : IsSFiniteKernel κ
x : α × γ
s : Set (β × δ)
h_1 : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞)
    ((((κ ∥ₖ Kernel.sum η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ (κ ∥ₖ η n : (a : α × γ) → Measure (β × δ)) x : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
pos₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.prod ((κ : (a : α) → Measure β) x.1) ((Kernel.sum η : (a : γ) → Measure δ) x.2) :
          (a : Set (β × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η n : (a : γ) → Measure δ) x.2) :
          (a : Set (β × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((κ ∥ₖ Kernel.sum η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) :
          (a : Set (β × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have pos₂ : Eq (α := ℝ≥0∞)
  ((Measure.prod ((κ : (a : α) → Measure β) x.1) (Measure.sum fun (n : ι) ↦ (η n : (a : γ) → Measure δ) x.2) :
        (a : Set (β × δ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((Measure.sum fun (n : ι) ↦ Measure.prod ((κ : (a : α) → Measure β) x.1) ((η n : (a : γ) → Measure δ) x.2) :
        (a : Set (β × δ)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: simp_rw [Kernel.sum_apply, parallelComp_apply, Kernel.sum_apply, Measure.prod_sum_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 : α × γ
inst : IsZeroOrMarkovKernel κ
inst_1 : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel (κ ∥ₖ η)
have inl : ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
  IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (0 ∥ₖ η)
Tactic: obtain rfl | _ := eq_zero_or_isMarkovKernel κ
Cleared hypotheses: κ, inst
-- 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 : IsZeroOrMarkovKernel κ
inst_1 : IsZeroOrMarkovKernel η
inl :
  ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
      (0 ∥ₖ η)
⊢ IsZeroOrMarkovKernel (κ ∥ₖ η)
have inr : IsMarkovKernel κ → IsZeroOrMarkovKernel (κ ∥ₖ η)
Tactic: obtain rfl | _ := eq_zero_or_isMarkovKernel κ
-- 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 γ δ
x : α × γ
inst : IsZeroOrMarkovKernel η
inst_1 : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
⊢ IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (0 ∥ₖ η)
have inl : ∀ [IsZeroOrMarkovKernel.{u_3, u_4} (α := γ) (β := δ) (mα := mγ) (mβ := mδ) 0],
  IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (0 ∥ₖ 0)
Tactic: obtain rfl | _ := eq_zero_or_isMarkovKernel η
Cleared hypotheses: η, inst
-- 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 γ δ
x : α × γ
inst : IsZeroOrMarkovKernel η
inst_1 : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
inl :
  ∀ [IsZeroOrMarkovKernel.{u_3, u_4} (α := γ) (β := δ) (mα := mγ) (mβ := mδ) 0],
    IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
      (0 ∥ₖ 0)
⊢ IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (0 ∥ₖ η)
have inl₁ : IsMarkovKernel η →
  IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (0 ∥ₖ η)
Tactic: obtain rfl | _ := eq_zero_or_isMarkovKernel η
-- 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 : IsZeroOrMarkovKernel κ
inst_1 : IsZeroOrMarkovKernel η
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ ∥ₖ η)
have inr : ∀ [IsZeroOrMarkovKernel.{u_3, u_4} (α := γ) (β := δ) (mα := mγ) (mβ := mδ) 0],
  IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (κ ∥ₖ 0)
Tactic: obtain rfl | _ := eq_zero_or_isMarkovKernel η
Cleared hypotheses: η, inst_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 δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst : IsZeroOrMarkovKernel κ
inst_1 : IsZeroOrMarkovKernel η
h : IsMarkovKernel κ
inr :
  ∀ [IsZeroOrMarkovKernel.{u_3, u_4} (α := γ) (β := δ) (mα := mγ) (mβ := mδ) 0],
    IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
      (κ ∥ₖ 0)
⊢ IsZeroOrMarkovKernel (κ ∥ₖ η)
have inr₁ : IsMarkovKernel η → IsZeroOrMarkovKernel (κ ∥ₖ η)
Tactic: obtain rfl | _ := eq_zero_or_isMarkovKernel η
-- 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 δ
x : α × γ
inst : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
inst_1 : IsZeroOrMarkovKernel.{u_3, u_4} (α := γ) (β := δ) (mα := mγ) (mβ := mδ) 0
⊢ IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (0 ∥ₖ 0)
have simpa : IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace) 0
Tactic: simpa using by infer_instance
-- 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 γ δ
x : α × γ
inst : IsZeroOrMarkovKernel η
inst_1 : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
h : IsMarkovKernel η
⊢ IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (0 ∥ₖ η)
have simpa : IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace) 0
Tactic: simpa using by infer_instance
-- 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 α β
x : α × γ
inst : IsZeroOrMarkovKernel κ
h : IsMarkovKernel κ
inst_1 : IsZeroOrMarkovKernel.{u_3, u_4} (α := γ) (β := δ) (mα := mγ) (mβ := mδ) 0
⊢ IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (κ ∥ₖ 0)
have simpa : IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace) 0
Tactic: simpa using by infer_instance
-- 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 η
⊢ IsFiniteKernel (κ ∥ₖ η)
have refine : ∀ (a : α × γ),
  (((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) Set.univ ≤
    κ.bound * η.bound
Tactic: refine ⟨⟨κ.bound * η.bound, ENNReal.mul_lt_top κ.bound_lt_top η.bound_lt_top, fun a ↦ ?_⟩⟩
-- 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 : α × γ
⊢ 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.1 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound
Tactic: gcongr