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 γ
h : Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) t) 0
rw :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0 ∧
    (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞) 0 fun (x : β) ↦
      (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0

Tactic:
rw [Filter.eventuallyLE_antisymm_iff]

Premises used: Filter.eventuallyLE_antisymm_iff
-- 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 γ
h : Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) t) 0
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0 ∧
    (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞) 0 fun (x : β) ↦
      (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
⟨Filter.EventuallyLE.trans_eq (ae_of_all _ fun _ ↦ measure_mono hst) ht,
    ae_of_all _ fun _ ↦ zero_le⟩

Premises used: zero_le, Filter.EventuallyLE.trans_eq, MeasureTheory.ae_of_all, And.intro, MeasureTheory.measure_mono
-- 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 γ
h : Eq (α := ℝ≥0∞) ((((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set γ
hst : s ⊆ t
mt : MeasurableSet t
ht :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (y : β) ↦ (((η : (a : β) → Measure γ) y : Measure γ) : (a : Set γ) → ℝ≥0∞) t) 0
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞)
      (fun (x : β) ↦ (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0 ∧
    (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞) 0 fun (x : β) ↦
      (((η : (a : β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s

Tactic:
exact ⟨Filter.EventuallyLE.trans_eq (ae_of_all _ fun _ ↦ measure_mono hst) ht,
    ae_of_all _ fun _ ↦ zero_le⟩
-- 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 : α
p : γ → Prop
h : ∀ᵐ (z : γ) ∂((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ), p z
⊢ ∀ᵐ (y : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), p z

Tactic:
ae_null_of_comp_null h

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, ProbabilityTheory.Kernel.ae_null_of_comp_null
-- 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 : α
p : γ → Prop
hp : MeasurableSet.{u_3} (α := γ) {z : γ | p z}
h : ∀ᵐ (y : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), p z
hs :
  ∀
    (h :
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
            {a : β | ¬∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a : Measure γ), p z} :
          ℝ≥0∞)
        (0 : ℝ≥0∞)),
    MeasurableSet.{u_3} (α := γ) {a : γ | ¬p a}
⊢ ∀ᵐ (z : γ) ∂((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ), p z

Tactic:
rwa [ae_iff, comp_null] at *

Premises used: MeasureTheory.ae_iff, ProbabilityTheory.Kernel.comp_null
-- 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 : α
p : γ → Prop
hp : MeasurableSet.{u_3} (α := γ) {z : γ | p z}
h :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {a : β | ¬∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a : Measure γ), p z} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ MeasurableSet.{u_3} (α := γ) {a : γ | ¬p a}

Tactic:
hp.compl

Premises used: Set.Mem, setOf, MeasurableSet.compl
-- 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 : α
p : γ → Prop
hp : MeasurableSet.{u_3} (α := γ) {z : γ | p z}
h :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {a : β | ¬∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) a : Measure γ), p z} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ MeasurableSet.{u_3} (α := γ) {a : γ | ¬p a}

Tactic:
exact hp.compl

Premises used: MeasurableSet.compl
-- 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 : α
p : γ → Prop
hp : MeasurableSet.{u_3} (α := γ) {z : γ | p z}
⊢ (∀ᵐ (z : γ) ∂((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ), p z) ↔
    ∀ᵐ (y : β) ∂((κ : (a : α) → Measure β) a : Measure β), ∀ᵐ (z : γ) ∂((η : (a : β) → Measure γ) y : Measure γ), p z

Tactic:
⟨ae_ae_of_ae_comp, ae_comp_of_ae_ae hp⟩

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_comp, Iff.intro, ProbabilityTheory.Kernel.ae_comp_of_ae_ae
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
hs : MeasurableSet s
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∞)
⊢ η.restrict (s := s) hs ∘ₖ κ = (η ∘ₖ κ).restrict (s := s) hs

Tactic:
ext a t ht
-- Module: Mathlib.Probability.Kernel.Composition.Comp
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
h₁ :
  ∫⁻ (b : β), (((η : (a : β) → Measure γ) b : Measure γ) : (a : Set γ) → ℝ≥0∞) (t ∩ s) ∂(κ : (a : α) → Measure β) a =
    (((η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (t ∩ s)
⊢ 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:
simp_rw [comp_apply' _ _ _ ht, restrict_apply' _ _ _ ht, comp_apply' _ _ _ (ht.inter hs)]

Premises used: ProbabilityTheory.Kernel.restrict_apply', ProbabilityTheory.Kernel.comp_apply', 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 β γ
κ : 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
rw₁ rw₂ :
  ∫⁻ (a : β), ∫⁻ (x : γ), g x ∂(η : (a : β) → Measure γ) a ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (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

Tactic:
rw [comp_apply, Measure.lintegral_bind (Kernel.aemeasurable _) hg.aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.lintegral_bind, ProbabilityTheory.Kernel.aemeasurable, 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
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
⊢ ξ ∘ₖ η ∘ₖ κ = ξ ∘ₖ (η ∘ₖ κ)

Tactic:
ext_fun fun a f hf => ?_

Premises used: ProbabilityTheory.Kernel.ext_fun
-- 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
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
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 => ?_

Premises used: ProbabilityTheory.Kernel.ext_fun
-- 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
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
a : α
f : δ → ℝ≥0∞
hf : Measurable f
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
⊢ ∫⁻ (b : δ), f b ∂(ξ ∘ₖ η ∘ₖ κ : (a : α) → Measure δ) a = ∫⁻ (b : δ), f b ∂(ξ ∘ₖ (η ∘ₖ κ) : (a : α) → Measure δ) a

Tactic:
simp_rw [lintegral_comp _ _ _ hf, lintegral_comp _ _ _ hf.lintegral_kernel]

Premises used: Measurable.lintegral_kernel, ProbabilityTheory.Kernel.lintegral_comp
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
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' := ⋯ } :
                    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∞)
⊢ 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' := ⋯ }

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
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' := ⋯ } :
                  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:
simp [comp_apply' _ _ _ hs, mul_comm]

Premises used: mul_comm, ProbabilityTheory.Kernel.comp_apply'
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsMarkovKernel κ
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∞)
⊢ discard β ∘ₖ κ = discard α

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsMarkovKernel κ
a : α
s : Set PUnit.{u_4 + 1}
h : 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:
simp [comp_discard']

Premises used: ProbabilityTheory.Kernel.comp_discard'
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
mα : MeasurableSpace α
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∞)
⊢ Eq (α := Kernel α (α × α)) (swap α α ∘ₖ copy α) (copy α)

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) (s.indicator 1 (a, a).swap) (s.indicator 1 (a, a))
⊢ Eq (α := ℝ≥0∞)
    ((((swap α α ∘ₖ copy α : (a : α) → Measure (α × α)) a : Measure (α × α)) : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((copy α : (a : α) → Measure (α × α)) a : Measure (α × α)) : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comp_apply, copy_apply, Measure.dirac_bind (Kernel.measurable _), swap_apply' _ hs,
    Measure.dirac_apply' _ hs]

Premises used: MeasureTheory.Measure.dirac_bind, MeasureTheory.Measure.dirac_apply', ProbabilityTheory.Kernel.copy_apply, ProbabilityTheory.Kernel.comp_apply, ProbabilityTheory.Kernel.measurable, ProbabilityTheory.Kernel.swap_apply'
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (s.indicator 1 (a, a).swap) (s.indicator 1 (a, a))

Tactic:
congr
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
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∞)
⊢ Eq (α := (a : α) → Measure γ) (⇑(const β μ ∘ₖ κ) : (a : α) → Measure γ) fun (a : α) ↦
    HSMul.hSMul (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ

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 γ
μ : 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∞)
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∞)
⊢ 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:
simp_rw [comp_apply' _ _ _ hs, const_apply, MeasureTheory.lintegral_const, Measure.smul_apply,
    smul_eq_mul, mul_comm]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.smul_apply, mul_comm, ProbabilityTheory.Kernel.comp_apply', smul_eq_mul, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
inst : IsMarkovKernel κ
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∞)
⊢ const β μ ∘ₖ κ = const α μ

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.Comp
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∞)
h₂ :
  Eq (α := ℝ≥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∞)

Tactic:
simp_rw [const_comp, measure_univ, one_smul, const_apply]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul, ProbabilityTheory.Kernel.const_apply, ProbabilityTheory.Kernel.const_comp
-- Module: Mathlib.Probability.Kernel.Composition.Comp
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ κ : Kernel α β
η : Kernel β γ
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
-- 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
⊢ Eq (α := ℝ≥0∞) ((((η ∘ₖ (μ + κ) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η ∘ₖ μ + η ∘ₖ κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [comp_apply' _ _ _ hs]

Premises used: 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 γ
μ : Kernel α β
κ η : Kernel β γ
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