-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_piEquivPiSubtypeProd_symm (p : δ → Prop) [DecidablePred p] :
    Measurable (Equiv.piEquivPiSubtypeProd p π).symm

Proof state:
case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x => x.2 ⟨j, ⋯⟩

Tactic:
have : Measurable fun (f : ∀ i : { x // ¬p x }, π i.1) => f ⟨j, hj⟩ :=
  measurable_pi_apply (π := fun i : {x // ¬p x} => π i.1) ⟨j, hj⟩

Result:
case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
this : Measurable fun f => f ⟨j, hj⟩
⊢ Measurable fun x => x.2 ⟨j, ⋯⟩

Proof state:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
⊢ Measurable fun x => (piEquivPiSubtypeProd p π).symm x j

Tactic:
simp only [hj, dif_pos, Equiv.piEquivPiSubtypeProd_symm_apply]

Result:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
⊢ Measurable fun x => x.1 ⟨j, ⋯⟩

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
⊢ Measurable ⇑(piEquivPiSubtypeProd p π).symm

Tactic:
refine measurable_pi_iff.2 fun j => ?_

Result:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
⊢ Measurable fun x => (piEquivPiSubtypeProd p π).symm x j

Proof state:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
⊢ Measurable fun x => x.1 ⟨j, ⋯⟩

Tactic:
have : Measurable fun (f : ∀ i : { x // p x }, π i.1) => f ⟨j, hj⟩ :=
  measurable_pi_apply (π := fun i : {x // p x} => π i.1) ⟨j, hj⟩

Result:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
this : Measurable fun f => f ⟨j, hj⟩
⊢ Measurable fun x => x.1 ⟨j, ⋯⟩

Proof state:
case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x => (piEquivPiSubtypeProd p π).symm x j

Tactic:
simp only [hj, Equiv.piEquivPiSubtypeProd_symm_apply, dif_neg, not_false_iff]

Result:
case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x => x.2 ⟨j, ⋯⟩

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
⊢ Measurable fun x => (piEquivPiSubtypeProd p π).symm x j

Tactic:
by_cases hj : p j

Result:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
⊢ Measurable fun x => (piEquivPiSubtypeProd p π).symm x j

case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x => (piEquivPiSubtypeProd p π).symm x j

Proof state:
case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
this : Measurable fun f => f ⟨j, hj⟩
⊢ Measurable fun x => x.2 ⟨j, ⋯⟩

Tactic:
exact Measurable.comp this measurable_snd

Result:
no goals

Proof state:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
this : Measurable fun f => f ⟨j, hj⟩
⊢ Measurable fun x => x.1 ⟨j, ⋯⟩

Tactic:
exact Measurable.comp this measurable_fst

Result:
no goals