α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
⊢ Measurable fun x => ↑(piEquivPiSubtypeProd p π).symm x j
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
⊢ Measurable ↑(piEquivPiSubtypeProd p π).symm
refine' measurable_pi_iff.2 fun j => _
case pos
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
⊢ Measurable fun x => ↑(piEquivPiSubtypeProd p π).symm x j

case neg
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x => ↑(piEquivPiSubtypeProd p π).symm x j
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
⊢ Measurable fun x => ↑(piEquivPiSubtypeProd p π).symm x j
by_cases hj : p j
case pos
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
⊢ Measurable fun x => Prod.fst x { val := j, property := (_ : p j) }
case pos
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
⊢ Measurable fun x => ↑(piEquivPiSubtypeProd p π).symm x j
simp only [hj, dif_pos, Equiv.piEquivPiSubtypeProd_symm_apply]
case pos
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
this : Measurable fun f => f { val := j, property := hj }
⊢ Measurable fun x => Prod.fst x { val := j, property := (_ : p j) }
case pos
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
⊢ Measurable fun x => Prod.fst x { val := j, property := (_ : p j) }
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⟩
no goals
case pos
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : p j
this : Measurable fun f => f { val := j, property := hj }
⊢ Measurable fun x => Prod.fst x { val := j, property := (_ : p j) }
exact Measurable.comp this measurable_fst
case neg
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x => Prod.snd x { val := j, property := (_ : ¬p j) }
case neg
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x => ↑(piEquivPiSubtypeProd p π).symm x j
simp only [hj, Equiv.piEquivPiSubtypeProd_symm_apply, dif_neg, not_false_iff]
case neg
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
this : Measurable fun f => f { val := j, property := hj }
⊢ Measurable fun x => Prod.snd x { val := j, property := (_ : ¬p j) }
case neg
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable fun x => Prod.snd x { val := j, property := (_ : ¬p j) }
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⟩
no goals
case neg
α : Type ?u.366644
β : Type ?u.366647
γ : Type ?u.366650
δ : Type u_1
δ' : Type ?u.366656
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝³ : MeasurableSpace α
inst✝² : (a : δ) → MeasurableSpace (π a)
inst✝¹ : MeasurableSpace γ
p : δ → Prop
inst✝ : DecidablePred p
j : δ
hj : ¬p j
this : Measurable fun f => f { val := j, property := hj }
⊢ Measurable fun x => Prod.snd x { val := j, property := (_ : ¬p j) }
exact Measurable.comp this measurable_snd