ProbabilityTheory.Kernel.deleteMiddle_map_prod

@[simp, nolint simpNF]lemma deleteMiddle_map_prod (κ : Kernel α β) {f : β → γ} {g : β → δ} {g' : β → ε}    (hg : Measurable g) :    deleteMiddle (map κ (fun b ↦ (f b, g b, g' b)))      = map κ (fun b ↦ (f b, g' b)) := by  by_cases hfg' : Measurable (fun b ↦ (f b, g' b))  · have : Measurable f := hfg'.fst    have : Measurable g' := hfg'.snd    rw [deleteMiddle_eq, map_map _ (by fun_prop) (by fun_prop)]    rfl  · have : ¬ (Measurable (fun b ↦ (f b, g b, g' b))) := by      contrapose! hfg'      have T : Measurable g' := hfg'.snd.snd      have U : Measurable f := hfg'.fst      exact U.prod T    simp [map_of_not_measurable _ hfg', map_of_not_measurable _ this]