awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
pos :
  ∫⁻ (a : α),
      ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a ∂μ =
    ∫⁻ (a : α),
      (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) ∂μ
⊢ Eq (α := ℝ≥0∞) ((((⇑η : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((snd.{u_2, u_3} (α := β) ((⇑(κ ⊗ₖ η) : (a : α) → Measure (β × γ)) ∘ₘ μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s :
      ℝ≥0∞)
have rw : MeasurableSet (α := β × γ) (Prod.snd ⁻¹' s)
Tactic: rw [Measure.bind_apply hs η.aemeasurable, Measure.snd_apply hs,
    Measure.bind_apply _ (Kernel.aemeasurable _), Measure.lintegral_compProd (η.measurable_coe hs)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α),
      ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a ∂μ =
    ∫⁻ (a : α),
      (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) ∂μ
have pos : ∀ (a : α),
  ∫⁻ (b : β), (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
    (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s)
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
⊢ ∫⁻ (b : β), (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
    (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s)
have pos : ∫⁻ (b : β), (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂(κ : (a : α) → Measure β) a
Tactic: rw [Kernel.compProd_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel (α × β) γ
inst : SFinite μ
inst_1 : IsSFiniteKernel η
hκ : IsSFiniteKernel κ
s : Set γ
hs : MeasurableSet s
a : α
pos :
  ∫⁻ (b : β), (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Prod.snd ⁻¹' s) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (b : β), (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) a =
    (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s)
have pos₁ : MeasurableSet (α := β × γ) (Prod.snd ⁻¹' s)
Tactic: rw [Kernel.compProd_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind.{u_2, u_3} (α := β) (mα := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) (⇑η : (a : β) → Measure γ))
have rw : Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
  ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
Tactic: rw [← snd_compProd μ κ, Kernel.prodMkLeft, snd, ← deterministic_comp_eq_map measurable_snd,
    comp_assoc, Kernel.comp_deterministic_eq_comap]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
rw :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind.{u_2, u_3} (α := β) (mα := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) (⇑η : (a : β) → Measure γ))
have rw₁ : Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd sorry) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
  ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
Tactic: rw [← snd_compProd μ κ, Kernel.prodMkLeft, snd, ← deterministic_comp_eq_map measurable_snd,
    comp_assoc, Kernel.comp_deterministic_eq_comap]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
rw :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
rw₁ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind.{u_2, u_3} (α := β) (mα := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) (⇑η : (a : β) → Measure γ))
have rw₂ : Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd sorry) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
  (bind (mα := mβ) (map Prod.snd (μ ⊗ₘ κ)) (⇑η : (a : β) → Measure γ))
Tactic: rw [← snd_compProd μ κ, Kernel.prodMkLeft, snd, ← deterministic_comp_eq_map measurable_snd,
    comp_assoc, Kernel.comp_deterministic_eq_comap]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
rw :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
rw₁ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
rw₂ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind (mα := mβ) (map Prod.snd (μ ⊗ₘ κ)) (⇑η : (a : β) → Measure γ))
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind.{u_2, u_3} (α := β) (mα := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) (⇑η : (a : β) → Measure γ))
have rw₃ : Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd sorry) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
  (bind.{u_2, u_3} (α := β) (mα := mβ) ((⇑(Kernel.deterministic Prod.snd sorry) : (a : α × β) → Measure β) ∘ₘ μ ⊗ₘ κ)
    (⇑η : (a : β) → Measure γ))
Tactic: rw [← snd_compProd μ κ, Kernel.prodMkLeft, snd, ← deterministic_comp_eq_map measurable_snd,
    comp_assoc, Kernel.comp_deterministic_eq_comap]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
rw :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
rw₁ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
rw₂ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind (mα := mβ) (map Prod.snd (μ ⊗ₘ κ)) (⇑η : (a : β) → Measure γ))
rw₃ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind.{u_2, u_3} (α := β) (mα := mβ) ((⇑(Kernel.deterministic Prod.snd ⋯) : (a : α × β) → Measure β) ∘ₘ μ ⊗ₘ κ)
      (⇑η : (a : β) → Measure γ))
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind.{u_2, u_3} (α := β) (mα := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) (⇑η : (a : β) → Measure γ))
have rw₄ : Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd sorry) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
  ((⇑(η ∘ₖ Kernel.deterministic Prod.snd sorry) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
Tactic: rw [← snd_compProd μ κ, Kernel.prodMkLeft, snd, ← deterministic_comp_eq_map measurable_snd,
    comp_assoc, Kernel.comp_deterministic_eq_comap]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
rw :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
rw₁ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑η : (a : β) → Measure γ) ∘ₘ (μ ⊗ₘ κ).snd)
rw₂ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind (mα := mβ) (map Prod.snd (μ ⊗ₘ κ)) (⇑η : (a : β) → Measure γ))
rw₃ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind.{u_2, u_3} (α := β) (mα := mβ) ((⇑(Kernel.deterministic Prod.snd ⋯) : (a : α × β) → Measure β) ∘ₘ μ ⊗ₘ κ)
      (⇑η : (a : β) → Measure γ))
rw₄ :
  Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    ((⇑(η ∘ₖ Kernel.deterministic Prod.snd ⋯) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
⊢ Eq.{u_3 + 1} (α := Measure γ) ((⇑(Kernel.prodMkLeft α η) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
    (bind.{u_2, u_3} (α := β) (mα := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) (⇑η : (a : β) → Measure γ))
have rw₅ : Eq.{u_3 + 1} (α := Measure γ) ((⇑(η.comap Prod.snd sorry) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
  ((⇑(η.comap Prod.snd sorry) : (a : α × β) → Measure γ) ∘ₘ μ ⊗ₘ κ)
Tactic: rw [← snd_compProd μ κ, Kernel.prodMkLeft, snd, ← deterministic_comp_eq_map measurable_snd,
    comp_assoc, Kernel.comp_deterministic_eq_comap]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
f : α → β
hf : Measurable f
⊢ μ ⊗ₘ Kernel.deterministic f hf = map (fun (a : α) ↦ (a, f a)) μ
have rw : Eq (α := Measure (α × β)) (map (fun (a : α) ↦ (id a, f a)) μ) (map (fun (a : α) ↦ (a, f a)) μ)
Tactic: rw [compProd_eq_comp_prod, Kernel.id, Kernel.deterministic_prod_deterministic,
    deterministic_comp_eq_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
⊢ (⇑κ : (a : α) → Measure β) ∘ₘ (μ + ν) =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν)
have simp_rw : (κ ∘ₖ Kernel.const Unit (μ + ν) : (a : Unit) → Measure β) () =
  HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
    ((κ ∘ₖ Kernel.const Unit ν : (a : Unit) → Measure β) () : Measure β)
Tactic: simp_rw [comp_eq_comp_const_apply, Kernel.const_add, Kernel.comp_add_right, Kernel.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
simp_rw :
  (κ ∘ₖ Kernel.const Unit (μ + ν) : (a : Unit) → Measure β) () =
    HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
      ((κ ∘ₖ Kernel.const Unit ν : (a : Unit) → Measure β) () : Measure β)
⊢ (⇑κ : (a : α) → Measure β) ∘ₘ (μ + ν) =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν)
have simp_rw₁ : (κ ∘ₖ HAdd.hAdd (α := Kernel Unit α) (Kernel.const Unit μ) (Kernel.const Unit ν) : (a : Unit) → Measure β) () =
  HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
    ((κ ∘ₖ Kernel.const Unit ν : (a : Unit) → Measure β) () : Measure β)
Tactic: simp_rw [comp_eq_comp_const_apply, Kernel.const_add, Kernel.comp_add_right, Kernel.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ : Kernel α β
simp_rw :
  (κ ∘ₖ Kernel.const Unit (μ + ν) : (a : Unit) → Measure β) () =
    HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
      ((κ ∘ₖ Kernel.const Unit ν : (a : Unit) → Measure β) () : Measure β)
simp_rw₁ :
  (κ ∘ₖ HAdd.hAdd (α := Kernel Unit α) (Kernel.const Unit μ) (Kernel.const Unit ν) : (a : Unit) → Measure β) () =
    HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
      ((κ ∘ₖ Kernel.const Unit ν : (a : Unit) → Measure β) () : Measure β)
⊢ (⇑κ : (a : α) → Measure β) ∘ₘ (μ + ν) =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑κ : (a : α) → Measure β) ∘ₘ ν)
have simp_rw₂ : (HAdd.hAdd (α := Kernel Unit β) (κ ∘ₖ Kernel.const Unit μ) (κ ∘ₖ Kernel.const Unit ν) : (a : Unit) → Measure β) () =
  HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
    ((κ ∘ₖ Kernel.const Unit ν : (a : Unit) → Measure β) () : Measure β)
Tactic: simp_rw [comp_eq_comp_const_apply, Kernel.const_add, Kernel.comp_add_right, Kernel.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
⊢ (⇑(κ + η) : (a : α) → Measure β) ∘ₘ μ =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)
have simp_rw : ((κ + η) ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () =
  HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
    ((η ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
Tactic: simp_rw [comp_eq_comp_const_apply, Kernel.comp_add_left, Kernel.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
simp_rw :
  ((κ + η) ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () =
    HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
      ((η ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
⊢ (⇑(κ + η) : (a : α) → Measure β) ∘ₘ μ =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)
have simp_rw₁ : (HAdd.hAdd (α := Kernel Unit β) (κ ∘ₖ Kernel.const Unit μ) (η ∘ₖ Kernel.const Unit μ) : (a : Unit) → Measure β) () =
  HAdd.hAdd (α := Measure β) (β := Measure β) ((κ ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
    ((η ∘ₖ Kernel.const Unit μ : (a : Unit) → Measure β) () : Measure β)
Tactic: simp_rw [comp_eq_comp_const_apply, Kernel.comp_add_left, Kernel.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
⊢ HAdd.hAdd (α := (a : α) → Measure β) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∘ₘ μ =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)
have rw : (⇑(κ + η) : (a : α) → Measure β) ∘ₘ μ =
  HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)
Tactic: rw [← Kernel.coe_add, add_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
rw :
  (⇑(κ + η) : (a : α) → Measure β) ∘ₘ μ =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)
⊢ HAdd.hAdd (α := (a : α) → Measure β) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∘ₘ μ =
    HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)
have rw₁ : HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ) =
  HAdd.hAdd (α := Measure β) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)
Tactic: rw [← Kernel.coe_add, add_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
a : ℝ≥0∞
⊢ (⇑κ : (a : α) → Measure β) ∘ₘ (a • μ) = HSMul.hSMul (β := Measure β) a ((⇑κ : (a : α) → Measure β) ∘ₘ μ)
have h : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure β) ∘ₘ (a • μ) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (β := Measure β) a ((⇑κ : (a : α) → Measure β) ∘ₘ μ) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
⊢ AbsolutelyContinuous.{u_3} (α := γ) (_m0 := mγ) ((⇑κ : (a : α) → Measure γ) ∘ₘ μ) ((⇑κ : (a : α) → Measure γ) ∘ₘ ν)
have refine : ∀ (s : Set γ) (hs : MeasurableSet s)
  (hs_zero : Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure γ) ∘ₘ ν : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure γ) ∘ₘ μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
μ ν : Measure α
hμν : μ ≪ ν
κ : Kernel α γ
s : Set γ
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure γ) ∘ₘ ν : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure γ) ∘ₘ μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : ∀
  (hs_zero :
    (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s)
      0),
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s) 0
Tactic: rw [Measure.bind_apply hs (Kernel.aemeasurable _),
    lintegral_eq_zero_iff (Kernel.measurable_coe _ hs)] at hs_zero ⊢
Cleared hypotheses: hs_zero
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
⊢ AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((⇑κ : (a : α) → Measure β) ∘ₘ μ) ((⇑η : (a : α) → Measure β) ∘ₘ μ)
have refine : ∀ (s : Set β) (hs : MeasurableSet s)
  (hs_zero : Eq (α := ℝ≥0∞) ((((⇑η : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
s : Set β
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((((⇑η : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : ∀
  (hs_zero :
    (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
      0),
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s) 0
Tactic: rw [Measure.bind_apply hs (Kernel.aemeasurable _),
    lintegral_eq_zero_iff (Kernel.measurable_coe _ hs)] at hs_zero ⊢
Cleared hypotheses: hs_zero
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureComp (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη :
  ∀ᵐ (a : α) ∂μ,
    AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a) ((η : (a : α) → Measure β) a)
s : Set β
hs : MeasurableSet s
hs_zero :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s) 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s) 0
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α |
            (fun (x : α) ↦
                Eq (α := ℝ≥0∞)
                  ((fun (a : α) ↦ ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)) x) (0 x))
              x}
          x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α)
                {x : α |
                  (fun (a : α) ↦
                      AbsolutelyContinuous.{u_2} (α := β) (_m0 := mβ) ((κ : (a : α) → Measure β) a)
                        ((η : (a : α) → Measure β) a))
                    x}
                x →
              Membership.mem (γ := Set α)
                {x : α |
                  (fun (x : α) ↦
                      Eq (α := ℝ≥0∞)
                        ((fun (a : α) ↦ ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)) x)
                        (0 x))
                    x}
                x}
          x}
    a
Tactic: filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_zero