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 κ
t : Set (α × β)
ht : MeasurableSet t
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((Kernel.sum κ.seq : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
      (∑' (n : ℕ), (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
n : ℕ
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)

Tactic:
measurable_kernel_prodMk_left_of_finite ht inferInstance

Premises used: inferInstance, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left_of_finite
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((Kernel.sum κ.seq : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
      (∑' (n : ℕ), (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
n : ℕ
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)

Tactic:
exact measurable_kernel_prodMk_left_of_finite ht inferInstance

Premises used: inferInstance, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left_of_finite
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
⊢ ∀ (b : β),
    Prod.mk b ⁻¹' s = {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}

Tactic:
have (b : _) : Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p : (α × β) × γ | (p.1.2, p.2) ∈ s}} := rfl
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this :
  ∀ (b : β),
    Prod.mk b ⁻¹' s = {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}
simp_rw :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
simp_rw [this]
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this :
  ∀ (b : β),
    Prod.mk b ⁻¹' s = {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}

Tactic:
(measurable_kernel_prodMk_left ?_).comp measurable_prodMk_left

Premises used: Measurable.comp, Set.Mem, setOf, Set.preimage, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left, 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 (α × β) γ
inst : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this :
  ∀ (b : β),
    Prod.mk b ⁻¹' s = {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}
refine : MeasurableSet (α := (α × β) × γ) {p : (α × β) × γ | (p.1.2, p.2) ∈ s}
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}

Tactic:
refine (measurable_kernel_prodMk_left ?_).comp measurable_prodMk_left

Premises used: Measurable.comp, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left, 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 (α × β) γ
inst : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this :
  ∀ (b : β),
    Prod.mk b ⁻¹' s = {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}
⊢ MeasurableSet (α := (α × β) × γ) {p : (α × β) × γ | (p.1.2, p.2) ∈ s}

Tactic:
(measurable_fst.snd.prodMk measurable_snd) hs

Premises used: Set.Mem, setOf, Measurable.prodMk, Set.preimage, measurable_snd, measurable_fst, Measurable.snd
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
this :
  ∀ (b : β),
    Prod.mk b ⁻¹' s = {c : γ | Membership.mem (γ := Set ((α × β) × γ)) {p : (α × β) × γ | (p.1.2, p.2) ∈ s} ((a, b), c)}
⊢ MeasurableSet (α := (α × β) × γ) {p : (α × β) × γ | (p.1.2, p.2) ∈ s}

Tactic:
exact (measurable_fst.snd.prodMk measurable_snd) hs

Premises used: Measurable.prodMk, measurable_snd, measurable_fst, Measurable.snd
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
s : Set (β × α)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (y : α) ↦
    (((κ : (a : α) → Measure β) y : Measure β) : (a : Set β) → ℝ≥0∞) ((fun (x : β) ↦ (x, y)) ⁻¹' s)

Tactic:
measurable_kernel_prodMk_left (measurableSet_swap_iff.mpr hs)

Premises used: Iff.mpr, Set.Mem, setOf, measurableSet_swap_iff, Set.preimage, Prod.swap, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
unfold :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), t.indicator (fun (x : α × β) ↦ c) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β), t.indicator (Function.const (α × β) c) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
unfold Function.const

Premises used: Function.const
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
simp_rw :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    HMul.hMul (β := ℝ≥0∞) c ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), t.indicator (fun (x : α × β) ↦ c) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [lintegral_indicator_const_comp measurable_prodMk_left ht _]

Premises used: MeasureTheory.lintegral_indicator_const_comp, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    HMul.hMul (β := ℝ≥0∞) c ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)

Tactic:
Measurable.const_mul (measurable_kernel_prodMk_left ht) c

Premises used: Measurable.const_mul, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    HMul.hMul (β := ℝ≥0∞) c ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)

Tactic:
exact Measurable.const_mul (measurable_kernel_prodMk_left ht) c

Premises used: Measurable.const_mul, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- 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)
⊢ ∀ (a : α × β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) a = uncurry f a

Tactic:
have h : ∀ a, ⨆ n, F n a = uncurry f a := SimpleFunc.iSup_eapprox_apply hf
-- 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 : α × β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) a = uncurry f a
⊢ ∀ (a : α) (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) = f a b

