awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
μ : Measure α
f : α → β
hf : Measurable f
x : γ
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((((const γ μ : Kernel γ α) : (a : γ) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₃ h₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((map (const γ μ) f : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((const γ (Measure.map f μ) : Kernel γ β) : (a : γ) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply' _ hf _ hs, const_apply, const_apply, Measure.map_apply hf hs]

Premises used: ProbabilityTheory.Kernel.map_apply', MeasureTheory.Measure.map_apply, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
g : γ → α
hg : Measurable g
⊢ Eq (α := (a : γ) → Measure β) (⇑(κ.comap g hg) : (a : γ) → Measure β) ((⇑κ : (a : α) → Measure β) ∘ g)

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 γ
g : γ → α
κ : Kernel α β
hg : Measurable g
c : γ
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ.comap g hg : (a : γ) → Measure β) c : Measure β)
    ((κ : (a : α) → Measure β) (g c) : 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 γ
g : γ → α
κ : Kernel α β
hg : Measurable g
c : γ
s : Set β
⊢ Eq (α := ℝ≥0∞) ((((κ.comap g hg : (a : γ) → Measure β) c : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) (g c) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

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 γ
g : γ → α
hg : Measurable g
h :
  ∀ (a : γ) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((comap 0 g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        (((((0 : Kernel γ β) : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel γ β) (comap 0 g hg) 0

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
hg : Measurable g
a : γ
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((comap 0 g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel γ β) : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ.comap id ⋯ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ.comap id ⋯ = κ

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ.comap id ⋯ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ κ.comap (fun (a : α) ↦ a) ⋯ = κ

Tactic:
comap_id κ

Premises used: ProbabilityTheory.Kernel.comap_id
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
c : γ
g' : β → ℝ≥0∞
⊢ ∫⁻ (b : β), g' b ∂(κ.comap g hg : (a : γ) → Measure β) c = ∫⁻ (b : β), g' b ∂(κ : (a : α) → Measure β) (g c)

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 γ
g : γ → α
κ : Kernel α β
inst : IsSFiniteKernel κ
hg : Measurable g
h :
  ∀ (a : γ) (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((Kernel.sum fun (n : ℕ) ↦ (κ.seq n).comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
        ℝ≥0∞)
      ((((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (Kernel.sum fun (n : ℕ) ↦ (κ.seq n).comap g hg) = κ.comap g hg

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst : IsSFiniteKernel κ
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (∑' (i : ℕ), ((((κ.seq i).comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
    (∑' (i : ℕ), (((κ.seq i : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (n : ℕ) ↦ (κ.seq n).comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Kernel.sum_apply, comap_apply' κ hg a s, Measure.sum_apply _ hs, ← measure_sum_seq κ,
    Measure.sum_apply _ hs]

Premises used: MeasureTheory.Measure.sum_apply, ProbabilityTheory.Kernel.sum_apply, ProbabilityTheory.Kernel.measure_sum_seq, ProbabilityTheory.Kernel.comap_apply'
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst : IsSFiniteKernel κ
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), ((((κ.seq i).comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
    (∑' (i : ℕ), (((κ.seq i : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) s)

Tactic:
simp_rw [comap_apply' _ hg _ s]

Premises used: ProbabilityTheory.Kernel.comap_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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsMarkovKernel κ
hg : Measurable g
a : γ
rw : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞) ((((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
rw [comap_apply' κ hg a Set.univ, measure_univ]

Premises used: Set.univ, MeasureTheory.IsProbabilityMeasure.measure_univ, ProbabilityTheory.Kernel.comap_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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
hg : Measurable g
inl :
  ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    IsZeroOrMarkovKernel.{u_4, u_2} (β := β) (mβ := mβ) (Kernel.comap 0 g hg)
inr : ∀ (h : IsMarkovKernel κ), IsZeroOrMarkovKernel (κ.comap g hg)
⊢ IsZeroOrMarkovKernel (κ.comap g hg)

Tactic:
rcases eq_zero_or_isMarkovKernel κ with rfl | h

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- 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 δ
f : β → γ
g : γ → α
hg : Measurable g
inst : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
⊢ IsZeroOrMarkovKernel.{u_4, u_2} (α := γ) (β := β) (mα := mγ) (mβ := mβ) 0

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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
hg : Measurable g
h : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap g hg)

Tactic:
have := IsMarkovKernel.comap κ hg
-- 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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
hg : Measurable g
h : IsMarkovKernel κ
this : IsMarkovKernel (κ.comap g hg)
⊢ IsZeroOrMarkovKernel (κ.comap g hg)

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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsFiniteKernel κ
hg : Measurable g
⊢ IsFiniteKernel (κ.comap g hg)

Tactic:
⟨⟨κ.bound, κ.bound_lt_top, fun a => ?_⟩⟩

Premises used: ProbabilityTheory.IsFiniteKernel.mk, ProbabilityTheory.Kernel.bound_lt_top, And.intro, Exists.intro, ProbabilityTheory.Kernel.bound
-- 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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsFiniteKernel κ
hg : Measurable g
refine : ∀ (a : γ), (((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound
⊢ IsFiniteKernel (κ.comap g hg)

Tactic:
refine ⟨⟨κ.bound, κ.bound_lt_top, fun a => ?_⟩⟩
-- 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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsFiniteKernel κ
hg : Measurable g
a : γ
rw : (((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound
⊢ (((κ.comap g hg : (a : γ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound

Tactic:
rw [comap_apply' κ hg a Set.univ]

Premises used: Set.univ, ProbabilityTheory.Kernel.comap_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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsFiniteKernel κ
hg : Measurable g
a : γ
⊢ (((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound

Tactic:
measure_le_bound κ _ _

Premises used: ProbabilityTheory.Kernel.measure_le_bound
-- 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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsFiniteKernel κ
hg : Measurable g
a : γ
⊢ (((κ : (a : α) → Measure β) (g a) : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound

Tactic:
exact measure_le_bound κ _ _

Premises used: ProbabilityTheory.Kernel.measure_le_bound
-- 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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst : IsSFiniteKernel κ
hg : Measurable g
⊢ IsSFiniteKernel (κ.comap g hg)

Tactic:
⟨⟨fun n => Kernel.comap (seq κ n) g hg, inferInstance, (sum_comap_seq κ hg).symm⟩⟩

Premises used: ProbabilityTheory.IsSFiniteKernel.mk, ProbabilityTheory.Kernel.comap, ProbabilityTheory.Kernel.sum_comap_seq, inferInstance, ProbabilityTheory.Kernel.seq, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
g : γ → α
κ : Kernel α β
f : δ → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ (a : δ) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ.comap (g ∘ f) ⋯ : (a : δ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        (((((κ.comap g hg).comap f hf : (a : δ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ.comap (g ∘ f) ⋯ = (κ.comap g hg).comap f hf

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
g : γ → α
κ : Kernel α β
f : δ → γ
hf : Measurable f
hg : Measurable g
a : δ
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ.comap (g ∘ f) ⋯ : (a : δ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((κ.comap g hg).comap f hf : (a : δ) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
h :
  ∀ (x : α) (s : Set δ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        (((((comap (κ.map g) f hf : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
        ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel α δ) (comap (κ.map g) f hf) ((κ.comap f hf).map g)

Tactic:
ext x s _
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((((κ.map g : Kernel β δ) : (a : β) → Measure δ) (f x) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((Measure.map g ((κ : (a : β) → Measure γ) (f x)) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) (((Measure.map g ((κ : (a : β) → Measure γ) (f x)) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map g ((κ.comap f hf : (a : α) → Measure γ) x) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
h₃ h₄ :
  Eq (α := ℝ≥0∞) (((Measure.map g ((κ : (a : β) → Measure γ) (f x)) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map g ((κ : (a : β) → Measure γ) (f x)) : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((comap (κ.map g) f hf : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((((κ.comap f hf).map g : Kernel α δ) : (a : α) → Measure δ) x : Measure δ) : (a : Set δ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [comap_apply, map_apply _ hg, map_apply _ hg, comap_apply]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.comap_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
h :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        (((((map Kernel.id f : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ map Kernel.id f = deterministic f hf

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.map f ((Kernel.id : (a : α) → Measure α) a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((Measure.map f ((Kernel.id : (a : α) → Measure α) a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) (((Measure.map f (Measure.dirac a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₃ h₄ :
  Eq (α := ℝ≥0∞) (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((map Kernel.id f : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Kernel.map_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply, Measure.map_dirac' hf]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.deterministic_apply, MeasureTheory.Measure.map_dirac', ProbabilityTheory.Kernel.id_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
h :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((comap Kernel.id f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ comap Kernel.id f hf = deterministic f hf

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((Kernel.id : (a : β) → Measure β) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((((Kernel.id : (a : β) → Measure β) (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₂ h₃ :
  Eq (α := ℝ≥0∞) (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.dirac (f a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((comap Kernel.id f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((deterministic f hf : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Kernel.comap_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply]

Premises used: ProbabilityTheory.Kernel.deterministic_apply, ProbabilityTheory.Kernel.id_apply, ProbabilityTheory.Kernel.comap_apply
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
g : β → γ
hg : Measurable g
rw : map (mβ := mβ) (map Kernel.id f) g = deterministic (g ∘ f) ⋯
rw₁ : map Kernel.id (g ∘ f) = deterministic (g ∘ f) ⋯
rw₂ : deterministic (g ∘ f) ⋯ = deterministic (g ∘ f) ⋯
rw₃ : Measurable (g ∘ f)
rw₄ : deterministic (g ∘ f) ⋯ = deterministic (g ∘ f) ⋯
rw₅ : Measurable (g ∘ f)
⊢ (deterministic f hf).map g = deterministic (g ∘ f) ⋯

Tactic:
rw [← id_map, ← map_comp_right _ hf hg, id_map]

Premises used: ProbabilityTheory.Kernel.map_comp_right, ProbabilityTheory.Kernel.id_map
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
ca : γ × α
⊢ Eq.{u_2 + 1} (α := Measure β) ((prodMkLeft γ κ : (a : γ × α) → Measure β) ca : Measure β)
    ((κ : (a : α) → Measure β) ca.2 : 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 α β
ca : α × γ
⊢ Eq.{u_2 + 1} (α := Measure β) ((prodMkRight γ κ : (a : α × γ) → Measure β) ca : Measure β)
    ((κ : (a : α) → Measure β) ca.1 : 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 α β
ca : γ × α
s : Set β
⊢ Eq (α := ℝ≥0∞) ((((prodMkLeft γ κ : (a : γ × α) → Measure β) ca : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) ca.2 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

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 α β
ca : α × γ
s : Set β
⊢ Eq (α := ℝ≥0∞) ((((prodMkRight γ κ : (a : α × γ) → Measure β) ca : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) ca.1 : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

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 γ
h :
  ∀ (x : α × β) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((prodMkLeft α 0 : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        ((((0 : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel (α × β) γ) (prodMkLeft α 0) 0

Tactic:
ext x s _
-- Module: Mathlib.Probability.Kernel.Composition.MapComap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α × β
s : Set γ
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((prodMkLeft α 0 : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((0 : (a : α × β) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥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 γ
h :
  ∀ (x : β × α) (s : Set γ),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((prodMkRight α 0 : (a : β × α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        ((((0 : (a : β × α) → Measure γ) x : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel (β × α) γ) (prodMkRight α 0) 0

Tactic:
ext x s _