awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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
⊢ Eq (α := ℝ≥0∞) (((((κ + η) ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ ∘ₖ μ + η ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: simp_rw [comp_apply' _ _ _ hs, add_apply, Measure.add_apply, comp_apply' _ _ _ hs,
    lintegral_add_left (Kernel.measurable_coe κ hs)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((((κ + η) ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ ∘ₖ μ + η ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have 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
Tactic: simp_rw [comp_apply' _ _ _ hs, add_apply, Measure.add_apply, comp_apply' _ _ _ hs,
    lintegral_add_left (Kernel.measurable_coe κ hs)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
⊢ η ∘ₖ Kernel.sum κ = Kernel.sum fun (i : ι) ↦ η ∘ₖ κ i
have 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∞)
Tactic: ext _ _ hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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
⊢ 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∞)
have 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∞)
Tactic: simp_rw [sum_apply, comp_apply' _ _ _ hs, Measure.sum_apply _ hs, sum_apply,
    lintegral_sum_measure, comp_apply' _ _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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∞)
⊢ 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∞)
have 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
Tactic: simp_rw [sum_apply, comp_apply' _ _ _ hs, Measure.sum_apply _ hs, sum_apply,
    lintegral_sum_measure, comp_apply' _ _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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
⊢ 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∞)
have 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
Tactic: simp_rw [sum_apply, comp_apply' _ _ _ hs, Measure.sum_apply _ hs, sum_apply,
    lintegral_sum_measure, comp_apply' _ _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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
⊢ 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∞)
have 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
Tactic: simp_rw [sum_apply, comp_apply' _ _ _ hs, Measure.sum_apply _ hs, sum_apply,
    lintegral_sum_measure, comp_apply' _ _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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
⊢ 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∞)
have 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)
Tactic: simp_rw [sum_apply, comp_apply' _ _ _ hs, Measure.sum_apply _ hs, sum_apply,
    lintegral_sum_measure, comp_apply' _ _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞)
    ((((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have rw : ∫⁻ (b : β),
    (((copy β : (a : β) → Measure (β × β)) b : Measure (β × β)) : (a : Set (β × β)) → ℝ≥0∞)
      (s ×ˢ t) ∂(κ : (a : α) → Measure β) a =
  (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (s ∩ t)
Tactic: rw [comp_apply' _ _ _ <| hs.prod ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β),
      (((copy β : (a : β) → Measure (β × β)) b : Measure (β × β)) : (a : Set (β × β)) → ℝ≥0∞)
        (s ×ˢ t) ∂(κ : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (s ∩ t)
have 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)
Tactic: simp_rw [copy_apply, Measure.dirac_apply' _ <| hs.prod ht, Set.indicator_prod_one]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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
have e_f : ∀ (b : β), HMul.hMul (α := ℝ≥0∞) (s.indicator 1 b) (t.indicator 1 b) = (s ∩ t).indicator 1 b
Tactic: congr with b
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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 =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (s ∩ t)
have _ : ∫⁻ (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: 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsMarkovKernel η
κ : Kernel α β
inst_1 : IsMarkovKernel κ
a : α
⊢ IsProbabilityMeasure.{u_3} (α := γ) (m0 := mγ)
    (Measure.bind.{u_2, u_3} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a) (⇑η : (a : β) → Measure γ))
have 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∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsMarkovKernel η
κ : Kernel α β
inst_1 : IsMarkovKernel κ
a : α
⊢ Eq (α := ℝ≥0∞)
    (((Measure.bind.{u_2, u_3} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a) (⇑η : (a : β) → Measure γ) :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        Set.univ :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
have measure_univ : ∫⁻ (a : β), (((η : (a : β) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ∂(κ : (a : α) → Measure β) a = 1
Tactic: rw [Measure.bind_apply .univ η.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
η : Kernel β γ
inst_1 : IsZeroOrMarkovKernel η
⊢ IsZeroOrMarkovKernel (η ∘ₖ κ)
have inl : ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
  IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (mα := mα) (η ∘ₖ 0)
Tactic: obtain rfl | _ := eq_zero_or_isMarkovKernel κ
Cleared hypotheses: κ, inst
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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)
⊢ IsZeroOrMarkovKernel (η ∘ₖ κ)
have inr : IsMarkovKernel κ → IsZeroOrMarkovKernel (η ∘ₖ κ)
Tactic: obtain rfl | _ := eq_zero_or_isMarkovKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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
⊢ IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (mα := mα) (η ∘ₖ 0)
have 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)
Tactic: obtain rfl | _ := eq_zero_or_isMarkovKernel η
Cleared hypotheses: η, inst
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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)
⊢ IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (mα := mα) (η ∘ₖ 0)
have inl₁ : IsMarkovKernel η → IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (mα := mα) (η ∘ₖ 0)
Tactic: obtain rfl | _ := eq_zero_or_isMarkovKernel η
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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 κ
⊢ IsZeroOrMarkovKernel (η ∘ₖ κ)
have inr : ∀ [IsZeroOrMarkovKernel.{u_2, u_3} (α := β) (β := γ) (mα := mβ) (mβ := mγ) 0],
  IsZeroOrMarkovKernel.{u_1, u_3} (β := γ) (mβ := mγ) (0 ∘ₖ κ)
Tactic: obtain rfl | _ := eq_zero_or_isMarkovKernel η
Cleared hypotheses: η, inst_1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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 ∘ₖ κ)
⊢ IsZeroOrMarkovKernel (η ∘ₖ κ)
have inr₁ : IsMarkovKernel η → IsZeroOrMarkovKernel (η ∘ₖ κ)
Tactic: obtain rfl | _ := eq_zero_or_isMarkovKernel η
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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γ)
    (Kernel.comp.{u_1, u_2, u_3} (β := β) (mβ := mβ) 0 0)
have simpa : IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0
Tactic: simpa using by infer_instance
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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α) (η ∘ₖ 0)
have simpa : IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0
Tactic: simpa using by infer_instance
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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γ) (0 ∘ₖ κ)
have simpa : IsZeroOrMarkovKernel.{u_1, u_3} (α := α) (β := γ) (mα := mα) (mβ := mγ) 0
Tactic: simpa using by infer_instance
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsFiniteKernel η
κ : Kernel α β
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.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsFiniteKernel η
κ : Kernel α β
inst_1 : IsFiniteKernel κ
a : α
⊢ HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound ≤
    κ.bound * η.bound
have bc : (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
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 * η.bound
have calc : HMul.hMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) η.bound ≤
  κ.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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst : IsSFiniteKernel η
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
⊢ IsSFiniteKernel (η ∘ₖ κ)
have 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)
Tactic: simp_rw [← kernel_sum_seq κ, ← kernel_sum_seq η, comp_sum_left, comp_sum_right]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
m n : ℕ
a : α
s : Set α
hs : MeasurableSet s
⊢ (((κ ^ (m + n) : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s =
    ∫⁻ (b : α), (((κ ^ n : (a : α) → Measure α) b : Measure α) : (a : Set α) → ℝ≥0∞) s ∂(κ ^ m : (a : α) → Measure α) a
have 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
Tactic: rw [add_comm]