Tactic:
simp only [Prod.forall, uncurry_apply_pair] at h

Premises used: Prod.forall, Function.uncurry_apply_pair
-- 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
simp_rw :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β), ⨆ (n : ℕ), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), f a b ∂(κ : (a : α) → Measure β) a

Tactic:
simp_rw [← h]
-- 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
a : α
hf₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (b : β) ↦ (F n : (a : α × β) → ℝ≥0∞) (a, b)
h_mono : Monotone.{0, u_2} (β := β → ℝ≥0∞) fun (n : ℕ) (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

Tactic:
rw [lintegral_iSup]

Premises used: MeasureTheory.lintegral_iSup
-- 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
a : α
⊢ ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (b : β) ↦ (F n : (a : α × β) → ℝ≥0∞) (a, b)

Tactic:
fun n => (F n).measurable.comp measurable_prodMk_left

Premises used: Measurable.comp, MeasureTheory.SimpleFunc.measurable, measurable_prodMk_left
-- 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
a : α
⊢ ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (b : β) ↦ (F n : (a : α × β) → ℝ≥0∞) (a, b)

Tactic:
exact fun n => (F n).measurable.comp measurable_prodMk_left

Premises used: Measurable.comp, MeasureTheory.SimpleFunc.measurable, measurable_prodMk_left
-- 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
a : α
⊢ Monotone.{0, u_2} (β := β → ℝ≥0∞) fun (n : ℕ) (b : β) ↦ (F n : (a : α × β) → ℝ≥0∞) (a, b)

Tactic:
fun i j hij b => SimpleFunc.monotone_eapprox (uncurry f) hij _

Premises used: Monotone, Prod.mk, MeasureTheory.SimpleFunc.monotone_eapprox, Function.uncurry
-- 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
a : α
⊢ Monotone.{0, u_2} (β := β → ℝ≥0∞) fun (n : ℕ) (b : β) ↦ (F n : (a : α × β) → ℝ≥0∞) (a, b)

Tactic:
exact fun i j hij b => SimpleFunc.monotone_eapprox (uncurry f) hij _

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox, Function.uncurry
-- 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
⊢ ∀ (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 _
-- 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
simp_rw :
  Measurable (β := ℝ≥0∞) fun (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

Tactic:
simp_rw [this]
-- 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
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ⨆ (n : ℕ), ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
.iSup fun n => ?_

Premises used: Measurable.iSup
-- 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
refine :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (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

Tactic:
refine .iSup fun n => ?_
-- 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 : ℕ
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
SimpleFunc.induction
    (motive := fun f => Measurable (fun (a : α) => ∫⁻ (b : β), f (a, b) ∂κ a)) ?_ ?_ (F n)

Premises used: MeasureTheory.SimpleFunc.induction
-- 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 : ℕ
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))
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)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ ∫⁻ (b : β), (F n : (a : α × β) → ℝ≥0∞) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
refine SimpleFunc.induction
    (motive := fun f => Measurable (fun (a : α) => ∫⁻ (b : β), f (a, b) ∂κ a)) ?_ ?_ (F n)

Premises used: MeasureTheory.SimpleFunc.induction
-- 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 : ℕ
c : ℝ≥0∞
t : Set (α × β)
ht : MeasurableSet t
refine_1 :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β), t.indicator (Function.const (α × β) c) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β),
      (SimpleFunc.piecewise t ht (SimpleFunc.const (α × β) c) (SimpleFunc.const (α × β) 0) : (a : α × β) → ℝ≥0∞)
        (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
      SimpleFunc.coe_zero, Set.piecewise_eq_indicator]

Premises used: MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, MeasureTheory.SimpleFunc.coe_const
-- 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 : ℕ
c : ℝ≥0∞
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β), t.indicator (Function.const (α × β) c) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
Kernel.measurable_lintegral_indicator_const (κ := κ) ht c

Premises used: ProbabilityTheory.Kernel.measurable_lintegral_indicator_const
-- 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 : ℕ
c : ℝ≥0∞
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∫⁻ (b : β), t.indicator (Function.const (α × β) c) (a, b) ∂(κ : (a : α) → Measure β) a

Tactic:
exact Kernel.measurable_lintegral_indicator_const (κ := κ) ht c

Premises used: ProbabilityTheory.Kernel.measurable_lintegral_indicator_const