awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), f a b ∂(κ : (a : α) → Measure β) a
have simp_rw : Measurable (β := ℝ≥0∞) fun (a : α) ↦
  ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [← h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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
a : α
⊢ ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a =
    ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
have hf₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (b : β) ↦ (F n : (a : α × β) → ℝ≥0∞) (a, b)
Tactic: rw [lintegral_iSup]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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
a : α
hf₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (b : β) ↦ (F n : (a : α × β) → ℝ≥0∞) (a, b)
⊢ ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a =
    ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
have h_mono : Monotone.{0, u_2} (β := β → ℝ≥0∞) fun (n : ℕ) (b : β) ↦ (F n : (a : α × β) → ℝ≥0∞) (a, b)
Tactic: rw [lintegral_iSup]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (hypothesis)
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
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
have this : ∀ (a : α),
  ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a =
    ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: have : ∀ a, (∫⁻ b, ⨆ n, F n (a, b) ∂κ a) = ⨆ n, ∫⁻ b, F n (a, b) ∂κ a := by
    intro a
    rw [lintegral_iSup]
    · exact fun n => (F n).measurable.comp measurable_prodMk_left
    · exact fun i j hij b => SimpleFunc.monotone_eapprox (uncurry f) hij _
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
have simp_rw : Measurable (β := ℝ≥0∞) fun (a : α) ↦
  ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
have refine : ∀ (n : ℕ),
  Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: refine .iSup fun n => ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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 : ℕ
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
have refine_1 : ∀ (c : ℝ≥0∞) {s : Set (α × β)} (hs : MeasurableSet s),
  (fun (f : SimpleFunc (α × β) ℝ≥0∞) ↦
      Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (f : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)
    (SimpleFunc.piecewise s hs (SimpleFunc.const (α × β) c) (SimpleFunc.const (α × β) 0))
Tactic: refine SimpleFunc.induction
    (motive := fun f => Measurable (fun (a : α) => ∫⁻ (b : β), f (a, b) ∂κ a)) ?_ ?_ (F n)
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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 : ℕ
refine_1 :
  ∀ (c : ℝ≥0∞) {s : Set (α × β)} (hs : MeasurableSet s),
    (fun (f : SimpleFunc (α × β) ℝ≥0∞) ↦
        Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (f : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a)
      (SimpleFunc.piecewise s hs (SimpleFunc.const (α × β) c) (SimpleFunc.const (α × β) 0))
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
have refine_2 : ∀ ⦃f g : SimpleFunc (α × β) ℝ≥0∞⦄,
  Disjoint (α := Set (α × β)) (support (M := ℝ≥0∞) (⇑f : (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)
        f →
      (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)
          (f + g)
Tactic: refine SimpleFunc.induction
    (motive := fun f => Measurable (fun (a : α) => ∫⁻ (b : β), f (a, b) ∂κ a)) ?_ ?_ (F n)
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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 : ℕ
c : ℝ≥0∞
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β),
      (SimpleFunc.piecewise t ht (SimpleFunc.const (α × β) c) (SimpleFunc.const (α × β) 0) : (a : α × β) → ℝ≥0∞)
        (a, b) ∂(κ : (a : α) → Measure β) a
have refine_1 : Measurable (β := ℝ≥0∞) fun (a : α) ↦
  ∫⁻ (b : β), t.indicator (Function.const (α × β) c) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
      SimpleFunc.coe_zero, Set.piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (g₁ + g₂ : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
have 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
Tactic: simp only [SimpleFunc.coe_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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
have 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
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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 : α
⊢ ∫⁻ (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
have 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
Tactic: rw [Pi.add_apply, lintegral_add_left (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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
⊢ ∫⁻ (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
have 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
Tactic: rw [Pi.add_apply, lintegral_add_left (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (hypothesis)
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
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((g₁ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞)
        ((g₂ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞) ∂(κ : (a : α) → Measure β) a
have 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
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)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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 (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((g₁ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞)
        ((g₂ : (a : α × β) → ℝ≥0∞) (a, b) : ℝ≥0∞) ∂(κ : (a : α) → Measure β) a
have 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)
Tactic: rw [h_add]
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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 (x : β) ↦ ∫⁻ (y : γ), f (x, y) ∂(η : (a : α × β) → Measure γ) (a, x)
have 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))
Tactic: change
    Measurable
      ((fun x => ∫⁻ y, (fun u : (α × β) × γ => f (u.1.2, u.2)) (x, y) ∂η x) ∘ fun x => (a, x))
-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableLIntegral (goal)
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))
have refine : Measurable (β := ℝ≥0∞) fun (u : (α × β) × γ) ↦ f (u.1.2, u.2)
Tactic: refine (Measurable.lintegral_kernel_prod_right' (κ := η)
    (f := (fun u ↦ f (u.fst.snd, u.snd))) ?_).comp measurable_prodMk_left
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ
have rw : Eq (α := Measure (𝓧 × Ω)) (Measure.map Prod.swap (μ ⊗ₘ κ))
  ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
Tactic: rw [compProd_posterior_eq_map_swap, Measure.swap_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
⊢ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = (⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ
have rw₁ : Eq (α := Measure (𝓧 × Ω)) (Measure.map Prod.swap (μ ⊗ₘ κ)) (Measure.map Prod.swap (μ ⊗ₘ κ))
Tactic: rw [compProd_posterior_eq_map_swap, Measure.swap_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : StandardBorelSpace Ω
inst_3 : Nonempty Ω
⊢ (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = μ ⊗ₘ κ
have rw : Measure.bind (α := 𝓧 × Ω) (mα := Prod.instMeasurableSpace)
    ((⇑(Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (𝓧 × Ω)) ∘ₘ μ ⊗ₘ κ)
    (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) =
  μ ⊗ₘ κ
Tactic: rw [compProd_posterior_eq_swap_comp, Measure.comp_assoc, Kernel.swap_swap, Measure.id_comp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Posterior (goal)
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 (Ω × 𝓧)) =
    μ ⊗ₘ κ
⊢ (⇑(Kernel.swap 𝓧 Ω) : (a : 𝓧 × Ω) → Measure (Ω × 𝓧)) ∘ₘ ((⇑κ : (a : Ω) → Measure 𝓧) ∘ₘ μ) ⊗ₘ κ†μ = μ ⊗ₘ κ
have rw₁ : (⇑(Kernel.swap 𝓧 Ω ∘ₖ Kernel.swap Ω 𝓧) : (a : Ω × 𝓧) → Measure (Ω × 𝓧)) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ κ
Tactic: rw [compProd_posterior_eq_swap_comp, Measure.comp_assoc, Kernel.swap_swap, Measure.id_comp]