awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : ∀ (i : ι), IsFiniteMeasure (μ i)
i : ι
f : X i → E
hf : Integrable f (μ i)
⊢ ∀ a ∈ Finset.erase Finset.univ i,
    Ne (α := ENNReal) ((μ a : (a : Set (X a)) → ENNReal) Set.univ : ENNReal) (⊤ : ENNReal)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : ∀ (i : ι), IsFiniteMeasure (μ i)
i : ι
f : X i → E
hf : Integrable f (μ i)
⊢ Integrable f
    (HSMul.hSMul (α := ENNReal) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (X j)) → ENNReal) Set.univ) (μ i))

Tactic:
exact hf.smul_measure <| ENNReal.prod_ne_top (by finiteness)

Premises used: ENNReal.prod_ne_top, MeasureTheory.Integrable.smul_measure
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : ∀ (i : ι), IsFiniteMeasure (μ i)
i : ι
f : X i → E
hf : Integrable f (μ i)
rw rw₁ rw₂ :
  Integrable f
    (HSMul.hSMul (α := ENNReal) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (X j)) → ENNReal) Set.univ) (μ i))
⊢ @Integrable _ _ _ _ (mX i) f (map (fun (x : (i : ι) → X i) ↦ x i) (Measure.pi (α := X) μ))

Tactic:
classical
  rw [Measure.pi_map_eval]
  exact hf.smul_measure <| ENNReal.prod_ne_top (by finiteness)

Premises used: MeasureTheory.Measure.pi_map_eval, ENNReal.prod_ne_top, MeasureTheory.Integrable.smul_measure
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → NormedAddCommGroup (X i)
inst_2 : ∀ (i : ι), IsFiniteMeasure (μ i)
i : ι
h : Integrable id (μ i)
⊢ Integrable (ε := X i) (fun (x : (i : ι) → X i) ↦ x i) (Measure.pi (α := X) μ)

Tactic:
integrable_comp_eval h

Premises used: MeasureTheory.integrable_comp_eval
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf : AEStronglyMeasurable f (μ i)
hφ : AEMeasurable (Function.eval (β := X) i) (Measure.pi (α := X) μ)
hfm : AEStronglyMeasurable (m₀ := mX i) f (map (Function.eval (β := X) i) (Measure.pi (α := X) μ))
⊢ Eq.{u_4 + 1} (α := E) (∫ (x : (i : ι) → X i), f (x i) ∂Measure.pi (α := X) μ) (∫ (x : X i), f x ∂μ i)

Tactic:
rw [← (measurePreserving_eval μ i).map_eq, integral_map]

Premises used: MeasureTheory.integral_map, MeasureTheory.measurePreserving_eval, MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf : AEStronglyMeasurable f (μ i)
⊢ Measurable (α := (x : ι) → X x) (Function.eval (β := X) i)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf : AEStronglyMeasurable f (μ i)
⊢ AEMeasurable (Function.eval (β := X) i) (Measure.pi (α := X) μ)

Tactic:
exact Measurable.aemeasurable (by fun_prop)

Premises used: Measurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf hfm hfm₁ hfm₂ hfm₃ : AEStronglyMeasurable f (μ i)
⊢ AEStronglyMeasurable (m₀ := mX i) f (map (Function.eval (β := X) i) (Measure.pi (α := X) μ))

Tactic:
rwa [(measurePreserving_eval μ i).map_eq]

Premises used: MeasureTheory.measurePreserving_eval, MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → NormedAddCommGroup (X i)
inst_2 : (i : ι) → NormedSpace ℝ (X i)
inst_3 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
inst_4 : OpensMeasurableSpace.{u_3} (X i)
inst_5 : SecondCountableTopology.{u_3} (X i)
⊢ Eq (α := X i) (∫ (x : (i : ι) → X i), x i ∂Measure.pi (α := X) μ) (∫ (x : X i), x ∂μ i)

Tactic:
integral_comp_eval aestronglyMeasurable_id

Premises used: MeasureTheory.integral_comp_eval, aestronglyMeasurable_id
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
simp_rw : MeasurableSet.{u_1} (α := α) {x : α | HasFiniteIntegral (f x) ν}
⊢ MeasurableSet.{u_1} (α := α) {x : α | Integrable (f x) ν}

Tactic:
simp_rw [Integrable, hf.of_uncurry_left.aestronglyMeasurable, true_and]

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Integrable, true_and, MeasureTheory.StronglyMeasurable.of_uncurry_left
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet.{u_1} (α := α) {x : α | HasFiniteIntegral (f x) ν}

