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 β γ
s : Set γ
hs : MeasurableSet s
⊢ η.restrict (s := s) hs ∘ₖ κ = (η ∘ₖ κ).restrict (s := s) hs
have h : ∀ (a : α) (t : Set γ) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞) ((((η.restrict (s := s) hs ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
    (((((η ∘ₖ κ).restrict (s := s) hs : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: ext a t 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 α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
a : α
t : Set γ
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((((η.restrict (s := s) hs ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
    (((((η ∘ₖ κ).restrict (s := s) hs : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
have h : ∫⁻ (b : β),
    (((η.restrict (s := s) hs : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
      t ∂(κ : (a : α) → Measure β) a =
  ((((η ∘ₖ κ).restrict (s := s) hs : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t
Tactic: simp_rw [comp_apply' _ _ _ ht, restrict_apply' _ _ _ ht, comp_apply' _ _ _ (ht.inter 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 β γ
s : Set γ
hs : MeasurableSet s
a : α
t : Set γ
ht : MeasurableSet t
h :
  ∫⁻ (b : β),
      (((η.restrict (s := s) hs : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
        t ∂(κ : (a : α) → Measure β) a =
    ((((η ∘ₖ κ).restrict (s := s) hs : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t
⊢ Eq (α := ℝ≥0∞) ((((η.restrict (s := s) hs ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
    (((((η ∘ₖ κ).restrict (s := s) hs : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
have h₁ : ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) (t ∩ s) ∂(κ : (a : α) → Measure β) a =
  (((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (t ∩ s)
Tactic: simp_rw [comp_apply' _ _ _ ht, restrict_apply' _ _ _ ht, comp_apply' _ _ _ (ht.inter 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 : α
g : γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : γ), g c ∂(η ∘ₖ κ : (a : α) → Measure γ) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a
have rw : ∫⁻ (c : γ), g c ∂Measure.bind.{u_2, u_3} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a) (⇑η : (a : β) → Measure γ) =
  ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a
Tactic: rw [comp_apply, Measure.lintegral_bind (Kernel.aemeasurable _) hg.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 β γ
κ : Kernel α β
a : α
g : γ → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (c : γ),
      g c ∂Measure.bind.{u_2, u_3} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a) (⇑η : (a : β) → Measure γ) =
    ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (c : γ), g c ∂(η ∘ₖ κ : (a : α) → Measure γ) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a
have rw₁ : ∫⁻ (a : β), ∫⁻ (x : γ), g x ∂(η : (a : β) → Measure γ) a ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a
Tactic: rw [comp_apply, Measure.lintegral_bind (Kernel.aemeasurable _) hg.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 γ
δ : Type u_4
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
⊢ ξ ∘ₖ η ∘ₖ κ = ξ ∘ₖ (η ∘ₖ κ)
have refine : ∀ (a : α) (f : δ → ℝ≥0∞) (hf : Measurable f),
  ∫⁻ (b : δ), f b ∂(ξ ∘ₖ η ∘ₖ κ : (a : α) → Measure δ) a = ∫⁻ (b : δ), f b ∂(ξ ∘ₖ (η ∘ₖ κ) : (a : α) → Measure δ) a
Tactic: refine ext_fun fun a f hf => ?_
-- 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
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
a : α
f : δ → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), f b ∂(ξ ∘ₖ η ∘ₖ κ : (a : α) → Measure δ) a = ∫⁻ (b : δ), f b ∂(ξ ∘ₖ (η ∘ₖ κ) : (a : α) → Measure δ) a
have simp_rw : ∫⁻ (b : β),
    ∫⁻ (b : γ), ∫⁻ (b : δ), f b ∂(ξ : (a : γ) → Measure δ) b ∂(η : (a : β) → Measure γ) b ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (b : γ), ∫⁻ (b : δ), f b ∂(ξ : (a : γ) → Measure δ) b ∂(η ∘ₖ κ : (a : α) → Measure γ) a
Tactic: simp_rw [lintegral_comp _ _ _ hf, lintegral_comp _ _ _ hf.lintegral_kernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ discard β ∘ₖ κ =
    {
      toFun := fun (a : α) ↦
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure PUnit.{u_4 + 1})
          ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) (Measure.dirac PUnit.unit),
      measurable' := ⋯ }
have h : ∀ (a : α) (s : Set PUnit.{u_4 + 1}) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((discard β ∘ₖ κ : (a : α) → Measure PUnit.{u_4 + 1}) a : Measure PUnit.{u_4 + 1}) :
          (a : Set PUnit.{u_4 + 1}) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((({
                    toFun := fun (a : α) ↦
                      HSMul.hSMul (α := ℝ≥0∞) (β := Measure PUnit.{u_4 + 1})
                        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
                        (Measure.dirac PUnit.unit),
                    measurable' := sorry } :
                  Kernel α PUnit.{u_4 + 1}) :
                (a : α) → Measure PUnit.{u_4 + 1})
              a :
            Measure PUnit.{u_4 + 1}) :
          (a : Set PUnit.{u_4 + 1}) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsMarkovKernel κ
⊢ discard β ∘ₖ κ = discard α
have h : ∀ (a : α) (s : Set PUnit.{u_4 + 1}),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((discard β ∘ₖ κ : (a : α) → Measure PUnit.{u_4 + 1}) a : Measure PUnit.{u_4 + 1}) :
            (a : Set PUnit.{u_4 + 1}) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((discard α : (a : α) → Measure PUnit.{u_4 + 1}) a : Measure PUnit.{u_4 + 1}) :
            (a : Set PUnit.{u_4 + 1}) → ℝ≥0∞)
          s :
        ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
⊢ Eq (α := Kernel α (α × α)) (swap α α ∘ₖ copy α) (copy α)
have h : ∀ (a : α) (s : Set (α × α)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((swap α α ∘ₖ copy α : (a : α) → Measure (α × α)) a : Measure (α × α)) : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((copy α : (a : α) → Measure (α × α)) a : Measure (α × α)) : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.Comp (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((swap α α ∘ₖ copy α : (a : α) → Measure (α × α)) a : Measure (α × α)) : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((copy α : (a : α) → Measure (α × α)) a : Measure (α × α)) : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (s.indicator 1 (a, a).swap) (s.indicator 1 (a, a))
Tactic: rw [comp_apply, copy_apply, Measure.dirac_bind (Kernel.measurable _), swap_apply' _ hs,
    Measure.dirac_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 γ
μ : Measure γ
κ : Kernel α β
⊢ Eq (α := (a : α) → Measure γ) (⇑(const β μ ∘ₖ κ) : (a : α) → Measure γ) fun (a : α) ↦
    HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ
have h : ∀ (x : α) (s : Set γ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((const β μ ∘ₖ κ : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
          (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 γ
μ : Measure γ
κ : Kernel α β
x : α
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((const β μ ∘ₖ κ : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : ∫⁻ (b : β),
    ((((const β μ : Kernel β γ) : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
      s ∂(κ : (a : α) → Measure β) x =
  (HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
      (a : Set γ) → ℝ≥0∞)
    s
Tactic: simp_rw [comp_apply' _ _ _ hs, const_apply, MeasureTheory.lintegral_const, Measure.smul_apply,
    smul_eq_mul, mul_comm]
-- 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 γ
μ : Measure γ
κ : Kernel α β
x : α
s : Set γ
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      ((((const β μ : Kernel β γ) : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
        (a : Set γ) → ℝ≥0∞)
      s
⊢ Eq (α := ℝ≥0∞) ((((const β μ ∘ₖ κ : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₁ : ∫⁻ (b : β), (μ : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) x =
  (HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
      (a : Set γ) → ℝ≥0∞)
    s
Tactic: simp_rw [comp_apply' _ _ _ hs, const_apply, MeasureTheory.lintegral_const, Measure.smul_apply,
    smul_eq_mul, mul_comm]
-- 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 γ
μ : Measure γ
κ : Kernel α β
x : α
s : Set γ
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      ((((const β μ : Kernel β γ) : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
        (a : Set γ) → ℝ≥0∞)
      s
h₁ :
  ∫⁻ (b : β), (μ : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) x =
    (HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
        (a : Set γ) → ℝ≥0∞)
      s
⊢ Eq (α := ℝ≥0∞) ((((const β μ ∘ₖ κ : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
  (HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
      (a : Set γ) → ℝ≥0∞)
    s
Tactic: simp_rw [comp_apply' _ _ _ hs, const_apply, MeasureTheory.lintegral_const, Measure.smul_apply,
    smul_eq_mul, mul_comm]
-- 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 γ
μ : Measure γ
κ : Kernel α β
x : α
s : Set γ
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      ((((const β μ : Kernel β γ) : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
        (a : Set γ) → ℝ≥0∞)
      s
h₁ :
  ∫⁻ (b : β), (μ : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) x =
    (HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
        (a : Set γ) → ℝ≥0∞)
      s
h₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
    (HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
        (a : Set γ) → ℝ≥0∞)
      s
⊢ Eq (α := ℝ≥0∞) ((((const β μ ∘ₖ κ : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₃ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((μ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [comp_apply' _ _ _ hs, const_apply, MeasureTheory.lintegral_const, Measure.smul_apply,
    smul_eq_mul, mul_comm]
-- 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 γ
μ : Measure γ
κ : Kernel α β
x : α
s : Set γ
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      ((((const β μ : Kernel β γ) : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞)
        s ∂(κ : (a : α) → Measure β) x =
    (HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
        (a : Set γ) → ℝ≥0∞)
      s
h₁ :
  ∫⁻ (b : β), (μ : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) x =
    (HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
        (a : Set γ) → ℝ≥0∞)
      s
h₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
    (HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
        (a : Set γ) → ℝ≥0∞)
      s
h₃ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
    HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      ((μ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((const β μ ∘ₖ κ : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₄ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((μ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [comp_apply' _ _ _ hs, const_apply, MeasureTheory.lintegral_const, Measure.smul_apply,
    smul_eq_mul, mul_comm]
-- 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 γ
μ : Measure γ
κ : Kernel α β
inst : IsMarkovKernel κ
⊢ const β μ ∘ₖ κ = const α μ
have h : ∀ (a : α) (s : Set γ),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((const β μ ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      (((((const α μ : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- 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 γ
μ : Measure γ
κ : Kernel α β
inst : IsMarkovKernel κ
a : α
s : Set γ
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((const β μ ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((const α μ : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  ((HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
        (a : Set γ) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  (((((const α μ : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [const_comp, measure_univ, one_smul, const_apply]
-- 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 γ
μ : Measure γ
κ : Kernel α β
inst : IsMarkovKernel κ
a : α
s : Set γ
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((((const α μ : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((const β μ ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((const α μ : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) 1 μ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  (((((const α μ : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [const_comp, measure_univ, one_smul, const_apply]
-- 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 γ
μ : Measure γ
κ : Kernel α β
inst : IsMarkovKernel κ
a : α
s : Set γ
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((((const α μ : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) 1 μ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((const α μ : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((const β μ ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((((const α μ : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  (((((const α μ : Kernel α γ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [const_comp, measure_univ, one_smul, const_apply]
-- 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 β γ
⊢ η ∘ₖ (μ + κ) = η ∘ₖ μ + η ∘ₖ κ
have h : ∀ (a : α) (s : Set γ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((η ∘ₖ (μ + κ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η ∘ₖ μ + η ∘ₖ κ : (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 γ
μ : Kernel α β
κ η : Kernel β γ
⊢ (κ + η) ∘ₖ μ = κ ∘ₖ μ + η ∘ₖ μ
have h : ∀ (a : α) (s : Set γ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((((κ + η) ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ ∘ₖ μ + η ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s 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
⊢ Eq (α := ℝ≥0∞) (((((κ + η) ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ ∘ₖ μ + η ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (b : β), (((κ + η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(μ : (a : α) → Measure β) a =
  (((κ ∘ₖ μ + η ∘ₖ μ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
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
⊢ 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 (α := 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
Tactic: simp_rw [comp_apply' _ _ _ hs, add_apply, Measure.add_apply, comp_apply' _ _ _ hs,
    lintegral_add_left (Kernel.measurable_coe κ hs)]