awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) = f a b
this :
  ∀ (a : α),
    ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a =
      ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
refine_2 :
  Disjoint (α := Set (α × β)) (support (M := ℝ≥0∞) (⇑g₁ : (a : α × β) → ℝ≥0∞))
      (support (M := ℝ≥0∞) (⇑g₂ : (a : α × β) → ℝ≥0∞)) →
    (fun (f : SimpleFunc (α × β) ℝ≥0∞) ↦
          Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (f : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)
        g₁ →
      (fun (f : SimpleFunc (α × β) ℝ≥0∞) ↦
            Measurable (β := ℝ≥0∞) fun (a : α) ↦
              ∫⁻ (b : β), (f : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)
          g₂ →
        (fun (f : SimpleFunc (α × β) ℝ≥0∞) ↦
            Measurable (β := ℝ≥0∞) fun (a : α) ↦
              ∫⁻ (b : β), (f : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)
          (g₁ + g₂)
⊢ Disjoint (α := Set (α × β)) (support (M := ℝ≥0∞) (⇑g₁ : (a : α × β) → ℝ≥0∞))
      (support (M := ℝ≥0∞) (⇑g₂ : (a : α × β) → ℝ≥0∞)) →
    (fun (f : SimpleFunc (α × β) ℝ≥0∞) ↦
          Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (f : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)
        g₁ →
      (fun (f : SimpleFunc (α × β) ℝ≥0∞) ↦
            Measurable (β := ℝ≥0∞) fun (a : α) ↦
              ∫⁻ (b : β), (f : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)
          g₂ →
        (fun (f : SimpleFunc (α × β) ℝ≥0∞) ↦
            Measurable (β := ℝ≥0∞) fun (a : α) ↦
              ∫⁻ (b : β), (f : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)
          (g₁ + g₂)

Tactic:
_
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) = f a b
this :
  ∀ (a : α),
    ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a =
      ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
h_1 :
  Disjoint (α := Set (α × β)) (support (M := ℝ≥0∞) (⇑g₁ : (a : α × β) → ℝ≥0∞))
    (support (M := ℝ≥0∞) (⇑g₂ : (a : α × β) → ℝ≥0∞))
hm₁ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
hm₂ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
refine_2 :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((g₁ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞)
        ((g₂ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞) ∂(κ : (a : α) → Measure β) a
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₁ + g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
simp only [SimpleFunc.coe_add, Pi.add_apply]

Premises used: MeasureTheory.SimpleFunc.coe_add, Pi.add_apply
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) = f a b
this :
  ∀ (a : α),
    ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a =
      ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
h_1 :
  Disjoint (α := Set (α × β)) (support (M := ℝ≥0∞) (⇑g₁ : (a : α × β) → ℝ≥0∞))
    (support (M := ℝ≥0∞) (⇑g₂ : (a : α × β) → ℝ≥0∞))
hm₁ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
hm₂ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
h₁ :
  ∀ (a : α),
    ∫⁻ (b : β),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((g₁ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞)
          ((g₂ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞) ∂(κ : (a : α) → Measure β) a =
      HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞)
        (fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)
        (fun (a : α) ↦ ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a) a
⊢ (fun (a : α) ↦
      ∫⁻ (b : β),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((g₁ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞)
          ((g₂ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞) ∂(κ : (a : α) → Measure β) a) =
    HAdd.hAdd (α := (a : α) → ℝ≥0∞)
      (fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a) fun (a : α) ↦
      ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
ext1 a
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) = f a b
this :
  ∀ (a : α),
    ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a =
      ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
h_1 :
  Disjoint (α := Set (α × β)) (support (M := ℝ≥0∞) (⇑g₁ : (a : α × β) → ℝ≥0∞))
    (support (M := ℝ≥0∞) (⇑g₂ : (a : α × β) → ℝ≥0∞))
hm₁ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
hm₂ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
a : α
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦ (g₁ : (a : α × β) → ℝ≥0∞) (a, b)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) = f a b
this :
  ∀ (a : α),
    ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a =
      ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
h_1 :
  Disjoint (α := Set (α × β)) (support (M := ℝ≥0∞) (⇑g₁ : (a : α × β) → ℝ≥0∞))
    (support (M := ℝ≥0∞) (⇑g₂ : (a : α × β) → ℝ≥0∞))
hm₁ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
hm₂ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
a : α
h₁ :
  ∫⁻ (b : β),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((g₁ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞)
        ((g₂ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a +
      ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
h₂ h₃ :
  ∫⁻ (a_1 : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, a_1) ∂(κ : (a : α) → Measure β) a +
      ∫⁻ (a_1 : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, a_1) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a +
      ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (b : β),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((g₁ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞)
        ((g₂ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞) ∂(κ : (a : α) → Measure β) a =
    HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞)
      (fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)
      (fun (a : α) ↦ ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a) a

Tactic:
rw [Pi.add_apply, lintegral_add_left (by fun_prop)]

Premises used: MeasureTheory.lintegral_add_left, Pi.add_apply
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) = f a b
this :
  ∀ (a : α),
    ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a =
      ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
h_1 :
  Disjoint (α := Set (α × β)) (support (M := ℝ≥0∞) (⇑g₁ : (a : α × β) → ℝ≥0∞))
    (support (M := ℝ≥0∞) (⇑g₂ : (a : α × β) → ℝ≥0∞))
hm₁ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
hm₂ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ (fun (a : α) ↦
      ∫⁻ (b : β),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((g₁ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞)
          ((g₂ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞) ∂(κ : (a : α) → Measure β) a) =
    HAdd.hAdd (α := (a : α) → ℝ≥0∞)
      (fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a) fun (a : α) ↦
      ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
have h_add :
      (fun a => ∫⁻ b, g₁ (a, b) + g₂ (a, b) ∂κ a) =
        (fun a => ∫⁻ b, g₁ (a, b) ∂κ a) + fun a => ∫⁻ b, g₂ (a, b) ∂κ a := by
      ext1 a
      rw [Pi.add_apply, lintegral_add_left (by fun_prop)]
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) = f a b
this :
  ∀ (a : α),
    ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a =
      ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
h_1 :
  Disjoint (α := Set (α × β)) (support (M := ℝ≥0∞) (⇑g₁ : (a : α × β) → ℝ≥0∞))
    (support (M := ℝ≥0∞) (⇑g₂ : (a : α × β) → ℝ≥0∞))
hm₁ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
hm₂ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
h_add :
  (fun (a : α) ↦
      ∫⁻ (b : β),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((g₁ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞)
          ((g₂ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞) ∂(κ : (a : α) → Measure β) a) =
    HAdd.hAdd (α := (a : α) → ℝ≥0∞)
      (fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a) fun (a : α) ↦
      ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
refine_2 :
  Measurable
    (HAdd.hAdd (α := (a : α) → ℝ≥0∞)
      (fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a) fun (a : α) ↦
      ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((g₁ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞)
        ((g₂ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞) ∂(κ : (a : α) → Measure β) a

Tactic:
rw [h_add]
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) = f a b
this :
  ∀ (a : α),
    ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a =
      ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
h_1 :
  Disjoint (α := Set (α × β)) (support (M := ℝ≥0∞) (⇑g₁ : (a : α × β) → ℝ≥0∞))
    (support (M := ℝ≥0∞) (⇑g₂ : (a : α × β) → ℝ≥0∞))
hm₁ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
hm₂ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
h_add :
  (fun (a : α) ↦
      ∫⁻ (b : β),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((g₁ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞)
          ((g₂ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞) ∂(κ : (a : α) → Measure β) a) =
    HAdd.hAdd (α := (a : α) → ℝ≥0∞)
      (fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a) fun (a : α) ↦
      ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ Measurable
    (HAdd.hAdd (α := (a : α) → ℝ≥0∞)
      (fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a) fun (a : α) ↦
      ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)

Tactic:
Measurable.add hm₁ hm₂

Premises used: Measurable.add
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) = f a b
this :
  ∀ (a : α),
    ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a =
      ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
h_1 :
  Disjoint (α := Set (α × β)) (support (M := ℝ≥0∞) (⇑g₁ : (a : α × β) → ℝ≥0∞))
    (support (M := ℝ≥0∞) (⇑g₂ : (a : α × β) → ℝ≥0∞))
hm₁ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
hm₂ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
h_add :
  (fun (a : α) ↦
      ∫⁻ (b : β),
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((g₁ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞)
          ((g₂ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞) ∂(κ : (a : α) → Measure β) a) =
    HAdd.hAdd (α := (a : α) → ℝ≥0∞)
      (fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a) fun (a : α) ↦
      ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ Measurable
    (HAdd.hAdd (α := (a : α) → ℝ≥0∞)
      (fun (a : α) ↦ ∫⁻ (b : β), (g₁ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a) fun (a : α) ↦
      ∫⁻ (b : β), (g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)

Tactic:
exact Measurable.add hm₁ hm₂

Premises used: Measurable.add
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
a : α
inst : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
x :
  Measurable.{u_2, 0} (α := β) (β := ℝ≥0∞)
    ((fun (x : α × β) ↦ ∫⁻ (y : γ), (fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)) (x, y) ∂(η : (a : α × β) → Measure γ) x) ∘
      fun (x : β) ↦ (a, x))
⊢ Measurable (β := ℝ≥0∞) fun (x : β) ↦ ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x)

Tactic:
change
    Measurable
      ((fun x => ∫⁻ y, (fun u : (α × β) × γ => f (u.1.2, u.2)) (x, y) ∂η x) ∘ fun x => (a, x))

Premises used: Measurable, Function.comp, Prod.mk, Prod.fst, Prod.snd, DFunLike.coe, MeasureTheory.lintegral
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
a : α
inst : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
⊢ Measurable.{u_2, 0} (α := β) (β := ℝ≥0∞)
    ((fun (x : α × β) ↦ ∫⁻ (y : γ), (fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)) (x, y) ∂(η : (a : α × β) → Measure γ) x) ∘
      fun (x : β) ↦ (a, x))

Tactic:
(Measurable.lintegral_kernel_prod_right' (κ := η)
    (f := (fun u ↦ f (u.fst.snd, u.snd))) ?_).comp measurable_prodMk_left

Premises used: Measurable.comp, Measurable.lintegral_kernel_prod_right', measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
a : α
inst : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
refine : Measurable (β := ℝ≥0∞) fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)
⊢ Measurable.{u_2, 0} (α := β) (β := ℝ≥0∞)
    ((fun (x : α × β) ↦ ∫⁻ (y : γ), (fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)) (x, y) ∂(η : (a : α × β) → Measure γ) x) ∘
      fun (x : β) ↦ (a, x))

Tactic:
refine (Measurable.lintegral_kernel_prod_right' (κ := η)
    (f := (fun u ↦ f (u.fst.snd, u.snd))) ?_).comp measurable_prodMk_left

Premises used: Measurable.comp, Measurable.lintegral_kernel_prod_right', measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
a : α
inst : IsSFiniteKernel η
f : β × γ → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), f a b ∂(κ.restrict (s := s) hs : (a : α) → Measure β) a

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : β × α → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (y : α) ↦ ∫⁻ (x : β), f (x, y) ∂(κ : (a : α) → Measure β) y

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : β → α → ℝ≥0∞
hf : Measurable (uncurry f)
⊢ Measurable (β := ℝ≥0∞) fun (y : α) ↦ ∫⁻ (x : β), f x y ∂(κ : (a : α) → Measure β) y

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : β → α → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ ∫⁻ (a : β), f a b ∂(κ.restrict (s := s) hs : (a : α) → Measure β) b

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : β → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), f b ∂(κ : (a : α) → Measure β) a

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
f : β → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable (α := α × β) (β := ℝ≥0∞) (uncurry fun (a : α) ↦ f)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
⊢ IsMarkovKernel (mα := m𝓧) (mβ := mΩ) (Measure.condKernel (Measure.map Prod.swap (μ ⊗ₘ κ)))

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = Measure.map Prod.swap (μ ⊗ₘ κ)

Tactic:
simpa using ((μ ⊗ₘ κ).map Prod.swap).disintegrate ((μ ⊗ₘ κ).map Prod.swap).condKernel

Premises used: MeasureTheory.Measure.map, MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate, Prod.swap, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
rw :
  Eq (α := Measure (𝓧 × Ω)) (Measure.map Prod.swap (μ ⊗ₘ κ))
    ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
rw₁ rw₂ : Eq (α := Measure (𝓧 × Ω)) (Measure.map Prod.swap (μ ⊗ₘ κ)) (Measure.map Prod.swap (μ ⊗ₘ κ))
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ

Tactic:
rw [compProd_posterior_eq_map_swap, Measure.swap_comp]

Premises used: MeasureTheory.Measure.swap_comp, ProbabilityTheory.compProd_posterior_eq_map_swap
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
rw :
  Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
      ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
      (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
    μ ⊗ₘ κ
rw₁ : (⇑(Kernel.swap 𝓧 Ω ∘ₖ Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ
rw₂ : (⇑Kernel.id : (a : Ω × 𝓧) → Measure (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ
rw₃ rw₄ : μ ⊗ₘ κ = μ ⊗ₘ κ
⊢ (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = μ ⊗ₘ κ

Tactic:
rw [compProd_posterior_eq_swap_comp, Measure.comp_assoc, Kernel.swap_swap, Measure.id_comp]

Premises used: ProbabilityTheory.Kernel.swap_swap, MeasureTheory.Measure.comp_assoc, MeasureTheory.Measure.id_comp, ProbabilityTheory.compProd_posterior_eq_swap_comp
-- Module: Mathlib.Probability.Kernel.Posterior
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
rw rw₁ : ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ
⊢ Measure.bind (α := 𝓧 × 𝓧) (mα := Prod.instMeasurableSpace)
      (Measure.bind (α := 𝓧) (mα := m𝓧) ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ)
        (⇑(Kernel.copy 𝓧) : (a : 𝓧) → Measure (𝓧 × 𝓧)))
      (⇑(Kernel.id ∥ₖ κ†μ) : (a : 𝓧 × 𝓧) → Measure (𝓧 × Ω)) =
    ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ

Tactic:
rw [← Measure.compProd_eq_parallelComp_comp_copy_comp]

Premises used: MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp