case pos
α : Type ?u.370700
β : Type ?u.370703
γ : Type ?u.370706
δ : Type u_1
δ' : Type ?u.370712
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : j = i
⊢ Measurable fun v => TProd.elim v hj

case neg
α : Type ?u.370700
β : Type ?u.370703
γ : Type ?u.370706
δ : Type u_1
δ' : Type ?u.370712
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v hj
α : Type ?u.370700
β : Type ?u.370703
γ : Type ?u.370706
δ : Type u_1
δ' : Type ?u.370712
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
⊢ Measurable fun v => TProd.elim v hj
by_cases hji : j = i
case pos
α : Type ?u.370700
β : Type ?u.370703
γ : Type ?u.370706
δ : Type u_1
δ' : Type ?u.370712
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
is : List δ
j : δ
hj : j ∈ j :: is
⊢ Measurable fun v => TProd.elim v hj
case pos
α : Type ?u.370700
β : Type ?u.370703
γ : Type ?u.370706
δ : Type u_1
δ' : Type ?u.370712
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : j = i
⊢ Measurable fun v => TProd.elim v hj
subst hji
no goals
case pos
α : Type ?u.370700
β : Type ?u.370703
γ : Type ?u.370706
δ : Type u_1
δ' : Type ?u.370712
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
is : List δ
j : δ
hj : j ∈ j :: is
⊢ Measurable fun v => TProd.elim v hj
simpa using measurable_fst
case neg
α : Type ?u.370700
β : Type ?u.370703
γ : Type ?u.370706
δ : Type u_1
δ' : Type ?u.370712
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v.snd (_ : j ∈ is)
case neg
α : Type ?u.370700
β : Type ?u.370703
γ : Type ?u.370706
δ : Type u_1
δ' : Type ?u.370712
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v hj
simp only [TProd.elim_of_ne _ hji]
case neg
α : Type ?u.370700
β : Type ?u.370703
γ : Type ?u.370706
δ : Type u_1
δ' : Type ?u.370712
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj✝ : j ∈ i :: is
hj : j = i ∨ j ∈ is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v.snd (_ : j ∈ is)
case neg
α : Type ?u.370700
β : Type ?u.370703
γ : Type ?u.370706
δ : Type u_1
δ' : Type ?u.370712
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v.snd (_ : j ∈ is)
rw [mem_cons] at hj
no goals
case neg
α : Type ?u.370700
β : Type ?u.370703
γ : Type ?u.370706
δ : Type u_1
δ' : Type ?u.370712
ι : Sort uι
s t u : Set α
π : δ → Type u_2
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj✝ : j ∈ i :: is
hj : j = i ∨ j ∈ is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v.snd (_ : j ∈ is)
exact (measurable_tProd_elim (hj.resolve_left hji)).comp measurable_snd