Tactic:
measurableSet_lt (Measurable.lintegral_prod_right hf.enorm) measurable_const

Premises used: MeasureTheory.StronglyMeasurable.enorm, setOf, measurableSet_lt, measurable_const, MeasureTheory.HasFiniteIntegral, Measurable.lintegral_prod_right
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet.{u_1} (α := α) {x : α | HasFiniteIntegral (f x) ν}

Tactic:
exact measurableSet_lt (Measurable.lintegral_prod_right hf.enorm) measurable_const

Premises used: measurableSet_lt, measurable_const, Measurable.lintegral_prod_right
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
pos : ∀ (hE : CompleteSpace E), StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
neg : ∀ (hE : ¬CompleteSpace E), StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : ¬CompleteSpace E
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν

Tactic:
simp [integral, hE, stronglyMeasurable_const]

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)

Tactic:
haveI : SeparableSpace (range (uncurry f) ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
⊢ 0 ∈ range (uncurry f) ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
n : ℕ
⊢ StronglyMeasurable (f' n)

Tactic:
StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)

Premises used: measurableSet_integrable, MeasureTheory.StronglyMeasurable.indicator
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
n : ℕ
refine : StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
⊢ StronglyMeasurable (f' n)

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

Premises used: measurableSet_integrable, MeasureTheory.StronglyMeasurable.indicator
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
n : ℕ
x : α
⊢ {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range

Tactic:
Finset.Subset.trans (Finset.filter_subset _ _) ?_

Premises used: Finset.Subset.trans, Finset.filter_subset
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
n : ℕ
x : α
refine : (s' n x).range ⊆ (s n).range
⊢ {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range

Tactic:
refine Finset.Subset.trans (Finset.filter_subset _ _) ?_

Premises used: Finset.Subset.trans, Finset.filter_subset
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
n : ℕ
x : α
y : E
simp_rw :
  Membership.mem (γ := Set E) (range.{u_3, u_2 + 1} (ι := β) (⇑(s' n x) : (a : β) → E)) y →
    Membership.mem (γ := Set E) (range (ι := α × β) (⇑(s n) : (a : α × β) → E)) y
⊢ y ∈ (s' n x).range → y ∈ (s n).range

Tactic:
simp_rw [SimpleFunc.mem_range]

Premises used: MeasureTheory.SimpleFunc.mem_range
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
n : ℕ
x : α
z : β
⊢ Membership.mem.{u_3, u_3} (α := E) (γ := Set E) (range (ι := α × β) (⇑(s n) : (a : α × β) → E))
    ((s' n x : (a : β) → E) z : E)

Tactic:
⟨(x, z), rfl⟩

Premises used: Set.Mem, setOf, Prod.mk, Exists.intro, Set.range, rfl
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
n : ℕ
x : α
z : β
⊢ Membership.mem.{u_3, u_3} (α := E) (γ := Set E) (range (ι := α × β) (⇑(s n) : (a : α × β) → E))
    ((s' n x : (a : β) → E) z : E)

Tactic:
exact ⟨(x, z), rfl⟩
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (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 x; refine Finset.Subset.trans (Finset.filter_subset _ _) ?_; intro y
      simp_rw [SimpleFunc.mem_range]; rintro ⟨z, rfl⟩; exact ⟨(x, z), rfl⟩
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
simp :
  StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦
    ∑ x_1 ∈ (s n).range, ν.real (preimage (β := E) (⇑(s' n x) : (a : β) → E) {x_1}) • x_1
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ SimpleFunc.integral ν (s' n x)

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

Premises used: MeasureTheory.SimpleFunc.integral_eq_sum_of_subset
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x)
n : ℕ
this : ∀ (x : α), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦
    ∑ x_1 ∈ (s n).range, ν.real (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.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (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_3} (β := E) fun (x_2 : α) ↦
      ν.real (preimage (β := E) (⇑(s' n x_2) : (a : β) → E) {x}) • x
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦
    ∑ x_1 ∈ (s n).range, ν.real (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.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (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_3} (β := E) fun (x_1 : α) ↦ ν.real (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.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (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 : Set β) → ℝ≥0∞) (preimage (β := E) (⇑(s' n x_1) : (a : β) → E) {x})
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x_1 : α) ↦ ν.real (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.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)
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 (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (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 : Set β) → ℝ≥0∞) (Prod.mk x_1 ⁻¹' preimage (β := E) (⇑(s n) : (a : α × β) → E) {x})
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : α) ↦ (ν : (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