-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
/-- The function `(f, x) ↦ update f a x : (Π a, π a) × π a → Π a, π a` is measurable. -/
lemma measurable_update_cylinderEvents' [DecidableEq ι] :
    @Measurable _ _ (.prod (cylinderEvents Δ) (m i)) (cylinderEvents Δ)
      (fun p : (∀ i, π i) × π i ↦ update p.1 i p.2)

Proof state:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
⊢ Measurable fun a => update a.1 i a.2 j

Tactic:
dsimp [update]

Result:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
⊢ Measurable fun a => if h : j = i then ⋯ ▸ a.2 else a.1 j

Proof state:
case pos
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
⊢ Measurable fun a => a.2

Tactic:
exact measurable_snd

Result:
no goals

Proof state:
case pos
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
h : j = i
⊢ Measurable fun a => ⋯ ▸ a.2

Tactic:
subst h

Result:
case pos
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
⊢ Measurable fun a => ⋯ ▸ a.2

Proof state:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
⊢ ∀ ⦃i_1 : ι⦄, i_1 ∈ Δ → Measurable fun a => update a.1 i a.2 i_1

Tactic:
intro j hj

Result:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
⊢ Measurable fun a => update a.1 i a.2 j

Proof state:
case pos
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
⊢ Measurable fun a => ⋯ ▸ a.2

Tactic:
dsimp

Result:
case pos
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
⊢ Measurable fun a => a.2

Proof state:
case neg
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
h : ¬j = i
⊢ Measurable fun a => a.1 j

Tactic:
exact measurable_cylinderEvents_iff.1 measurable_fst hj

Result:
no goals

Proof state:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
⊢ Measurable fun a => if h : j = i then ⋯ ▸ a.2 else a.1 j

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
h : j = i
⊢ Measurable fun a => ⋯ ▸ a.2

case neg
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
h : ¬j = i
⊢ Measurable fun a => a.1 j

Proof state:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
⊢ Measurable fun p => update p.1 i p.2

Tactic:
rw [measurable_cylinderEvents_iff]

Result:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
⊢ ∀ ⦃i_1 : ι⦄, i_1 ∈ Δ → Measurable fun a => update a.1 i a.2 i_1