awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
pos :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y
neg :
  ∀ (hE : ¬CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : ¬CompleteSpace E
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y

Tactic:
simp [integral, hE, stronglyMeasurable_const]

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.integral
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)

Tactic:
haveI : TopologicalSpace.SeparableSpace (range (uncurry f) ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
⊢ 0 ∈ range (uncurry f) ∪ {0}

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
⊢ StronglyMeasurable (f' n)

Tactic:
StronglyMeasurable.indicator ?_ (measurableSet_kernel_integrable hf)

Premises used: MeasureTheory.StronglyMeasurable.indicator, ProbabilityTheory.measurableSet_kernel_integrable
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
refine : StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
⊢ StronglyMeasurable (f' n)

Tactic:
refine StronglyMeasurable.indicator ?_ (measurableSet_kernel_integrable hf)

Premises used: MeasureTheory.StronglyMeasurable.indicator, ProbabilityTheory.measurableSet_kernel_integrable
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
x : α
⊢ {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range

Tactic:
Finset.Subset.trans (Finset.filter_subset _ _) (SimpleFunc.range_comp_subset_range _ _)

Premises used: MeasureTheory.SimpleFunc.range_comp_subset_range, Finset.Subset.trans, Finset.filter_subset
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
x : α
⊢ {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range

Tactic:
exact Finset.Subset.trans (Finset.filter_subset _ _) (SimpleFunc.range_comp_subset_range _ _)

Premises used: MeasureTheory.SimpleFunc.range_comp_subset_range, Finset.Subset.trans, Finset.filter_subset
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
⊢ ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range

Tactic:
have : ∀ x, ((s' n x).range.filter fun x => x ≠ 0) ⊆ (s n).range := by
      intro
      exact Finset.Subset.trans (Finset.filter_subset _ _) (SimpleFunc.range_comp_subset_range _ _)
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
simp :
  StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    ∑ x_1 ∈ (s n).range,
      Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x)
          (preimage (β := E) (⇑(s' n x) : (a : β) → E) {x_1}) •
        x_1
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦ SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)

Tactic:
simp only [SimpleFunc.integral_eq_sum_of_subset (this _)]

Premises used: MeasureTheory.SimpleFunc.integral_eq_sum_of_subset
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    ∑ x_1 ∈ (s n).range,
      Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x)
          (preimage (β := E) (⇑(s' n x) : (a : β) → E) {x_1}) •
        x_1

Tactic:
Finset.stronglyMeasurable_fun_sum _ fun x _ => ?_

Premises used: Finset.stronglyMeasurable_fun_sum
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
refine :
  ∀ x ∈ (s n).range,
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x_2 : α) ↦
      Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x_2)
          (preimage (β := E) (⇑(s' n x_2) : (a : β) → E) {x}) •
        x
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    ∑ x_1 ∈ (s n).range,
      Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x)
          (preimage (β := E) (⇑(s' n x) : (a : β) → E) {x_1}) •
        x_1

Tactic:
refine Finset.stronglyMeasurable_fun_sum _ fun x _ => ?_

Premises used: Finset.stronglyMeasurable_fun_sum
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
h : x ∈ (s n).range
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x_1 : α) ↦
    Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x_1)
        (preimage (β := E) (⇑(s' n x_1) : (a : β) → E) {x}) •
      x

Tactic:
(Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _

Premises used: Measurable.stronglyMeasurable, MeasureTheory.Measure.real, MeasureTheory.StronglyMeasurable.smul_const, Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
h : x ∈ (s n).range
refine :
  Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
    (((κ : (a : α) → Measure β) x_1 : Measure β) : (a : Set β) → ℝ≥0∞)
      (preimage (β := E) (⇑(s' n x_1) : (a : β) → E) {x})
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x_1 : α) ↦
    Measure.real.{u_2} (α := β) (m := mβ) ((κ : (a : α) → Measure β) x_1)
        (preimage (β := E) (⇑(s' n x_1) : (a : β) → E) {x}) •
      x

Tactic:
refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _

Premises used: Measurable.stronglyMeasurable, MeasureTheory.StronglyMeasurable.smul_const, Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
h : x ∈ (s n).range
simp :
  Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
    (((κ : (a : α) → Measure β) x_1 : Measure β) : (a : Set β) → ℝ≥0∞)
      (Prod.mk x_1 ⁻¹' preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
    (((κ : (a : α) → Measure β) x_1 : Measure β) : (a : Set β) → ℝ≥0∞)
      (preimage (β := E) (⇑(s' n x_1) : (a : β) → E) {x})

Tactic:
simp only [s', SimpleFunc.coe_comp, preimage_comp]

Premises used: Set.preimage_comp, MeasureTheory.SimpleFunc.coe_comp
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
h : x ∈ (s n).range
ht : MeasurableSet (α := α × β) (preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦
    (((κ : (a : α) → Measure β) x_1 : Measure β) : (a : Set β) → ℝ≥0∞)
      (Prod.mk x_1 ⁻¹' preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})

Tactic:
apply Kernel.measurable_kernel_prodMk_left

Premises used: ProbabilityTheory.Kernel.measurable_kernel_prodMk_left
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
h : x ∈ (s n).range
⊢ MeasurableSet (α := α × β) (preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})

Tactic:
(s n).measurableSet_fiber x

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
h : x ∈ (s n).range
⊢ MeasurableSet (α := α × β) (preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})

Tactic:
exact (s n).measurableSet_fiber x

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
⊢ ∀ (n : ℕ), StronglyMeasurable (f' n)

Tactic:
have hf' : ∀ n, StronglyMeasurable (f' n) := by
    intro n; refine StronglyMeasurable.indicator ?_ (measurableSet_kernel_integrable hf)
    have : ∀ x, ((s' n x).range.filter fun x => x ≠ 0) ⊆ (s n).range := by
      intro
      exact Finset.Subset.trans (Finset.filter_subset _ _) (SimpleFunc.range_comp_subset_range _ _)
    simp only [SimpleFunc.integral_eq_sum_of_subset (this _)]
    refine Finset.stronglyMeasurable_fun_sum _ fun x _ => ?_
    refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
    simp only [s', SimpleFunc.coe_comp, preimage_comp]
    apply Kernel.measurable_kernel_prodMk_left
    exact (s n).measurableSet_fiber x
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : IsSFiniteKernel κ
inst_2 : NormedSpace ℝ E
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : TopologicalSpace.SeparableSpace.{u_4} (↑(range (uncurry f) ∪ {0}) : Type u_4)
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E :=
  fun (n : ℕ) ↦
    indicator {x : α | @Integrable _ _ _ _ mβ (f x) ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
      SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
rw :
  ∀ (x : α),
    Tendsto.{0, u_4} (β := E) (fun (i : ℕ) ↦ f' i x) atTop
      (𝓝 (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y))
⊢ Tendsto f' atTop (𝓝 fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f x y)

Tactic:
rw [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds