awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
basic :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅)
basic₁ :
  ∀
    (h_eq_ite :
      Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
        (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
        fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅)
basic₂ :
  ∀
    (h_eq_ite :
      Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
        (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (if a ∈ t₁ then t₂ else ∅))
        fun (a : α) ↦ if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      if a ∈ t₁ then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t₂ else 0
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)

Tactic:
classical
    simp_rw [mk_preimage_prod_right_eq_if]
    have h_eq_ite : (fun a => κ a (ite (a ∈ t₁) t₂ ∅)) = fun a => ite (a ∈ t₁) (κ a t₂) 0 := by
      ext1 a
      split_ifs
      exacts [rfl, measure_empty]
    rw [h_eq_ite]
    exact Measurable.ite ht₁ (Kernel.measurable_coe κ ht₂) measurable_const

Premises used: Set.mk_preimage_prod_right_eq_if, Measurable.ite, ProbabilityTheory.Kernel.measurable_coe, measurable_const
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
a : α
h : ∀ (b : β), b ∈ Prod.mk a ⁻¹' tᶜ ↔ b ∈ univ \ Prod.mk a ⁻¹' t
⊢ Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t

Tactic:
ext1 b
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
a : α
b : β
⊢ b ∈ Prod.mk a ⁻¹' tᶜ ↔ b ∈ univ \ Prod.mk a ⁻¹' t

Tactic:
simp only [mem_compl_iff, mem_preimage, mem_diff, mem_univ, true_and]

Premises used: Set.mem_diff, Set.mem_univ, Set.mem_compl_iff, Set.mem_preimage, true_and
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
⊢ ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t

Tactic:
have h_eq_sdiff : ∀ a, Prod.mk a ⁻¹' tᶜ = Set.univ \ Prod.mk a ⁻¹' t := by
      intro a
      ext1 b
      simp only [mem_compl_iff, mem_preimage, mem_diff, mem_univ, true_and]
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
compl :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' tᶜ)

Tactic:
simp_rw [h_eq_sdiff]
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
h :
  ∀ (a : α),
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t) =
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t))
    fun (a : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)

Tactic:
ext1 a
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
h : NullMeasurableSet (Prod.mk a ⁻¹' t) ((κ : (a : α) → Measure β) a)
h₁ :
  Ne (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)

Tactic:
rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]

Premises used: Set.subset_univ, Set.inter_univ, Set.diff_inter_self_eq_diff, MeasureTheory.measure_diff
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ NullMeasurableSet (Prod.mk a ⁻¹' t) ((κ : (a : α) → Measure β) a)

Tactic:
(measurable_prodMk_left htm).nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ NullMeasurableSet (Prod.mk a ⁻¹' t) ((κ : (a : α) → Measure β) a)

Tactic:
exact (measurable_prodMk_left htm).nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ Ne (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ Ne (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t))
    fun (a : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)

Tactic:
have : (fun a => κ a (Set.univ \ Prod.mk a ⁻¹' t)) =
        fun a => κ a Set.univ - κ a (Prod.mk a ⁻¹' t) := by
      ext1 a
      rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]
      · exact (measurable_prodMk_left htm).nullMeasurableSet
      · exact measure_ne_top _ _
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t))
    fun (a : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
compl :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t)

Tactic:
rw [this]
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t))
    fun (a : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)

Tactic:
Measurable.sub (Kernel.measurable_coe κ MeasurableSet.univ) iht

Premises used: Measurable.sub, ProbabilityTheory.Kernel.measurable_coe, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t_1 : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
t : Set (α × β)
htm : MeasurableSet t
iht :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (univ \ Prod.mk a ⁻¹' t))
    fun (a : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)

Tactic:
exact Measurable.sub (Kernel.measurable_coe κ MeasurableSet.univ) iht

Premises used: Measurable.sub, ProbabilityTheory.Kernel.measurable_coe, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i)
a : α
hn : Pairwise (α := ℕ) (onFun.{1, u_2 + 1, 1} (β := Set β) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f i)
h : ∀ (i : ℕ), MeasurableSet (Prod.mk a ⁻¹' f i)
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i) : ℝ≥0∞)

Tactic:
rw [preimage_iUnion, measure_iUnion]

Premises used: MeasureTheory.measure_iUnion, Set.preimage_iUnion
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i)
a : α
⊢ Pairwise (α := ℕ) (onFun.{1, u_2 + 1, 1} (β := Set β) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f i)

Tactic:
h_disj.mono fun _ _ ↦ .preimage _

Premises used: Prod.mk, Disjoint.preimage, Pairwise.mono
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i)
a : α
⊢ Pairwise (α := ℕ) (onFun.{1, u_2 + 1, 1} (β := Set β) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f i)

Tactic:
exact h_disj.mono fun _ _ ↦ .preimage _

Premises used: Pairwise.mono
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i)
a : α
⊢ ∀ (i : ℕ), MeasurableSet (Prod.mk a ⁻¹' f i)

Tactic:
fun i ↦ measurable_prodMk_left (hf_meas i)

Premises used: measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i)
a : α
⊢ ∀ (i : ℕ), MeasurableSet (Prod.mk a ⁻¹' f i)

Tactic:
exact fun i ↦ measurable_prodMk_left (hf_meas i)

Premises used: measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i)
⊢ ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑' (i : ℕ), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i) : ℝ≥0∞)

Tactic:
have (a : α) : κ a (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, κ a (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      · exact h_disj.mono fun _ _ ↦ .preimage _
      · exact fun i ↦ measurable_prodMk_left (hf_meas i)
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i)
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑' (i : ℕ), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i)

Tactic:
simpa only [this] using Measurable.tsum hf

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

Tactic:
rw [← Kernel.kernel_sum_seq κ]

Premises used: ProbabilityTheory.Kernel.kernel_sum_seq
-- Module: Mathlib.Probability.Kernel.MeasurableLIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
⊢ ∀ (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∞)

Tactic:
have (a : _) : Kernel.sum (Kernel.seq κ) a (Prod.mk a ⁻¹' t) =
      ∑' n, Kernel.seq κ n a (Prod.mk a ⁻¹' t) :=
    Kernel.sum_apply' _ _ (measurable_prodMk_left ht)
-- 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∞)
simp_rw :
  Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∑' (n : ℕ), (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    (((Kernel.sum κ.seq : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)

Tactic:
simp_rw [this]
-- 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∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∑' (n : ℕ), (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)

Tactic:
Measurable.tsum fun n => ?_

Premises used: Measurable.tsum
-- 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∞)
refine :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (a : α) ↦
      (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ∑' (n : ℕ), (((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' t)

Tactic:
refine Measurable.tsum fun n => ?_

Premises used: Measurable.tsum