-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem measurable_measure_prod_mk_left_finite [IsFiniteMeasure ν] {s : Set (α × β)}
    (hs : MeasurableSet s) : Measurable fun x => ν (Prod.mk x ⁻¹' s)

Proof state:
case iUnion
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x => ν (Prod.mk x ⁻¹' f i)
this : ∀ (a : α), ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' (i : ℕ), ν (Prod.mk a ⁻¹' f i)
⊢ Measurable fun x => ν (Prod.mk x ⁻¹' ⋃ i, f i)

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

Result:
no goals

Proof state:
case compl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ s : Set (α × β)
hs : MeasurableSet s
ihs : Measurable fun x => ν (Prod.mk x ⁻¹' s)
⊢ Measurable fun x => ν univ - ν (Prod.mk x ⁻¹' s)

Tactic:
exact ihs.const_sub _

Result:
no goals

Proof state:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ : Set (α × β)
s : Set α
hs : s ∈ {s | MeasurableSet s}
t : Set β
⊢ Measurable fun x => ν (Prod.mk x ⁻¹' (fun x1 x2 => x1 ×ˢ x2) s t)

Tactic:
simpa only [mk_preimage_prod_right_eq_if, measure_if]
using measurable_const.indicator hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => ν (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_prod_mk_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_prod_mk_left (hfm i)]
  simpa only [this] using Measurable.ennreal_tsum ihf

Result:
no goals

Proof state:
case iUnion
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x => ν (Prod.mk x ⁻¹' f i)
⊢ Measurable fun x => ν (Prod.mk x ⁻¹' ⋃ i, f i)

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_prod_mk_left (hfm i)]

Result:
case iUnion
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x => ν (Prod.mk x ⁻¹' f i)
this : ∀ (a : α), ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' (i : ℕ), ν (Prod.mk a ⁻¹' f i)
⊢ Measurable fun x => ν (Prod.mk x ⁻¹' ⋃ i, f i)

Proof state:
case basic
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ s : Set (α × β)
hs : s ∈ image2 (fun x1 x2 => x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t}
⊢ Measurable fun x => ν (Prod.mk x ⁻¹' s)

Tactic:
obtain ⟨s, hs, t, -, rfl⟩ := hs

Result:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ : Set (α × β)
s : Set α
hs : s ∈ {s | MeasurableSet s}
t : Set β
⊢ Measurable fun x => ν (Prod.mk x ⁻¹' (fun x1 x2 => x1 ×ˢ x2) s t)

Proof state:
case empty
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
⊢ Measurable fun x => ν (Prod.mk x ⁻¹' ∅)

Tactic:
simp

Result:
no goals

Proof state:
case hn
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x => ν (Prod.mk x ⁻¹' f i)
a : α
⊢ Pairwise (Disjoint on fun i => Prod.mk a ⁻¹' f i)

case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x => ν (Prod.mk x ⁻¹' f i)
a : α
⊢ ∀ (i : ℕ), MeasurableSet (Prod.mk a ⁻¹' f i)

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

Result:
no goals

Proof state:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ : Set (α × β)
s : Set α
hs : s ∈ {s | MeasurableSet s}
t : Set β
⊢ Measurable fun x => ν (Prod.mk x ⁻¹' (fun x1 x2 => x1 ×ˢ x2) s t)

Tactic:
classical simpa only [mk_preimage_prod_right_eq_if, measure_if]
  using measurable_const.indicator hs

Result:
no goals

Proof state:
case compl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ s : Set (α × β)
hs : MeasurableSet s
ihs : Measurable fun x => ν (Prod.mk x ⁻¹' s)
⊢ Measurable fun x => ν (Prod.mk x ⁻¹' sᶜ)

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

Result:
case compl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s✝ s : Set (α × β)
hs : MeasurableSet s
ihs : Measurable fun x => ν (Prod.mk x ⁻¹' s)
⊢ Measurable fun x => ν univ - ν (Prod.mk x ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x => ν (Prod.mk x ⁻¹' f i)
a : α
⊢ ν (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' (i : ℕ), ν (Prod.mk a ⁻¹' f i)

Tactic:
rw [preimage_iUnion, measure_iUnion]

Result:
case hn
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x => ν (Prod.mk x ⁻¹' f i)
a : α
⊢ Pairwise (Disjoint on fun i => Prod.mk a ⁻¹' f i)

case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : IsFiniteMeasure ν
s : Set (α × β)
f : ℕ → Set (α × β)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun x => ν (Prod.mk x ⁻¹' f i)
a : α
⊢ ∀ (i : ℕ), MeasurableSet (Prod.mk a ⁻¹' f i)