awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : IsFiniteMeasure ν
s_1 : Set (α × β)
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:
classical simpa only [mk_preimage_prod_right_eq_if, measure_if]
      using measurable_const.indicator hs

Premises used: Measurable.indicator, Set.mk_preimage_prod_right_eq_if, MeasureTheory.measure_if, measurable_const
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)
compl :
  Measurable (β := ℝ≥0∞) fun (x : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' sᶜ)

Tactic:
simp_rw [preimage_compl, measure_compl (measurable_prodMk_left hs) (measure_ne_top ν _)]

Premises used: MeasureTheory.measure_compl, MeasureTheory.measure_ne_top, Set.preimage_compl, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞)

Tactic:
ihs.const_sub _

Premises used: Measurable.const_sub
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : α) ↦
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞)

Tactic:
exact ihs.const_sub _

Premises used: Measurable.const_sub
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)
h : ∀ (i : ℕ), MeasurableSet (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∞)

Tactic:
rw [preimage_iUnion, measure_iUnion]

Premises used: MeasureTheory.measure_iUnion, Set.preimage_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : α
⊢ Pairwise (α := ℕ) (onFun.{1, u_2 + 1, 1} (β := Set β) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f i)

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

Premises used: Prod.mk, Disjoint.preimage, Pairwise.mono
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : α
⊢ ∀ (i : ℕ), MeasurableSet (Prod.mk a ⁻¹' f i)

Tactic:
fun i ↦ measurable_prodMk_left (hfm i)

Premises used: measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : α
⊢ Pairwise (α := ℕ) (onFun.{1, u_2 + 1, 1} (β := Set β) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f i)

Tactic:
exacts [hfd.mono fun _ _ ↦ .preimage _, fun i ↦ measurable_prodMk_left (hfm i)]

Premises used: measurable_prodMk_left, Pairwise.mono
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)

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)]
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑' (i : ℕ), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' f i) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ⋃ (i : ℕ), f i)

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

Premises used: Measurable.tsum
-- Module: Mathlib.MeasureTheory.Measure.Prod
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ᶜ)
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)
⊢ 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

Premises used: MeasureTheory.measure_compl, Compl.compl, MeasureTheory.measure_ne_top, Measurable.indicator, Set.mk_preimage_prod_right_eq_if, MeasureTheory.measure_if, measurable_const, Set.preimage_compl, Set.iUnion, measurable_prodMk_left, rfl
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
rw : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (sum (sfiniteSeq ν) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)

Tactic:
rw [← sum_sfiniteSeq ν]

Premises used: MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
simp_rw : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ∑' (i : ℕ), (sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (sum (sfiniteSeq ν) : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)

Tactic:
simp_rw [Measure.sum_apply_of_countable]

Premises used: MeasureTheory.Measure.sum_apply_of_countable
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : α) ↦ ∑' (i : ℕ), (sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)

Tactic:
Measurable.tsum (fun i ↦ measurable_measure_prodMk_left_finite hs)

Premises used: Measurable.tsum, measurable_measure_prodMk_left_finite
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : α) ↦ ∑' (i : ℕ), (sfiniteSeq ν i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)

Tactic:
exact Measurable.tsum (fun i ↦ measurable_measure_prodMk_left_finite hs)

Premises used: Measurable.tsum, measurable_measure_prodMk_left_finite
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (y : β) ↦ (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, y)) ⁻¹' s)

Tactic:
measurable_measure_prodMk_left (measurableSet_swap_iff.mpr hs)

Premises used: Iff.mpr, Set.Mem, setOf, measurableSet_swap_iff, measurable_measure_prodMk_left, Set.preimage, Prod.swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
h :
  ∀ (s : Set (α × β)),
    MeasurableSet s → Measurable (β := ℝ≥0∞) fun (b : α) ↦ (map (Prod.mk b) ν : (a : Set (α × β)) → ℝ≥0∞) s
⊢ Measurable (β := Measure (α × β)) fun (x : α) ↦ map (Prod.mk x) ν

Tactic:
apply measurable_of_measurable_coe

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (map (Prod.mk b) ν : (a : Set (α × β)) → ℝ≥0∞) s

Tactic:
simp_rw [map_apply measurable_prodMk_left hs]

Premises used: MeasureTheory.Measure.map_apply, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
exact measurable_measure_prodMk_left hs

