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.snd : Kernel α γ) : (a : α) → Measure γ) a =
    ∫⁻ (bc : β × γ), g bc.2 ∂(κ : (a : α) → Measure (β × γ)) a
rw₁ rw₂ :
  ∫⁻ (a : β × γ), g a.2 ∂(κ : (a : α) → Measure (β × γ)) a = ∫⁻ (bc : β × γ), g bc.2 ∂(κ : (a : α) → Measure (β × γ)) a
⊢ ∫⁻ (c : γ), g c ∂(κ.snd : (a : α) → Measure γ) a = ∫⁻ (bc : β × γ), g bc.2 ∂(κ : (a : α) → Measure (β × γ)) a

Tactic:
rw [snd_eq, lintegral_map _ measurable_snd a hg]

Premises used: ProbabilityTheory.Kernel.lintegral_map, ProbabilityTheory.Kernel.snd_eq, measurable_snd
-- 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.snd)
⊢ IsMarkovKernel κ.snd

Tactic:
rw [Kernel.snd_eq]

Premises used: ProbabilityTheory.Kernel.snd_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.snd)

Tactic:
IsMarkovKernel.map _ measurable_snd

Premises used: measurable_snd, 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β := mγ) (κ.map Prod.snd)

Tactic:
exact IsMarkovKernel.map _ measurable_snd

Premises used: measurable_snd, 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β := mγ) (κ.map Prod.snd)
⊢ IsZeroOrMarkovKernel κ.snd

Tactic:
rw [Kernel.snd_eq]

Premises used: ProbabilityTheory.Kernel.snd_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.snd)

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.snd)
⊢ IsFiniteKernel κ.snd

Tactic:
rw [Kernel.snd_eq]

Premises used: ProbabilityTheory.Kernel.snd_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.snd)

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.snd)
⊢ IsSFiniteKernel κ.snd

Tactic:
rw [Kernel.snd_eq]

Premises used: ProbabilityTheory.Kernel.snd_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.snd)

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 κ.snd
⊢ IsFiniteKernel κ

Tactic:
⟨(snd κ).bound, (snd κ).bound_lt_top,
    fun a ↦ le_trans ?_ (measure_le_bound (snd κ) 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.snd, 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 κ.snd
refine :
  ∀ (a : α),
    LE.le (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      ((((κ.snd : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ IsFiniteKernel κ

Tactic:
refine ⟨(snd κ).bound, (snd κ).bound_lt_top,
    fun a ↦ le_trans ?_ (measure_le_bound (snd κ) 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 κ.snd
a : α
rw :
  LE.le (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' Set.univ) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ.snd : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)

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

Premises used: ProbabilityTheory.Kernel.snd_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 κ.snd
a : α
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' Set.univ) : ℝ≥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 : β → δ
hf : Measurable f
pos :
  ∀ (hg : Measurable g),
    Eq (α := Kernel α δ) (snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map g)
neg :
  ∀ (hg : ¬Measurable g),
    Eq (α := Kernel α δ) (snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map g)
⊢ Eq (α := Kernel α δ) (snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map g)

Tactic:
by_cases hg : Measurable g

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

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 : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞)
        (Set.preimage (β := γ × δ) (fun (x : β) ↦ (f x, g x)) (Prod.snd ⁻¹' s)) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
pos₁ : MeasurableSet (α := γ × δ) (Prod.snd ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    ((((snd.{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 g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)

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

Premises used: ProbabilityTheory.Kernel.map_apply', ProbabilityTheory.Kernel.snd_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 : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞)
        (Set.preimage (β := γ × δ) (fun (x : β) ↦ (f x, g x)) (Prod.snd ⁻¹' s)) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) (g ⁻¹' 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 : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ MeasurableSet (α := γ × δ) (Prod.snd ⁻¹' s)

Tactic:
measurable_snd hs

Premises used: measurable_snd
-- 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 : β → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
hs : MeasurableSet s
⊢ MeasurableSet (α := γ × δ) (Prod.snd ⁻¹' s)

Tactic:
exact measurable_snd hs

Premises used: measurable_snd
-- 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 : β → δ
hf : Measurable f
hg : ¬Measurable g
contrapose : ∀ (hg : Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)), Measurable g
⊢ ¬Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)

Tactic:
contrapose hg
-- 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 : β → δ
hf : Measurable f
hg : Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)
⊢ Measurable g

Tactic:
hg.snd

Premises used: Measurable.snd
-- 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 : β → δ
hf : Measurable f
hg : Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)
⊢ Measurable g

Tactic:
exact hg.snd

Premises used: Measurable.snd
-- 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 : β → δ
hf : Measurable f
hg : ¬Measurable g
⊢ ¬Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)

Tactic:
have : ¬ Measurable (fun x ↦ (f x, g x)) := by
      contrapose hg; exact hg.snd
-- 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 : β → δ
hf : Measurable f
hg : ¬Measurable g
this : ¬Measurable (β := γ × δ) fun (x : β) ↦ (f x, g x)
⊢ Eq (α := Kernel α δ) (snd.{u_1, u_3, u_4} (β := γ) (mβ := mγ) (κ.map fun (x : β) ↦ (f x, g x))) (κ.map g)

Tactic:
simp [map_of_not_measurable _ hg, 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₂ : κ = κ
⊢ snd.{u_1, u_3, u_2} (β := γ) (mβ := mγ) (κ.map fun (a : β) ↦ (f a, a)) = κ

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

Premises used: ProbabilityTheory.Kernel.map_id', ProbabilityTheory.Kernel.snd_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 (δ × α) γ) (snd (prodMkLeft δ κ)) (prodMkLeft δ κ.snd)

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 (α × δ) γ) (snd (prodMkRight δ κ)) (prodMkRight δ κ.snd)

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 α (β × γ)
h :
  ∀ (a : α) (s : Set γ) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ.swapRight.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ.snd : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ.swapRight.fst = κ.snd

Tactic:
ext a s hs
-- 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
h :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        {p : β × γ | Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ s} p.swap} :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
h₁ : MeasurableSet (α := γ × β) {p : γ × β | p.1 ∈ s}
⊢ Eq (α := ℝ≥0∞) ((((κ.swapRight.fst : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.snd : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [fst_apply' _ _ hs, swapRight_apply', snd_apply' _ _ hs]

Premises used: ProbabilityTheory.Kernel.swapRight_apply', ProbabilityTheory.Kernel.fst_apply', ProbabilityTheory.Kernel.snd_apply'
-- 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∞)
        {p : β × γ | Membership.mem (γ := Set (γ × β)) {p : γ × β | p.1 ∈ s} p.swap} :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' 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
⊢ 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 γ
κ : Kernel α (β × γ)
a : α
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 γ
κ : Kernel α (β × γ)
h :
  ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ.swapRight.snd : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ.swapRight.snd = κ.fst

Tactic:
ext a s hs
-- 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
h :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        {p : β × γ | Membership.mem (γ := Set (γ × β)) (Prod.snd ⁻¹' s) p.swap} :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) {p : β × γ | p.1 ∈ s} : ℝ≥0∞)
h₁ : MeasurableSet (α := γ × β) (Prod.snd ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) ((((κ.swapRight.snd : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [snd_apply' _ _ hs, swapRight_apply', fst_apply' _ _ hs]

Premises used: ProbabilityTheory.Kernel.swapRight_apply', ProbabilityTheory.Kernel.fst_apply', ProbabilityTheory.Kernel.snd_apply'
-- 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∞)
        {p : β × γ | Membership.mem (γ := Set (γ × β)) (Prod.snd ⁻¹' s) p.swap} :
      ℝ≥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
⊢ MeasurableSet (α := γ × β) (Prod.snd ⁻¹' s)

Tactic:
measurable_snd hs

Premises used: measurable_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 : α
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (α := γ × β) (Prod.snd ⁻¹' s)

Tactic:
exact measurable_snd hs

Premises used: measurable_snd
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
b : β
a : α
⊢ Eq.{u_4 + 1} (α := Measure γ) ((κ.sectL b : (a : α) → Measure γ) a : Measure γ)
    ((κ : (a : α × β) → Measure γ) (a, b) : Measure γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
b : β
⊢ Eq (α := Kernel α γ) (sectL (mβ := mβ) 0 b) 0

Tactic:
simp [sectL]

Premises used: ProbabilityTheory.Kernel.sectL
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
inst : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap (fun (a : α) ↦ (a, b)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
inst : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap (fun (a : α) ↦ (a, b)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
inst : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap (fun (a : α) ↦ (a, b)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
inst : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap (fun (a : α) ↦ (a, b)) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
b : β
inst rw : NeZero.{u_4} (R := Measure γ) ((κ : (a : α × β) → Measure γ) (a, b) : Measure γ)
⊢ NeZero.{u_4} (R := Measure γ) ((κ.sectL b : (a : α) → Measure γ) a : Measure γ)

Tactic:
rw [sectL_apply]

Premises used: ProbabilityTheory.Kernel.sectL_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
b : β
inst : NeZero.{u_4} (R := Measure γ) ((κ : (a : α × β) → Measure γ) (a, b) : Measure γ)
⊢ NeZero.{u_4} (R := Measure γ) ((κ : (a : α × β) → Measure γ) (a, b) : Measure γ)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst : ∀ (b : β), IsMarkovKernel (κ.sectL b)
⊢ IsMarkovKernel κ

Tactic:
⟨fun _ ↦ ⟨?_⟩⟩

Premises used: MeasureTheory.IsProbabilityMeasure.mk, ProbabilityTheory.IsMarkovKernel.mk
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ_1 : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ_1 : MeasurableSpace γ_1
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
inst : ∀ (b : β), IsMarkovKernel (κ.sectL b)
refine :
  ∀ (x : α × β),
    Eq (α := ℝ≥0∞) ((((κ : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ IsMarkovKernel κ

Tactic:
refine ⟨fun _ ↦ ⟨?_⟩⟩