awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
g : γ × β → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (c : γ × β), g c ∂(κ.map Prod.swap : (a : α) → Measure (γ × β)) a =
    ∫⁻ (bc : β × γ), g bc.swap ∂(κ : (a : α) → Measure (β × γ)) a
rw₁ rw₂ :
  ∫⁻ (a : β × γ), g a.swap ∂(κ : (a : α) → Measure (β × γ)) a =
    ∫⁻ (bc : β × γ), g bc.swap ∂(κ : (a : α) → Measure (β × γ)) a
⊢ ∫⁻ (c : γ × β), g c ∂(κ.swapRight : (a : α) → Measure (γ × β)) a =
    ∫⁻ (bc : β × γ), g bc.swap ∂(κ : (a : α) → Measure (β × γ)) a

Tactic:
rw [swapRight_eq, lintegral_map _ measurable_swap a hg]

Premises used: ProbabilityTheory.Kernel.lintegral_map, ProbabilityTheory.Kernel.swapRight_eq, measurable_swap
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsMarkovKernel κ
rw : IsMarkovKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)
⊢ IsMarkovKernel κ.swapRight

Tactic:
rw [Kernel.swapRight_eq]

Premises used: ProbabilityTheory.Kernel.swapRight_eq
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsMarkovKernel κ
⊢ IsMarkovKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)

Tactic:
IsMarkovKernel.map _ measurable_swap

Premises used: measurable_swap, ProbabilityTheory.Kernel.IsMarkovKernel.map
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsMarkovKernel κ
⊢ IsMarkovKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)

Tactic:
exact IsMarkovKernel.map _ measurable_swap

Premises used: measurable_swap, ProbabilityTheory.Kernel.IsMarkovKernel.map
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsZeroOrMarkovKernel κ
rw : IsZeroOrMarkovKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)
⊢ IsZeroOrMarkovKernel κ.swapRight

Tactic:
rw [Kernel.swapRight_eq]

Premises used: ProbabilityTheory.Kernel.swapRight_eq
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsFiniteKernel κ
rw : IsFiniteKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)
⊢ IsFiniteKernel κ.swapRight

Tactic:
rw [Kernel.swapRight_eq]

Premises used: ProbabilityTheory.Kernel.swapRight_eq
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsFiniteKernel κ
⊢ IsFiniteKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsSFiniteKernel κ
rw : IsSFiniteKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)
⊢ IsSFiniteKernel κ.swapRight

Tactic:
rw [Kernel.swapRight_eq]

Premises used: ProbabilityTheory.Kernel.swapRight_eq
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsSFiniteKernel κ
⊢ IsSFiniteKernel (mβ := Prod.instMeasurableSpace) (κ.map Prod.swap)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
⊢ κ.fst = κ.map Prod.fst

Tactic:
simp [fst]

Premises used: ProbabilityTheory.Kernel.fst
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ.fst : (a : α) → Measure β) a : Measure β)
    (Measure.map (α := β × γ) Prod.fst ((κ : (a : α) → Measure (β × γ)) a) : Measure β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.1 ∈ s} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.1 ∈ s} : ℝ≥0∞)

Tactic:
rw [fst_apply, Measure.map_apply measurable_fst hs]

Premises used: MeasureTheory.Measure.map_apply, ProbabilityTheory.Kernel.fst_apply, measurable_fst
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.1 ∈ s} : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ Measure.real (m := mβ) ((κ.fst : (a : α) → Measure β) a) s =
    Measure.real (α := β × γ) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × γ)) a) {p : β × γ | p.1 ∈ s}

Tactic:
simp [fst_apply', hs, measureReal_def]

Premises used: ProbabilityTheory.Kernel.fst_apply', MeasureTheory.measureReal_def
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Eq (α := Kernel α β) (fst.{u_1, u_2, u_3} (γ := γ) (mγ := mγ) 0) 0

Tactic:
simp [fst]

Premises used: ProbabilityTheory.Kernel.fst
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
g : β → ℝ≥0∞
hg : Measurable g
rw :
  ∫⁻ (c : β), g c ∂((κ.map Prod.fst : Kernel α β) : (a : α) → Measure β) a =
    ∫⁻ (bc : β × γ), g bc.1 ∂(κ : (a : α) → Measure (β × γ)) a
rw₁ rw₂ :
  ∫⁻ (a : β × γ), g a.1 ∂(κ : (a : α) → Measure (β × γ)) a = ∫⁻ (bc : β × γ), g bc.1 ∂(κ : (a : α) → Measure (β × γ)) a
⊢ ∫⁻ (c : β), g c ∂(κ.fst : (a : α) → Measure β) a = ∫⁻ (bc : β × γ), g bc.1 ∂(κ : (a : α) → Measure (β × γ)) a

Tactic:
rw [fst_eq, lintegral_map _ measurable_fst a hg]

Premises used: ProbabilityTheory.Kernel.lintegral_map, ProbabilityTheory.Kernel.fst_eq, measurable_fst
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsMarkovKernel κ
rw : IsMarkovKernel (mβ := mβ) (κ.map Prod.fst)
⊢ IsMarkovKernel κ.fst

Tactic:
rw [Kernel.fst_eq]

Premises used: ProbabilityTheory.Kernel.fst_eq
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsMarkovKernel κ
⊢ IsMarkovKernel (mβ := mβ) (κ.map Prod.fst)

Tactic:
IsMarkovKernel.map _ measurable_fst

Premises used: ProbabilityTheory.Kernel.IsMarkovKernel.map, measurable_fst
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsMarkovKernel κ
⊢ IsMarkovKernel (mβ := mβ) (κ.map Prod.fst)

Tactic:
exact IsMarkovKernel.map _ measurable_fst

Premises used: ProbabilityTheory.Kernel.IsMarkovKernel.map, measurable_fst
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsZeroOrMarkovKernel κ
rw : IsZeroOrMarkovKernel (mβ := mβ) (κ.map Prod.fst)
⊢ IsZeroOrMarkovKernel κ.fst

Tactic:
rw [Kernel.fst_eq]

Premises used: ProbabilityTheory.Kernel.fst_eq
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (mβ := mβ) (κ.map Prod.fst)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsFiniteKernel κ
rw : IsFiniteKernel (mβ := mβ) (κ.map Prod.fst)
⊢ IsFiniteKernel κ.fst

Tactic:
rw [Kernel.fst_eq]

Premises used: ProbabilityTheory.Kernel.fst_eq
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsFiniteKernel κ
⊢ IsFiniteKernel (mβ := mβ) (κ.map Prod.fst)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsSFiniteKernel κ
rw : IsSFiniteKernel (mβ := mβ) (κ.map Prod.fst)
⊢ IsSFiniteKernel κ.fst

Tactic:
rw [Kernel.fst_eq]

Premises used: ProbabilityTheory.Kernel.fst_eq
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
inst : IsSFiniteKernel κ
⊢ IsSFiniteKernel (mβ := mβ) (κ.map Prod.fst)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
h : IsFiniteKernel κ.fst
⊢ IsFiniteKernel κ

Tactic:
⟨(fst κ).bound, (fst κ).bound_lt_top,
    fun a ↦ le_trans ?_ (measure_le_bound (fst κ) a Set.univ)⟩

Premises used: Set.univ, ProbabilityTheory.IsFiniteKernel.mk, ProbabilityTheory.Kernel.bound_lt_top, And.intro, ProbabilityTheory.Kernel.measure_le_bound, Exists.intro, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.bound, le_trans
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
h : IsFiniteKernel κ.fst
refine :
  ∀ (a : α),
    LE.le (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ IsFiniteKernel κ

Tactic:
refine ⟨(fst κ).bound, (fst κ).bound_lt_top,
    fun a ↦ le_trans ?_ (measure_le_bound (fst κ) a Set.univ)⟩
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
h : IsFiniteKernel κ.fst
a : α
rw :
  LE.le (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        {p : β × γ | Membership.mem (γ := Set β) Set.univ p.1} :
      ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
rw [fst_apply' _ _ MeasurableSet.univ]

Premises used: ProbabilityTheory.Kernel.fst_apply', MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α (β × γ)
h : IsFiniteKernel κ.fst
a : α
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        {p : β × γ | Membership.mem (γ := Set β) Set.univ p.1} :
      ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : 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
pos :
  ∀ (hf : Measurable f),
    Eq (α := Kernel α γ) (fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map f)
neg :
  ∀ (hf : ¬Measurable f),
    Eq (α := Kernel α γ) (fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map f)
⊢ Eq (α := Kernel α γ) (fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map f)

Tactic:
by_cases hf : Measurable f

Premises used: Measurable
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : 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
pos :
  ∀ (x : α) (s : Set γ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x)) : (a : α) → Measure γ) x :
              Measure γ) :
            (a : Set γ) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel α γ) (fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map f)

Tactic:
ext x s hs
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : 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
pos :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞)
        (Set.preimage (β := γ × δ) (fun (x : β) ↦ (f x, g x)) {p : γ × δ | p.1 ∈ s}) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
pos₁ : MeasurableSet (α := γ × δ) {p : γ × δ | p.1 ∈ s}
⊢ Eq (α := ℝ≥0∞)
    ((((fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x)) : (a : α) → Measure γ) x : Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((((κ.map f : Kernel α γ) : (a : α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

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

Premises used: ProbabilityTheory.Kernel.map_apply', ProbabilityTheory.Kernel.fst_apply', Measurable.prod
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : 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
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞)
        (Set.preimage (β := γ × δ) (fun (x : β) ↦ (f x, g x)) {p : γ × δ | p.1 ∈ s}) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)

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

Premises used: Set.mem_setOf, Set.preimage
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : 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:
measurable_fst hs

Premises used: Set.preimage, measurable_fst
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : 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

Premises used: measurable_fst
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : 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
contrapose : ∀ (hf : Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)), Measurable f
⊢ ¬Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)

Tactic:
contrapose hf
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : 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:
hf.fst

Premises used: Measurable.fst
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : 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

Premises used: Measurable.fst
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : 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:
have : ¬ Measurable (fun x ↦ (f x, g x)) := by
      contrapose hf; exact hf.fst
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : 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)
⊢ Eq (α := Kernel α γ) (fst.{u_1, u_3, u_4} (γ := δ) (mγ := mδ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map f)

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

Premises used: ProbabilityTheory.Kernel.map_of_not_measurable
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
f : β → γ
hf : Measurable f
rw : (κ.map fun (a : β) ↦ a) = κ
rw₁ rw₂ : κ = κ
⊢ fst.{u_1, u_2, u_3} (γ := γ) (mγ := mγ) (κ.map fun (a : β) ↦ (a, f a)) = κ

Tactic:
rw [fst_map_prod _ hf, Kernel.map_id']

Premises used: ProbabilityTheory.Kernel.map_id', ProbabilityTheory.Kernel.fst_map_prod
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_5
inst : MeasurableSpace δ
κ : Kernel α (β × γ)
⊢ Eq (α := Kernel (δ × α) β) (fst (prodMkLeft δ κ)) (prodMkLeft δ κ.fst)

Tactic:
rfl

Premises used: ProbabilityTheory.Kernel.comap, rfl, ProbabilityTheory.Kernel.prodMkLeft
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
δ : Type u_5
inst : MeasurableSpace δ
⊢ Eq (α := Kernel (α × δ) β) (fst (prodMkRight δ κ)) (prodMkRight δ κ.fst)

Tactic:
rfl

Premises used: ProbabilityTheory.Kernel.comap, ProbabilityTheory.Kernel.prodMkRight, rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
⊢ κ.snd = κ.map Prod.snd

Tactic:
simp [snd]

Premises used: ProbabilityTheory.Kernel.snd
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
⊢ Eq.{u_3 + 1} (α := Measure γ) ((κ.snd : (a : α) → Measure γ) a : Measure γ)
    (Measure.map (α := β × γ) Prod.snd ((κ : (a : α) → Measure (β × γ)) a) : Measure γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞)
    (((Measure.map (α := β × γ) Prod.snd ((κ : (a : α) → Measure (β × γ)) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.snd : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [snd_apply, Measure.map_apply measurable_snd hs]

Premises used: MeasureTheory.Measure.map_apply, ProbabilityTheory.Kernel.snd_apply, measurable_snd
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ Eq (α := Kernel α γ) (snd.{u_1, u_2, u_3} (β := β) (mβ := mβ) 0) 0

Tactic:
simp [snd]

Premises used: ProbabilityTheory.Kernel.snd