Premises used: measurable_measure_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
h :
  ∀ (s : Set (α × β)),
    MeasurableSet s → Measurable (β := ℝ≥0∞) fun (b : β) ↦ (map (fun (x : α) ↦ (x, b)) μ : (a : Set (α × β)) → ℝ≥0∞) s
⊢ Measurable (β := Measure (α × β)) fun (y : β) ↦ map (fun (x : α) ↦ (x, y)) μ

Tactic:
apply measurable_of_measurable_coe

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
h : Measurable (β := ℝ≥0∞) fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, b)) ⁻¹' s)
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦ (map (fun (x : α) ↦ (x, b)) μ : (a : Set (α × β)) → ℝ≥0∞) s

Tactic:
simp_rw [map_apply measurable_prodMk_right hs]

Premises used: MeasureTheory.Measure.map_apply, measurable_prodMk_right
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : β) ↦ (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, b)) ⁻¹' s)

Tactic:
measurable_measure_prodMk_right hs

Premises used: measurable_measure_prodMk_right
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : β) ↦ (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, b)) ⁻¹' s)

Tactic:
exact measurable_measure_prodMk_right hs

Premises used: measurable_measure_prodMk_right
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ∫⁻ (y : β), f x y ∂ν

Tactic:
hf.lintegral_prod_right'

Premises used: Measurable.lintegral_prod_right'
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (y : β) ↦ ∫⁻ (x : α), f (x, y) ∂μ

Tactic:
(measurable_swap_iff.mpr hf).lintegral_prod_right'

Premises used: Iff.mpr, Measurable.lintegral_prod_right', Prod.swap, measurable_swap_iff
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
⊢ Measurable (β := ℝ≥0∞) fun (y : β) ↦ ∫⁻ (x : α), f x y ∂μ

Tactic:
hf.lintegral_prod_left'

Premises used: Measurable.lintegral_prod_left'
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_4
β : Type u_5
inst : MeasureSpace α
inst_1 : MeasureSpace β
⊢ Eq (α := Measure (α × β)) volume (Measure.prod volume volume)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hs : MeasurableSet s
simp :
  (μ.bind fun (x : α) ↦ map (Prod.mk x) ν : (a : Set (α × β)) → ℝ≥0∞) s ≤
    ∫⁻ (x : α), (map (Prod.mk x) ν : (a : Set (α × β)) → ℝ≥0∞) s ∂μ
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s ≤ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ

Tactic:
simp only [Measure.prod, ← map_apply measurable_prodMk_left hs]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.prod, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.bind fun (x : α) ↦ map (Prod.mk x) ν : (a : Set (α × β)) → ℝ≥0∞) s ≤
    ∫⁻ (x : α), (map (Prod.mk x) ν : (a : Set (α × β)) → ℝ≥0∞) s ∂μ

Tactic:
bind_apply_le _ hs

Premises used: MeasureTheory.Measure.bind_apply_le
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.bind fun (x : α) ↦ map (Prod.mk x) ν : (a : Set (α × β)) → ℝ≥0∞) s ≤
    ∫⁻ (x : α), (map (Prod.mk x) ν : (a : Set (α × β)) → ℝ≥0∞) s ∂μ

Tactic:
exact bind_apply_le _ hs

Premises used: MeasureTheory.Measure.bind_apply_le
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
h₁ : t ⊆ T
⊢ LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (S ×ˢ T) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
⊢ s ⊆ S

Tactic:
apply subset_toMeasurable

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
⊢ t ⊆ T

Tactic:
apply subset_toMeasurable

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
⊢ MeasurableSet (S ×ˢ T)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
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∞)
simp_rw₄ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
      ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₅ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) =
    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∞)

Tactic:
simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, mul_comm]

Premises used: MeasureTheory.lintegral_const, Set.mk_preimage_prod_right_eq_if, MeasureTheory.Measure.restrict_apply_univ, MeasureTheory.lintegral_indicator, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.measure_if, mul_comm
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
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∞)
simp_rw₄ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
      ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₅ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) =
    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∞)

Tactic:
classical
      simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, mul_comm]

Premises used: MeasureTheory.lintegral_const, Set.mk_preimage_prod_right_eq_if, MeasureTheory.Measure.restrict_apply_univ, MeasureTheory.lintegral_indicator, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.measure_if, mul_comm
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ rw₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [measure_toMeasurable, measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable