awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 ∥ₖ η

Tactic:
simp [h]
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 η
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∞)
⊢ Kernel.sum κ ∥ₖ η = Kernel.sum fun (i : ι) ↦ κ i ∥ₖ η

Tactic:
ext x
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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∞)
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∞)
⊢ 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:
simp_rw [Kernel.sum_apply, parallelComp_apply, Kernel.sum_apply, Measure.prod_sum_left]

Premises used: ProbabilityTheory.Kernel.sum_apply, MeasureTheory.Measure.prod_sum_left, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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
neg : ∀ (h : ¬IsSFiniteKernel κ), κ ∥ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i

Tactic:
by_cases h : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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

Tactic:
simp [h]
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 κ
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∞)
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ∥ₖ η i

Tactic:
ext x
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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∞)
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∞)
⊢ 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:
simp_rw [Kernel.sum_apply, parallelComp_apply, Kernel.sum_apply, Measure.prod_sum_right]

Premises used: ProbabilityTheory.Kernel.sum_apply, MeasureTheory.Measure.prod_sum_right, ProbabilityTheory.Kernel.parallelComp_apply
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x_1 : α × γ
inst : IsMarkovKernel κ
inst_1 : IsMarkovKernel η
x : α × γ
⊢ Eq (α := ℝ≥0∞)
    ((((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) x : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
simp [parallelComp_apply_univ]

Premises used: ProbabilityTheory.Kernel.parallelComp_apply_univ
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 ∥ₖ η)
inr : IsMarkovKernel κ → IsZeroOrMarkovKernel (κ ∥ₖ η)
⊢ IsZeroOrMarkovKernel (κ ∥ₖ η)

Tactic:
obtain rfl | _ := eq_zero_or_isMarkovKernel κ

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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)
inl₁ :
  IsMarkovKernel η →
    IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
      (0 ∥ₖ η)
⊢ IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (0 ∥ₖ η)

Tactic:
obtain rfl | _ := eq_zero_or_isMarkovKernel η

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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)
inr₁ : IsMarkovKernel η → IsZeroOrMarkovKernel (κ ∥ₖ η)
⊢ IsZeroOrMarkovKernel (κ ∥ₖ η)

Tactic:
obtain rfl | _ := eq_zero_or_isMarkovKernel η

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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
simpa :
  IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace) 0
⊢ IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (0 ∥ₖ 0)

Tactic:
simpa using by infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 η
simpa :
  IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace) 0
⊢ IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (0 ∥ₖ η)

Tactic:
simpa using by infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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
simpa :
  IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace) 0
⊢ IsZeroOrMarkovKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (κ ∥ₖ 0)

Tactic:
simpa using by infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 κ
h_1 : IsMarkovKernel η
⊢ IsZeroOrMarkovKernel (κ ∥ₖ η)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 (κ ∥ₖ η)

Tactic:
⟨⟨κ.bound * η.bound, ENNReal.mul_lt_top κ.bound_lt_top η.bound_lt_top, fun a ↦ ?_⟩⟩

Premises used: HMul.hMul, ProbabilityTheory.IsFiniteKernel.mk, ENNReal.mul_lt_top, ProbabilityTheory.Kernel.bound_lt_top, And.intro, Exists.intro, ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 η
refine :
  ∀ (a : α × γ),
    (((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) Set.univ ≤
      κ.bound * η.bound
⊢ IsFiniteKernel (κ ∥ₖ η)

Tactic:
refine ⟨⟨κ.bound * η.bound, ENNReal.mul_lt_top κ.bound_lt_top η.bound_lt_top, fun a ↦ ?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 =
    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∞)

Tactic:
parallelComp_apply_univ

Premises used: ProbabilityTheory.Kernel.parallelComp_apply_univ
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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
h₂ : (((η : (a : γ) → Measure δ) a.2 : 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

Tactic:
gcongr
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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.1 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound

Tactic:
measure_le_bound κ a.1 Set.univ

Premises used: Set.univ, Prod.fst, ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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.1 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound

Tactic:
exact measure_le_bound κ a.1 Set.univ

Premises used: Set.univ, Prod.fst, ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) Set.univ ≤ η.bound

Tactic:
measure_le_bound η a.2 Set.univ

Premises used: Set.univ, ProbabilityTheory.Kernel.measure_le_bound, Prod.snd
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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.2 : Measure δ) : (a : Set δ) → ℝ≥0∞) Set.univ ≤ η.bound

Tactic:
exact measure_le_bound η a.2 Set.univ

Premises used: Set.univ, ProbabilityTheory.Kernel.measure_le_bound, Prod.snd
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 : α × γ
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
⊢ (((κ ∥ₖ η : (a : α × γ) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) Set.univ ≤
    κ.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

Premises used: Set.univ, Prod.fst, ProbabilityTheory.Kernel.parallelComp, Prod.snd, DFunLike.coe, ProbabilityTheory.Kernel.parallelComp_apply_univ, ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 (κ ∥ₖ η)
neg : ∀ (h : ¬IsSFiniteKernel κ), IsSFiniteKernel (κ ∥ₖ η)
⊢ IsSFiniteKernel (κ ∥ₖ η)

Tactic:
by_cases h : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 κ
neg : IsSFiniteKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace) 0
⊢ IsSFiniteKernel (κ ∥ₖ η)

Tactic:
simp only [h, not_false_eq_true, parallelComp_of_not_isSFiniteKernel_left]

Premises used: ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_left, not_false_eq_true
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 (κ ∥ₖ η)
neg : ∀ (h : ¬IsSFiniteKernel η), IsSFiniteKernel (κ ∥ₖ η)
⊢ IsSFiniteKernel (κ ∥ₖ η)

Tactic:
by_cases h : IsSFiniteKernel η

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 η
neg : IsSFiniteKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace) 0
⊢ IsSFiniteKernel (κ ∥ₖ η)

Tactic:
simp only [h, not_false_eq_true, parallelComp_of_not_isSFiniteKernel_right]

Premises used: ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_right, not_false_eq_true
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 η
pos :
  IsSFiniteKernel (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (Kernel.sum fun (i : ℕ) ↦ Kernel.sum fun (i_1 : ℕ) ↦ κ.seq i ∥ₖ η.seq i_1)
⊢ IsSFiniteKernel (κ ∥ₖ η)

Tactic:
simp_rw [← kernel_sum_seq κ, ← kernel_sum_seq η, parallelComp_sum_left, parallelComp_sum_right]

Premises used: ProbabilityTheory.Kernel.parallelComp_sum_left, ProbabilityTheory.Kernel.parallelComp_sum_right, ProbabilityTheory.Kernel.kernel_sum_seq
-- Module: Mathlib.Probability.Kernel.Composition.ParallelComp
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 (α := α × γ) (β := β × δ) (mα := Prod.instMeasurableSpace) (mβ := Prod.instMeasurableSpace)
    (Kernel.sum fun (i : ℕ) ↦ Kernel.sum fun (i_1 : ℕ) ↦ κ.seq i ∥ₖ η.seq i_1)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Prod
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel α γ
⊢ κ ∥ₖ η ∘ₖ copy α = κ ×ₖ η

Tactic:
rfl

Premises used: rfl, ProbabilityTheory.Kernel.prod