awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
x : ι
⊢ ∫⁻ (ω : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsProbabilityMeasure μ) (Measure.map f (↑(νs x) : Measure Ω))
            ⋯) :
        Measure Ω') =
    ∫⁻ (ω : Ω), (↑((g : (a : Ω') → ℝ≥0) (f ω)) : ℝ≥0∞) ∂(↑(νs x) : Measure Ω)
have h : Measurable (β := ℝ≥0∞) fun (ω : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞)
Tactic: refine lintegral_map ?_ f_cont.measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω'), (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(ν.map ⋯) : Measure Ω') =
    ∫⁻ (ω : Ω),
      (↑((g.compContinuous { toFun := f, continuous_toFun := f_cont : C(Ω, Ω') } : (a : Ω) → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑ν : Measure Ω)
have h : ∫⁻ (ω : Ω'),
    (↑((g : (a : Ω') → ℝ≥0) ω) :
      ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsProbabilityMeasure μ) (Measure.map f (↑ν : Measure Ω)) sorry) :
      Measure Ω') =
  ∫⁻ (ω : Ω), (↑((g : (a : Ω') → ℝ≥0) (f ω)) : ℝ≥0∞) ∂(↑ν : Measure Ω)
Tactic: simp only [map, compContinuous_apply, ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(νs i) : Measure Ω)) L
      (𝓝 (∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω)))
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
g : Ω' →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω'),
      (↑((g : (a : Ω') → ℝ≥0) ω) :
        ℝ≥0∞) ∂(↑(Subtype.mk (p := fun (μ : Measure Ω') ↦ IsProbabilityMeasure μ) (Measure.map f (↑ν : Measure Ω)) ⋯) :
        Measure Ω') =
    ∫⁻ (ω : Ω), (↑((g : (a : Ω') → ℝ≥0) (f ω)) : ℝ≥0∞) ∂(↑ν : Measure Ω)
have h : Measurable (β := ℝ≥0∞) fun (ω : Ω') ↦ (↑((g : (a : Ω') → ℝ≥0) ω) : ℝ≥0∞)
Tactic: refine lintegral_map ?_ f_cont.measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
inst_2 : TopologicalSpace Ω
inst_3 : OpensMeasurableSpace Ω
inst_4 : TopologicalSpace Ω'
inst_5 : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous[inst_2, inst_4] f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun (ν : ProbabilityMeasure Ω) ↦ ν.map ⋯
have rw : ∀ (x : ProbabilityMeasure Ω),
  ContinuousAt.{u_1, u_2} (Y := ProbabilityMeasure Ω') (fun (ν : ProbabilityMeasure Ω) ↦ ν.map sorry) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : Measure (Measure α)
inst_1 : IsProbabilityMeasure m
hm : ∀ᵐ (μ : Measure α) ∂m, IsProbabilityMeasure μ
⊢ IsProbabilityMeasure m.join
have simp : ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) univ ∂m = 1
Tactic: simp only [isProbabilityMeasure_iff, MeasurableSet.univ, Measure.join_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
m : Measure (Measure α)
inst_1 : IsProbabilityMeasure m
hm : ∀ᵐ (μ : Measure α) ∂m, IsProbabilityMeasure μ
⊢ ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) univ ∂m = 1
have hm₁ : ∀ᵐ (μ : Measure α) ∂m, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: simp_rw [isProbabilityMeasure_iff] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
m : Measure α
inst_2 : IsProbabilityMeasure m
f : α → Measure β
hf₀ : AEMeasurable f m
hf₁ : ∀ᵐ (μ : α) ∂m, IsProbabilityMeasure (f μ)
⊢ IsProbabilityMeasure (m.bind f)
have simp : ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) univ ∂m = 1
Tactic: simp only [isProbabilityMeasure_iff, MeasurableSet.univ, Measure.bind_apply _ hf₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
m : Measure α
inst_2 : IsProbabilityMeasure m
f : α → Measure β
hf₀ : AEMeasurable f m
hf₁ : ∀ᵐ (μ : α) ∂m, IsProbabilityMeasure (f μ)
⊢ ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) univ ∂m = 1
have hf₂ : ∀ᵐ (μ : α) ∂m, Eq (α := ℝ≥0∞) ((f μ : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: simp_rw [isProbabilityMeasure_iff] at hf₁
Cleared hypotheses: hf₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s_1 s : Set (α × β)
hs :
  Membership.mem (γ := Set (Set (α × β)))
    (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t}) s
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
have basic : ∀ (s : Set α) (hs : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s) (t : Set β),
  Measurable (β := ℝ≥0∞) fun (x : α) ↦
    (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t)
Tactic: obtain ⟨s, hs, t, -, rfl⟩ := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s_1 s : Set (α × β)
hs : MeasurableSet s
ihs : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' sᶜ)
have compl : Measurable (β := ℝ≥0∞) fun (x : α) ↦
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞)
Tactic: simp_rw [preimage_compl, measure_compl (measurable_prodMk_left hs) (measure_ne_top ν _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' f i)
a : α
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i) : ℝ≥0∞)
have hn : Pairwise (α := ℕ) (onFun.{1, u_2 + 1, 1} (β := Set β) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f i)
Tactic: rw [preimage_iUnion, measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' f i)
a : α
hn : Pairwise (α := ℕ) (onFun.{1, u_2 + 1, 1} (β := Set β) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f i)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i) : ℝ≥0∞)
have h : ∀ (i : ℕ), MeasurableSet (Prod.mk a ⁻¹' f i)
Tactic: rw [preimage_iUnion, measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' f i)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ⋃ (i : ℕ), f i)
have this : ∀ (a : α),
  Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i) : ℝ≥0∞)
Tactic: have (a : α) : ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, ν (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      exacts [hfd.mono fun _ _ ↦ .preimage _, fun i ↦ measurable_prodMk_left (hfm i)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
have empty : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ∅)
Tactic: induction s, hs using induction_on_inter generateFrom_prod.symm isPiSystem_prod with
  | empty => simp
  | basic s hs =>
    obtain ⟨s, hs, t, -, rfl⟩ := hs
    classical simpa only [mk_preimage_prod_right_eq_if, measure_if]
      using measurable_const.indicator hs
  | compl s hs ihs =>
    simp_rw [preimage_compl, measure_compl (measurable_prodMk_left hs) (measure_ne_top ν _)]
    exact ihs.const_sub _
  | iUnion f hfd hfm ihf =>
    have (a : α) : ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, ν (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      exacts [hfd.mono fun _ _ ↦ .preimage _, fun i ↦ measurable_prodMk_left (hfm i)]
    simpa only [this] using Measurable.tsum ihf
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s : Set (α × β)
hs : MeasurableSet s
empty : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ∅)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
have basic : ∀ (s : Set (α × β))
  (hs :
    Membership.mem (γ := Set (Set (α × β)))
      (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
      s),
  Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
Tactic: induction s, hs using induction_on_inter generateFrom_prod.symm isPiSystem_prod with
  | empty => simp
  | basic s hs =>
    obtain ⟨s, hs, t, -, rfl⟩ := hs
    classical simpa only [mk_preimage_prod_right_eq_if, measure_if]
      using measurable_const.indicator hs
  | compl s hs ihs =>
    simp_rw [preimage_compl, measure_compl (measurable_prodMk_left hs) (measure_ne_top ν _)]
    exact ihs.const_sub _
  | iUnion f hfd hfm ihf =>
    have (a : α) : ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, ν (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      exacts [hfd.mono fun _ _ ↦ .preimage _, fun i ↦ measurable_prodMk_left (hfm i)]
    simpa only [this] using Measurable.tsum ihf
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s : Set (α × β)
hs : MeasurableSet s
empty : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ∅)
basic :
  ∀ (s : Set (α × β))
    (hs :
      Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        s),
    Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
have compl : ∀ (s : Set (α × β)) (hs : MeasurableSet s)
  (ihs : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)),
  Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' sᶜ)
Tactic: induction s, hs using induction_on_inter generateFrom_prod.symm isPiSystem_prod with
  | empty => simp
  | basic s hs =>
    obtain ⟨s, hs, t, -, rfl⟩ := hs
    classical simpa only [mk_preimage_prod_right_eq_if, measure_if]
      using measurable_const.indicator hs
  | compl s hs ihs =>
    simp_rw [preimage_compl, measure_compl (measurable_prodMk_left hs) (measure_ne_top ν _)]
    exact ihs.const_sub _
  | iUnion f hfd hfm ihf =>
    have (a : α) : ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, ν (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      exacts [hfd.mono fun _ _ ↦ .preimage _, fun i ↦ measurable_prodMk_left (hfm i)]
    simpa only [this] using Measurable.tsum ihf
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s : Set (α × β)
hs : MeasurableSet s
empty : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ∅)
basic :
  ∀ (s : Set (α × β))
    (hs :
      Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        s),
    Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
compl :
  ∀ (s : Set (α × β)) (hs : MeasurableSet s)
    (ihs : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)),
    Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' sᶜ)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
have iUnion : ∀ (f : ℕ → Set (α × β)) (hfd : Pairwise (Disjoint on f)) (hfm : ∀ (i : ℕ), MeasurableSet (f i))
  (ihf : ∀ (i : ℕ), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' f i)),
  Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ⋃ (i : ℕ), f i)
Tactic: induction s, hs using induction_on_inter generateFrom_prod.symm isPiSystem_prod with
  | empty => simp
  | basic s hs =>
    obtain ⟨s, hs, t, -, rfl⟩ := hs
    classical simpa only [mk_preimage_prod_right_eq_if, measure_if]
      using measurable_const.indicator hs
  | compl s hs ihs =>
    simp_rw [preimage_compl, measure_compl (measurable_prodMk_left hs) (measure_ne_top ν _)]
    exact ihs.const_sub _
  | iUnion f hfd hfm ihf =>
    have (a : α) : ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' i, ν (Prod.mk a ⁻¹' f i) := by
      rw [preimage_iUnion, measure_iUnion]
      exacts [hfd.mono fun _ _ ↦ .preimage _, fun i ↦ measurable_prodMk_left (hfm i)]
    simpa only [this] using Measurable.tsum ihf
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
have rw : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (sum (sfiniteSeq ν) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
Tactic: rw [← sum_sfiniteSeq ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (sum (sfiniteSeq ν) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
have simp_rw : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ∑' (i : ℕ), (sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
Tactic: simp_rw [Measure.sum_apply_of_countable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
⊢ Measurable (β := Measure (α × β)) fun (x : α) ↦ map (Prod.mk x) ν
have h : ∀ (s : Set (α × β)),
  MeasurableSet s → Measurable (β := ℝ≥0∞) fun (b : α) ↦ (map (Prod.mk b) ν : (a : Set (α × β)) → ℝ≥0∞) s
Tactic: apply measurable_of_measurable_coe
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (map (Prod.mk b) ν : (a : Set (α × β)) → ℝ≥0∞) s
have h : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: simp_rw [map_apply measurable_prodMk_left hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
⊢ Measurable (β := Measure (α × β)) fun (y : β) ↦ map (fun (x : α) ↦ (x, y)) μ
have h : ∀ (s : Set (α × β)),
  MeasurableSet s → Measurable (β := ℝ≥0∞) fun (b : β) ↦ (map (fun (x : α) ↦ (x, b)) μ : (a : Set (α × β)) → ℝ≥0∞) s
Tactic: apply measurable_of_measurable_coe
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦ (map (fun (x : α) ↦ (x, b)) μ : (a : Set (α × β)) → ℝ≥0∞) s
have h : Measurable (β := ℝ≥0∞) fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, b)) ⁻¹' s)
Tactic: simp_rw [map_apply measurable_prodMk_right hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s ≤ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ
have simp : (μ.bind fun (x : α) ↦ map (Prod.mk x) ν : (a : Set (α × β)) → ℝ≥0∞) s ≤
  ∫⁻ (x : α), (map (Prod.mk x) ν : (a : Set (α × β)) → ℝ≥0∞) s ∂μ
Tactic: simp only [Measure.prod, ← map_apply measurable_prodMk_left hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (S ×ˢ T) : ℝ≥0∞)
have h : s ⊆ S
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
h : s ⊆ S
⊢ LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (S ×ˢ T) : ℝ≥0∞)
have h₁ : t ⊆ T
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
simp_rw :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' toMeasurable μ s ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
⊢ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' S ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
have simp_rw₁ : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (if x ∈ toMeasurable μ s then T else ∅) ∂μ =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
Tactic: simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
simp_rw :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' toMeasurable μ s ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₁ :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (if x ∈ toMeasurable μ s then T else ∅) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
⊢ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' S ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
have simp_rw₂ : ∫⁻ (x : α), (toMeasurable μ s).indicator (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) T) x ∂μ =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
Tactic: simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
simp_rw :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' toMeasurable μ s ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₁ :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (if x ∈ toMeasurable μ s then T else ∅) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₂ :
  ∫⁻ (x : α), (toMeasurable μ s).indicator (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) T) x ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
⊢ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' S ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
have simp_rw₃ : ∫⁻ (x : α) in toMeasurable μ s, (ν : (a : Set β) → ℝ≥0∞) T ∂μ =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
Tactic: simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, mul_comm]