awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Kernel α β
κ η : Kernel β γ
a : α
s : Set γ
hs : MeasurableSet s
h :
  ∫⁻ (b : β), (((κ + η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(μ : (a : α) → Measure β) a =
    (((κ ∘ₖ μ + η ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
h₁ :
  ∫⁻ (b : β),
      (HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : β) → Measure γ) b : Measure γ)
            ((η : (a : β) → Measure γ) b : Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s ∂(μ : (a : α) → Measure β) a =
    (HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ ∘ₖ μ : (a : α) → Measure γ) a : Measure γ)
          ((η ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) :
        (a : Set γ) → ℝ≥0∞)
      s
h₂ :
  ∫⁻ (b : β),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) ∂(μ : (a : α) → Measure β) a =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₃ :
  ∫⁻ (b : β),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        ((((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) ∂(μ : (a : α) → Measure β) a =
    ∫⁻ (b : β), (((κ : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(μ : (a : α) → Measure β) a +
      ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(μ : (a : α) → Measure β) a
⊢ Eq (α := ℝ≥0∞) (((((κ + η) ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ ∘ₖ μ + η ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [comp_apply' _ _ _ hs, add_apply, Measure.add_apply, comp_apply' _ _ _ hs,
    lintegral_add_left (Kernel.measurable_coe κ hs)]

Premises used: MeasureTheory.Measure.add_apply, MeasureTheory.lintegral_add_left, ProbabilityTheory.Kernel.add_apply, ProbabilityTheory.Kernel.measurable_coe, ProbabilityTheory.Kernel.comp_apply'
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
h :
  ∀ (a : α) (s : Set γ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((η ∘ₖ Kernel.sum κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((Kernel.sum fun (i : ι) ↦ η ∘ₖ κ i : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ η ∘ₖ Kernel.sum κ = Kernel.sum fun (i : ι) ↦ η ∘ₖ κ i

Tactic:
ext _ _ hs
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
a : α
s : Set γ
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((η ∘ₖ Kernel.sum κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.sum fun (n : ι) ↦ (η ∘ₖ κ n : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  ∫⁻ (b : β),
      (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(Kernel.sum κ : (a : α) → Measure β) a =
    ((Measure.sum fun (n : ι) ↦ (η ∘ₖ κ n : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
h₂ :
  ∫⁻ (b : β),
      (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(Kernel.sum κ : (a : α) → Measure β) a =
    ∑' (i : ι), (((η ∘ₖ κ i : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
h₃ :
  (∫⁻ (b : β),
      (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
        s ∂Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a) =
    ∑' (i : ι), (((η ∘ₖ κ i : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
h₄ :
  Eq (α := ℝ≥0∞)
    (∑' (i : ι),
      ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ i : (a : α) → Measure β) a)
    (∑' (i : ι), (((η ∘ₖ κ i : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞) ((((η ∘ₖ Kernel.sum κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ η ∘ₖ κ i : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [sum_apply, comp_apply' _ _ _ hs, Measure.sum_apply _ hs, sum_apply,
    lintegral_sum_measure, comp_apply' _ _ _ hs]

Premises used: MeasureTheory.Measure.sum_apply, ProbabilityTheory.Kernel.sum_apply, ProbabilityTheory.Kernel.comp_apply', MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  ∫⁻ (b : β),
      (((copy β : (a : β) → Measure (β × β)) b : Measure (β × β)) : (a : Set (β × β)) → ℝ≥0∞)
        (s ×ˢ t) ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (s ∩ t)
⊢ Eq (α := ℝ≥0∞)
    ((((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)

Tactic:
rw [comp_apply' _ _ _ <| hs.prod ht]

Premises used: MeasurableSet.prod, ProbabilityTheory.Kernel.comp_apply'
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
simp_rw :
  ∫⁻ (b : β), HMul.hMul (α := ℝ≥0∞) (s.indicator 1 b) (t.indicator 1 b) ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (s ∩ t)
⊢ ∫⁻ (b : β),
      (((copy β : (a : β) → Measure (β × β)) b : Measure (β × β)) : (a : Set (β × β)) → ℝ≥0∞)
        (s ×ˢ t) ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (s ∩ t)

Tactic:
simp_rw [copy_apply, Measure.dirac_apply' _ <| hs.prod ht, Set.indicator_prod_one]

Premises used: MeasureTheory.Measure.dirac_apply', ProbabilityTheory.Kernel.copy_apply, MeasurableSet.prod, Set.indicator_prod_one
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
e_f : ∀ (b : β), HMul.hMul (α := ℝ≥0∞) (s.indicator 1 b) (t.indicator 1 b) = (s ∩ t).indicator 1 b
⊢ ∫⁻ (b : β), HMul.hMul (α := ℝ≥0∞) (s.indicator 1 b) (t.indicator 1 b) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β), (s ∩ t).indicator 1 b ∂(κ : (a : α) → Measure β) a

Tactic:
congr with b
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
b : β
⊢ HMul.hMul (α := ℝ≥0∞) (s.indicator 1 b) (t.indicator 1 b) = (s ∩ t).indicator 1 b

Tactic:
simp [Set.inter_indicator_one]

Premises used: Set.inter_indicator_one
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), (s ∩ t).indicator 1 b ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (s ∩ t)

Tactic:
lintegral_indicator_one <| hs.inter ht

Premises used: MeasureTheory.lintegral_indicator_one, MeasurableSet.inter
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
_ :
  ∫⁻ (b : β), HMul.hMul (α := ℝ≥0∞) (s.indicator 1 b) (t.indicator 1 b) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β), (s ∩ t).indicator 1 b ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (b : β), HMul.hMul (α := ℝ≥0∞) (s.indicator 1 b) (t.indicator 1 b) ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (s ∩ t)

Tactic:
calc
  _ = ∫⁻ b, (s ∩ t).indicator 1 b ∂κ a := by
    congr with b
    simp [Set.inter_indicator_one]
  _ = κ a (s ∩ t) := lintegral_indicator_one <| hs.inter ht

Premises used: Inter.inter, MeasureTheory.lintegral_indicator_one, DFunLike.coe, MeasurableSet.inter
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsMarkovKernel η
κ : Kernel α β
inst_1 : IsMarkovKernel κ
a : α
measure_univ :
  Eq (α := ℝ≥0∞)
    (((Measure.bind.{u_2, u_3} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a) (⇑η : (a : β) → Measure γ) :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        Set.univ :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ IsProbabilityMeasure.{u_3} (α := γ) (m0 := mγ)
    (Measure.bind.{u_2, u_3} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a) (⇑η : (a : β) → Measure γ))

Tactic:
constructor
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsMarkovKernel η
κ : Kernel α β
inst_1 : IsMarkovKernel κ
a : α
measure_univ :
  ∫⁻ (a : β), (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ∂(κ : (a : α) → Measure β) a = 1
⊢ Eq (α := ℝ≥0∞)
    (((Measure.bind.{u_2, u_3} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a) (⇑η : (a : β) → Measure γ) :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        Set.univ :
      ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
rw [Measure.bind_apply .univ η.aemeasurable]

Premises used: MeasureTheory.Measure.bind_apply, ProbabilityTheory.Kernel.aemeasurable, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsMarkovKernel η
κ : Kernel α β
inst_1 : IsMarkovKernel κ
a : α
⊢ ∫⁻ (a : β), (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ∂(κ : (a : α) → Measure β) a = 1

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
η : Kernel β γ
inst_1 : IsZeroOrMarkovKernel η
inl :
  ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (mα := mα) (η ∘ₖ 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.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsZeroOrMarkovKernel η
inst_1 : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
inl :
  ∀ [IsZeroOrMarkovKernel.{u_2, u_3} (α := β) (β := γ) (mα := mβ) (mβ := mγ) 0],
    IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ)
      (Kernel.comp.{u_1, u_2, u_3} (β := β) (mβ := mβ) 0 0)
inl₁ : IsMarkovKernel η → IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (mα := mα) (η ∘ₖ 0)
⊢ IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (mα := mα) (η ∘ₖ 0)

Tactic:
obtain rfl | _ := eq_zero_or_isMarkovKernel η

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
η : Kernel β γ
inst_1 : IsZeroOrMarkovKernel η
h : IsMarkovKernel κ
inr :
  ∀ [IsZeroOrMarkovKernel.{u_2, u_3} (α := β) (β := γ) (mα := mβ) (mβ := mγ) 0],
    IsZeroOrMarkovKernel.{u_1, u_3} (β := γ) (mβ := mγ) (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.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
inst_1 : IsZeroOrMarkovKernel.{u_2, u_3} (α := β) (β := γ) (mα := mβ) (mβ := mγ) 0
⊢ IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
inst_1 : IsZeroOrMarkovKernel.{u_2, u_3} (α := β) (β := γ) (mα := mβ) (mβ := mγ) 0
simpa : IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0
⊢ IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ)
    (Kernel.comp.{u_1, u_2, u_3} (β := β) (mβ := mβ) 0 0)

Tactic:
simpa using by infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsZeroOrMarkovKernel η
inst_1 : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
h : IsMarkovKernel η
⊢ IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsZeroOrMarkovKernel η
inst_1 : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
h : IsMarkovKernel η
simpa : IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0
⊢ IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (mα := mα) (η ∘ₖ 0)

Tactic:
simpa using by infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
h : IsMarkovKernel κ
inst_1 : IsZeroOrMarkovKernel.{u_2, u_3} (α := β) (β := γ) (mα := mβ) (mβ := mγ) 0
⊢ IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
h : IsMarkovKernel κ
inst_1 : IsZeroOrMarkovKernel.{u_2, u_3} (α := β) (β := γ) (mα := mβ) (mβ := mγ) 0
simpa : IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0
⊢ IsZeroOrMarkovKernel.{u_1, u_3} (β := γ) (mβ := mγ) (0 ∘ₖ κ)

Tactic:
simpa using by infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
η : Kernel β γ
inst_1 : IsZeroOrMarkovKernel η
h : IsMarkovKernel κ
h_1 : IsMarkovKernel η
⊢ IsZeroOrMarkovKernel (η ∘ₖ κ)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsFiniteKernel η
κ : Kernel α β
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.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsFiniteKernel η
κ : Kernel α β
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.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsFiniteKernel η
κ : Kernel α β
inst_1 : IsFiniteKernel κ
a : α
⊢ (((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤
    HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound

Tactic:
comp_apply_univ_le κ η a

Premises used: ProbabilityTheory.Kernel.comp_apply_univ_le
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsFiniteKernel η
κ : Kernel α β
inst_1 : IsFiniteKernel κ
a : α
bc : (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound
⊢ HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound ≤
    κ.bound * η.bound

Tactic:
gcongr
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsFiniteKernel η
κ : Kernel α β
inst_1 : IsFiniteKernel κ
a : α
⊢ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound

Tactic:
measure_le_bound κ a Set.univ

Premises used: Set.univ, ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsFiniteKernel η
κ : Kernel α β
inst_1 : IsFiniteKernel κ
a : α
⊢ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound

Tactic:
exact measure_le_bound κ a Set.univ

Premises used: Set.univ, ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsFiniteKernel η
κ : Kernel α β
inst_1 : IsFiniteKernel κ
a : α
calc :
  HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound ≤
    κ.bound * η.bound
⊢ (((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound * η.bound

Tactic:
calc (η ∘ₖ κ) a Set.univ
  _ ≤ κ a Set.univ * η.bound := comp_apply_univ_le κ η a
  _ ≤ κ.bound * η.bound := by gcongr; exact measure_le_bound κ a Set.univ

Premises used: ProbabilityTheory.Kernel.comp, Set.univ, ProbabilityTheory.Kernel.comp_apply_univ_le, DFunLike.coe, ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsSFiniteKernel η
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
simp_rw :
  IsSFiniteKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ)
    (Kernel.sum fun (i : ℕ) ↦ Kernel.sum fun (i_1 : ℕ) ↦ η.seq i ∘ₖ κ.seq i_1)
⊢ IsSFiniteKernel (η ∘ₖ κ)

Tactic:
simp_rw [← kernel_sum_seq κ, ← kernel_sum_seq η, comp_sum_left, comp_sum_right]

Premises used: ProbabilityTheory.Kernel.comp_sum_left, ProbabilityTheory.Kernel.kernel_sum_seq, ProbabilityTheory.Kernel.comp_sum_right
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsSFiniteKernel η
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
⊢ IsSFiniteKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ)
    (Kernel.sum fun (i : ℕ) ↦ Kernel.sum fun (i_1 : ℕ) ↦ η.seq i ∘ₖ κ.seq i_1)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
m n : ℕ
⊢ κ ^ (m + n) = (κ ^ m) ∘ₖ (κ ^ n)

Tactic:
_root_.pow_add κ m n

Premises used: pow_add
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
m n : ℕ
a : α
s : Set α
hs : MeasurableSet s
rw :
  (((κ ^ (n + m) : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s =
    ∫⁻ (b : α), (((κ ^ n : (a : α) → Measure α) b : Measure α) : (a : Set α) → ℝ≥0∞) s ∂(κ ^ m : (a : α) → Measure α) a
⊢ (((κ ^ (m + n) : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s =
    ∫⁻ (b : α), (((κ ^ n : (a : α) → Measure α) b : Measure α) : (a : Set α) → ℝ≥0∞) s ∂(κ ^ m : (a : α) → Measure α) a

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
m n : ℕ
a : α
s : Set α
hs : MeasurableSet s
⊢ (((κ ^ (n + m) : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s =
    ∫⁻ (b : α), (((κ ^ n : (a : α) → Measure α) b : Measure α) : (a : Set α) → ℝ≥0∞) s ∂(κ ^ m : (a : α) → Measure α) a

Tactic:
simp [pow_add, comp_apply' _ _ _ hs]

Premises used: ProbabilityTheory.Kernel.pow_add, ProbabilityTheory.Kernel.comp_apply'
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
n : ℕ
a : α
s : Set α
hs : MeasurableSet s
⊢ (((κ ^ (n + 1) : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s =
    ∫⁻ (b : α), (((κ : (a : α) → Measure α) b : Measure α) : (a : Set α) → ℝ≥0∞) s ∂(κ ^ n : (a : α) → Measure α) a

Tactic:
simpa using pow_add_apply_eq_lintegral _ n 1 _ hs

Premises used: ProbabilityTheory.Kernel.pow_add_apply_eq_lintegral, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel κ
⊢ κ ⊗ₖ η = 0

Tactic:
simp [compProd, h]

Premises used: ProbabilityTheory.Kernel.compProd
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
h : ¬IsSFiniteKernel η
⊢ κ ⊗ₖ η = 0

Tactic:
simp [compProd, h]

Premises used: ProbabilityTheory.Kernel.compProd
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
⊢ Measurable (α := α × α) (β := Measure (β × γ))
    (⇑(swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ
              deterministic (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × β) → (α × β) × β) ⋯ ∘ₖ
            (Kernel.id ∥ₖ copy β) ∘ₖ
          (Kernel.id ∥ₖ κ)) :
      (a : α × α) → Measure (β × γ))

Tactic:
fun_prop