-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma fst_map_prod (κ : Kernel α β) {f : β → γ} {g : β → δ} (hg : Measurable g) :
    fst (map κ (fun x ↦ (f x, g x))) = map κ f

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
⊢ (κ.map fun x => (f x, g x)).fst = κ.map f

Tactic:
ext x s hs

Result:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ ((κ.map fun x => (f x, g x)).fst x) s = ((κ.map f) x) s

Proof state:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ ((κ.map fun x => (f x, g x)).fst x) s = ((κ.map f) x) s

Tactic:
rw [fst_apply' _ _ hs, map_apply' _ (hf.prod hg) _, map_apply' _ hf _ hs]

Result:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ (κ x) ((fun x => (f x, g x)) ⁻¹' {p | p.1 ∈ s}) = (κ x) (f ⁻¹' s)

case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : ¬Measurable f
⊢ (κ.map fun x => (f x, g x)).fst = κ.map f

Tactic:
have : ¬ Measurable (fun x ↦ (f x, g x)) := by
  contrapose! hf; exact hf.fst

Result:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : ¬Measurable f
this : ¬Measurable fun x => (f x, g x)
⊢ (κ.map fun x => (f x, g x)).fst = κ.map f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable fun x => (f x, g x)
⊢ Measurable f

Tactic:
exact hf.fst

Result:
no goals

Proof state:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ (κ x) ((fun x => (f x, g x)) ⁻¹' {p | p.1 ∈ s}) = (κ x) (f ⁻¹' s)

Tactic:
simp only [Set.preimage, Set.mem_setOf]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : ¬Measurable f
this : ¬Measurable fun x => (f x, g x)
⊢ (κ.map fun x => (f x, g x)).fst = κ.map f

Tactic:
simp [map_of_not_measurable _ hf, map_of_not_measurable _ this]

Result:
no goals

Proof state:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
x : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}

Tactic:
exact measurable_fst hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : ¬Measurable f
⊢ ¬Measurable fun x => (f x, g x)

Tactic:
contrapose! hf

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable fun x => (f x, g x)
⊢ Measurable f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
⊢ (κ.map fun x => (f x, g x)).fst = κ.map f

Tactic:
by_cases hf : Measurable f

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : Measurable f
⊢ (κ.map fun x => (f x, g x)).fst = κ.map f

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hg : Measurable g
hf : ¬Measurable f
⊢ (κ.map fun x => (f x, g x)).fst = κ.map f