-- Mathlib/Probability/Kernel/MeasurableLIntegral.lean
theorem measurable_kernel_prod_mk_left_of_finite {t : Set (α × β)} (ht : MeasurableSet t)
    (hκs : ∀ a, IsFiniteMeasure (κ a)) : Measurable fun a => κ a (Prod.mk a ⁻¹' t)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ (fun a => (κ a) (if a ∈ t₁ then t₂ else ∅)) = fun a => if a ∈ t₁ then (κ a) t₂ else 0

Tactic:
ext1 a

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
⊢ (κ a) (if a ∈ t₁ then t₂ else ∅) = if a ∈ t₁ then (κ a) t₂ else 0

Proof state:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable fun a => (κ a) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)

Tactic:
simp_rw [mk_preimage_prod_right_eq_if]

Result:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable fun a => (κ a) (if a ∈ t₁ then t₂ else ∅)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ (κ a) (univ \ Prod.mk a ⁻¹' t) = (κ a) univ - (κ a) (Prod.mk a ⁻¹' t)

Tactic:
rw [← Set.diff_inter_self_eq_diff, Set.inter_univ, measure_diff (Set.subset_univ _)]

Result:
case h.h₂
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ NullMeasurableSet (Prod.mk a ⁻¹' t) (κ a)

case h.h_fin
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
h_eq_sdiff : ∀ (a : α), Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t
a : α
⊢ (κ a) (Prod.mk a ⁻¹' t) ≠ ⊤

Proof state:
case hn
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), Measurable fun a => (κ a) (Prod.mk a ⁻¹' f i)
a : α
⊢ Pairwise (Disjoint on fun i => Prod.mk a ⁻¹' f i)

Tactic:
exact h_disj.mono fun _ _ ↦ .preimage _

Result:
no goals

Proof state:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
h_eq_ite : (fun a => (κ a) (if a ∈ t₁ then t₂ else ∅)) = fun a => if a ∈ t₁ then (κ a) t₂ else 0
⊢ Measurable fun a => if a ∈ t₁ then (κ a) t₂ else 0

Tactic:
exact Measurable.ite ht₁ (Kernel.measurable_coe κ ht₂) measurable_const

Result:
no goals

Proof state:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
h_eq_ite : (fun a => (κ a) (if a ∈ t₁ then t₂ else ∅)) = fun a => if a ∈ t₁ then (κ a) t₂ else 0
⊢ Measurable fun a => (κ a) (if a ∈ t₁ then t₂ else ∅)

Tactic:
rw [h_eq_ite]

Result:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
h_eq_ite : (fun a => (κ a) (if a ∈ t₁ then t₂ else ∅)) = fun a => if a ∈ t₁ then (κ a) t₂ else 0
⊢ Measurable fun a => if a ∈ t₁ then (κ a) t₂ else 0

Proof state:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable fun a => (κ a) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)

Tactic:
classical
simp_rw [mk_preimage_prod_right_eq_if]
have h_eq_ite : (fun a => κ a (ite (a ∈ t₁) t₂ ∅)) = fun a => ite (a ∈ t₁) (κ a t₂) 0 := by
  ext1 a
  split_ifs
  exacts [rfl, measure_empty]
rw [h_eq_ite]
exact Measurable.ite ht₁ (Kernel.measurable_coe κ ht₂) measurable_const

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
a : α
⊢ Prod.mk a ⁻¹' tᶜ = univ \ Prod.mk a ⁻¹' t

Tactic:
ext1 b

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
htm : MeasurableSet t
iht : Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
a : α
b : β
⊢ b ∈ Prod.mk a ⁻¹' tᶜ ↔ b ∈ univ \ Prod.mk a ⁻¹' t

Proof state:
case basic
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t✝ : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t : Set (α × β)
ht : ∃ a, MeasurableSet a ∧ ∃ b, MeasurableSet b ∧ a ×ˢ b = t
⊢ Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)

Tactic:
obtain ⟨t₁, ht₁, t₂, ht₂, rfl⟩ := ht

Result:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
⊢ Measurable fun a => (κ a) (Prod.mk a ⁻¹' t₁ ×ˢ t₂)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
⊢ (κ a) (if a ∈ t₁ then t₂ else ∅) = if a ∈ t₁ then (κ a) t₂ else 0

Tactic:
split_ifs

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
h✝ : a ∈ t₁
⊢ (κ a) t₂ = (κ a) t₂

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
t₁ : Set α
ht₁ : MeasurableSet t₁
t₂ : Set β
ht₂ : MeasurableSet t₂
a : α
h✝ : a ∉ t₁
⊢ (κ a) ∅ = 0

Proof state:
case empty
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
⊢ Measurable fun a => (κ a) (Prod.mk a ⁻¹' ∅)

Tactic:
simp only [preimage_empty, measure_empty, measurable_const]

Result:
no goals