awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
β : Type u_4
inst : MeasurableSpace β
μ ν : Measure α
a : β
s : Set α
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((((const β (μ + ν) : Kernel β α) : (a : β) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((((HAdd.hAdd (α := Kernel β α) (const β μ) (const β ν) : (a : β) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
μ : ι → Measure β
⊢ Eq (α := Kernel α β) (Kernel.sum fun (n : ι) ↦ const α (μ n)) (const α (Measure.sum μ))

Tactic:
rfl

Premises used: ProbabilityTheory.Kernel.sum, ProbabilityTheory.Kernel.const, rfl
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μβ : Measure β
inst : IsFiniteMeasure μβ
⊢ IsFiniteKernel (mα := mα) (const α μβ)

Tactic:
⟨⟨μβ Set.univ, measure_lt_top _ _, fun _ => le_rfl⟩⟩

Premises used: le_rfl, MeasureTheory.measure_lt_top, Set.univ, ProbabilityTheory.IsFiniteKernel.mk, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μβ : Measure β
inst : SFinite μβ
rw : Eq (α := Kernel α β) (const α μβ) (const α (Measure.sum (sfiniteSeq μβ)))
rw₁ rw₂ : Eq (α := Kernel α β) (const α μβ) (const α μβ)
⊢ Eq (α := Kernel α β) (const α μβ) (Kernel.sum fun (n : ℕ) ↦ const α (sfiniteSeq μβ n))

Tactic:
rw [sum_const, sum_sfiniteSeq]

Premises used: ProbabilityTheory.Kernel.sum_const, MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μβ : Measure β
hμβ : IsProbabilityMeasure μβ
⊢ IsMarkovKernel (mα := mα) (const α μβ)

Tactic:
⟨fun _ => hμβ⟩

Premises used: ProbabilityTheory.IsMarkovKernel.mk
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μβ : Measure β
hμβ : IsZeroOrProbabilityMeasure μβ
inl :
  ∀ [hμβ : IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) 0],
    IsZeroOrMarkovKernel.{u_1, u_2} (β := β) (mα := mα) (mβ := mβ) (const α 0)
inr : ∀ (h : IsProbabilityMeasure μβ), IsZeroOrMarkovKernel (mα := mα) (const α μβ)
⊢ IsZeroOrMarkovKernel (mα := mα) (const α μβ)

Tactic:
rcases eq_zero_or_isProbabilityMeasure μβ with rfl | h

Premises used: MeasureTheory.eq_zero_or_isProbabilityMeasure, rfl
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
hμβ : IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) 0
⊢ IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μβ : Measure β
hμβ : IsZeroOrProbabilityMeasure μβ
h : IsProbabilityMeasure μβ
⊢ IsZeroOrMarkovKernel (mα := mα) (const α μβ)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Nonempty α
μβ : Measure β
⊢ IsSFiniteKernel (mα := mα) (const α μβ) ↔ SFinite μβ

Tactic:
⟨fun h ↦ h.sFinite (Classical.arbitrary α), fun _ ↦ inferInstance⟩

Premises used: inferInstance, ProbabilityTheory.IsSFiniteKernel.sFinite, Iff.intro, Classical.arbitrary
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : Nonempty β
⊢ Nonempty { κ : Kernel α β // IsMarkovKernel κ }

Tactic:
nonempty_subtype.2 ⟨Kernel.const _ (Measure.dirac Classical.ofNonempty), inferInstance⟩

Premises used: Iff.mpr, Classical.ofNonempty, inferInstance, MeasureTheory.Measure.dirac, nonempty_subtype, Exists.intro, ProbabilityTheory.Kernel.const
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
μ : Measure β
a : α
rw rw₁ : ∫⁻ (x : β), f x ∂μ = ∫⁻ (x : β), f x ∂μ
⊢ ∫⁻ (x : β), f x ∂((const α μ : Kernel α β) : (a : α) → Measure β) a = ∫⁻ (x : β), f x ∂μ

Tactic:
rw [const_apply]

Premises used: ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
μ : Measure β
a : α
s : Set β
rw rw₁ : ∫⁻ (x : β) in s, f x ∂μ = ∫⁻ (x : β) in s, f x ∂μ
⊢ ∫⁻ (x : β) in s, f x ∂((const α μ : Kernel α β) : (a : α) → Measure β) a = ∫⁻ (x : β) in s, f x ∂μ

Tactic:
rw [const_apply]

Premises used: ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
⊢ Eq (α := Kernel α PUnit.{u_4 + 1}) (discard α) (const α (Measure.dirac PUnit.unit))

Tactic:
rfl

Premises used: ProbabilityTheory.Kernel.discard, ProbabilityTheory.Kernel.deterministic, ProbabilityTheory.Kernel.const, rfl
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t : Set β
κ : Kernel α β
hs : MeasurableSet s
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (a : α) ↦ Measure.restrict ((κ : (a : α) → Measure β) a) s

Tactic:
Measure.measurable_of_measurable_coe _ fun t ht => ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t : Set β
κ : Kernel α β
hs : MeasurableSet s
refine :
  ∀ (t : Set β) (ht : MeasurableSet t),
    Measurable (β := ℝ≥0∞) fun (b : α) ↦
      ((Measure.restrict ((κ : (a : α) → Measure β) b) s : Measure β) : (a : Set β) → ℝ≥0∞) t
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (a : α) ↦ Measure.restrict ((κ : (a : α) → Measure β) a) s

Tactic:
refine Measure.measurable_of_measurable_coe _ fun t ht => ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t_1 : Set β
κ : Kernel α β
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
simp_rw : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (((κ : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) (t ∩ s)
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.restrict ((κ : (a : α) → Measure β) b) s : Measure β) : (a : Set β) → ℝ≥0∞) t

Tactic:
simp_rw [Measure.restrict_apply ht]

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t_1 : Set β
κ : Kernel α β
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (((κ : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) (t ∩ s)

Tactic:
Kernel.measurable_coe κ (ht.inter hs)

Premises used: ProbabilityTheory.Kernel.measurable_coe, MeasurableSet.inter
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t_1 : Set β
κ : Kernel α β
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (((κ : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) (t ∩ s)

Tactic:
exact Kernel.measurable_coe κ (ht.inter hs)

Premises used: ProbabilityTheory.Kernel.measurable_coe, MeasurableSet.inter
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
κ : Kernel α β
hs : MeasurableSet s
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ.restrict (s := s) hs : (a : α) → Measure β) a : Measure β)
    (Measure.restrict ((κ : (a : α) → Measure β) a) s : Measure β)

Tactic:
rfl

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.OuterMeasure.toMeasure, MeasureTheory.Measure.ofMeasurable, rfl
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set β
κ : Kernel α β
hs : MeasurableSet s
a : α
ht : MeasurableSet t
rw :
  Eq (α := ℝ≥0∞) (((Measure.restrict ((κ : (a : α) → Measure β) a) s : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.restrict (s := s) hs : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
rw [restrict_apply κ hs a, Measure.restrict_apply ht]

Premises used: ProbabilityTheory.Kernel.restrict_apply, MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
μ : Measure β
hs : MeasurableSet s
h :
  ∀ (a : α) (s_1 : Set β),
    MeasurableSet s_1 →
      Eq (α := ℝ≥0∞)
        (((((Kernel.restrict (s := s) (const α μ) hs : Kernel α β) : (a : α) → Measure β) a : Measure β) :
              (a : Set β) → ℝ≥0∞)
            s_1 :
          ℝ≥0∞)
        (((((const α (μ.restrict s) : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s_1 :
          ℝ≥0∞)
⊢ Eq (α := Kernel α β) (Kernel.restrict (s := s) (const α μ) hs) (const α (μ.restrict s))

Tactic:
ext a
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
μ : Measure β
hs : MeasurableSet s
a : α
s_1 : Set β
h : MeasurableSet s_1
⊢ Eq (α := ℝ≥0∞)
    (((((Kernel.restrict (s := s) (const α μ) hs : Kernel α β) : (a : α) → Measure β) a : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s_1 :
      ℝ≥0∞)
    (((((const α (μ.restrict s) : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s_1 : ℝ≥0∞)

Tactic:
simp [Kernel.restrict_apply, Kernel.const_apply]

Premises used: ProbabilityTheory.Kernel.restrict_apply, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := Measure β) ((κ.restrict (s := Set.univ) ⋯ : (a : α) → Measure β) a : Measure β)
      ((κ : (a : α) → Measure β) a : Measure β)
⊢ κ.restrict (s := Set.univ) ⋯ = κ

Tactic:
ext1 a
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
h :
  Eq.{u_2 + 1} (α := Measure β) (Measure.restrict ((κ : (a : α) → Measure β) a) Set.univ) ((κ : (a : α) → Measure β) a)
h₁ h₂ :
  Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) ((κ : (a : α) → Measure β) a : Measure β)
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ.restrict (s := Set.univ) ⋯ : (a : α) → Measure β) a : Measure β)
    ((κ : (a : α) → Measure β) a : Measure β)

Tactic:
rw [Kernel.restrict_apply, Measure.restrict_univ]

Premises used: ProbabilityTheory.Kernel.restrict_apply, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
κ : Kernel α β
hs : MeasurableSet s
a : α
f : β → ℝ≥0∞
rw rw₁ : ∫⁻ (b : β) in s, f b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β) in s, f b ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (b : β), f b ∂(κ.restrict (s := s) hs : (a : α) → Measure β) a = ∫⁻ (b : β) in s, f b ∂(κ : (a : α) → Measure β) a

Tactic:
rw [restrict_apply]

Premises used: ProbabilityTheory.Kernel.restrict_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
κ : Kernel α β
hs : MeasurableSet s
a : α
f : β → ℝ≥0∞
t : Set β
rw :
  ∫⁻ (b : β) in t, f b ∂Measure.restrict ((κ : (a : α) → Measure β) a) s =
    ∫⁻ (b : β) in t ∩ s, f b ∂(κ : (a : α) → Measure β) a
rw₁ rw₂ : ∫⁻ (b : β) in t ∩ s, f b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β) in t ∩ s, f b ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (b : β) in t, f b ∂(κ.restrict (s := s) hs : (a : α) → Measure β) a =
    ∫⁻ (b : β) in t ∩ s, f b ∂(κ : (a : α) → Measure β) a

Tactic:
rw [restrict_apply, Measure.restrict_restrict' hs]

Premises used: ProbabilityTheory.Kernel.restrict_apply, MeasureTheory.Measure.restrict_restrict'
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t : Set β
κ : Kernel α β
inst : IsFiniteKernel κ
hs : MeasurableSet s
⊢ IsFiniteKernel (κ.restrict (s := s) hs)

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.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t : Set β
κ : Kernel α β
inst : IsFiniteKernel κ
hs : MeasurableSet s
refine :
  ∀ (a : α), (((κ.restrict (s := s) hs : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound
⊢ IsFiniteKernel (κ.restrict (s := s) hs)

Tactic:
refine ⟨⟨κ.bound, κ.bound_lt_top, fun a => ?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t : Set β
κ : Kernel α β
inst : IsFiniteKernel κ
hs : MeasurableSet s
a : α
rw : (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.univ ∩ s) ≤ κ.bound
⊢ (((κ.restrict (s := s) hs : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound

Tactic:
rw [restrict_apply' κ hs a MeasurableSet.univ]

Premises used: ProbabilityTheory.Kernel.restrict_apply', MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t : Set β
κ : Kernel α β
inst : IsFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.univ ∩ s) ≤ κ.bound

Tactic:
measure_le_bound κ a _

Premises used: ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t : Set β
κ : Kernel α β
inst : IsFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.univ ∩ s) ≤ κ.bound

Tactic:
exact measure_le_bound κ a _

Premises used: ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t : Set β
κ : Kernel α β
inst : IsSFiniteKernel κ
hs : MeasurableSet s
⊢ IsSFiniteKernel (κ.restrict (s := s) hs)

Tactic:
⟨⟨fun n => Kernel.restrict (seq κ n) hs, inferInstance, ?_⟩⟩

Premises used: ProbabilityTheory.IsSFiniteKernel.mk, ProbabilityTheory.Kernel.restrict, inferInstance, ProbabilityTheory.Kernel.seq, And.intro, Exists.intro
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t : Set β
κ : Kernel α β
inst : IsSFiniteKernel κ
hs : MeasurableSet s
refine : κ.restrict (s := s) hs = Kernel.sum fun (n : ℕ) ↦ (κ.seq n).restrict (s := s) hs
⊢ IsSFiniteKernel (κ.restrict (s := s) hs)

Tactic:
refine ⟨⟨fun n => Kernel.restrict (seq κ n) hs, inferInstance, ?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t : Set β
κ : Kernel α β
inst : IsSFiniteKernel κ
hs : MeasurableSet s
h :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := Measure β) ((κ.restrict (s := s) hs : (a : α) → Measure β) a : Measure β)
      ((Kernel.sum fun (n : ℕ) ↦ (κ.seq n).restrict (s := s) hs : (a : α) → Measure β) a : Measure β)
⊢ κ.restrict (s := s) hs = Kernel.sum fun (n : ℕ) ↦ (κ.seq n).restrict (s := s) hs

Tactic:
ext1 a
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
s t : Set β
κ : Kernel α β
inst : IsSFiniteKernel κ
hs : MeasurableSet s
a : α
h :
  Eq.{u_2 + 1} (α := Measure β) ((κ.restrict (s := s) hs : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ℕ) ↦ ((κ.seq n).restrict (s := s) hs : (a : α) → Measure β) a : Measure β)
h₁ :
  Eq (α := Measure β) (Measure.restrict ((κ : (a : α) → Measure β) a) s)
    (Measure.sum fun (n : ℕ) ↦ Measure.restrict ((κ.seq n : (a : α) → Measure β) a) s)
h₂ :
  Eq (α := Measure β) (Measure.restrict ((κ : (a : α) → Measure β) a) s)
    (Measure.restrict (Measure.sum fun (i : ℕ) ↦ (κ.seq i : (a : α) → Measure β) a) s)
h₃ :
  Eq (α := Measure β) (Measure.restrict ((κ : (a : α) → Measure β) a) s)
    (Measure.restrict ((Kernel.sum κ.seq : (a : α) → Measure β) a) s)
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ.restrict (s := s) hs : (a : α) → Measure β) a : Measure β)
    ((Kernel.sum fun (n : ℕ) ↦ (κ.seq n).restrict (s := s) hs : (a : α) → Measure β) a : Measure β)

Tactic:
simp_rw [sum_apply, restrict_apply, ← Measure.restrict_sum _ hs, ← sum_apply, kernel_sum_seq]

Premises used: ProbabilityTheory.Kernel.restrict_apply, MeasureTheory.Measure.restrict_sum, ProbabilityTheory.Kernel.kernel_sum_seq, ProbabilityTheory.Kernel.sum_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
⊢ Measurable.{u_1, u_4} (β := Measure γ) fun (a : α) ↦ Measure.comap f ((κ : (a : α) → Measure β) a)

Tactic:
Measure.measurable_measure.mpr fun t ht => ?_

Premises used: Iff.mpr, MeasureTheory.Measure.measurable_measure
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
refine :
  ∀ (t : Set γ) (ht : MeasurableSet t),
    Measurable (β := ℝ≥0∞) fun (b : α) ↦
      ((Measure.comap f ((κ : (a : α) → Measure β) b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t
⊢ Measurable.{u_1, u_4} (β := Measure γ) fun (a : α) ↦ Measure.comap f ((κ : (a : α) → Measure β) a)

Tactic:
refine Measure.measurable_measure.mpr fun t ht => ?_

Premises used: Iff.mpr, MeasureTheory.Measure.measurable_measure
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
h :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (((Measure.comap f ((κ : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ ((Measure.comap f ((κ : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t)

Tactic:
ext1 a
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
a : α
rw : ∀ (s : Set γ), MeasurableSet s → MeasurableSet (f '' s)
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f ((κ : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)

Tactic:
rw [Measure.comap_apply _ hf.injective _ _ ht]

Premises used: MeasureTheory.Measure.comap_apply, MeasurableEmbedding.injective
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
a : α
⊢ ∀ (s : Set γ), MeasurableSet s → MeasurableSet (f '' s)

Tactic:
fun s' hs' ↦ hf.measurableSet_image.mpr hs'

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
a : α
⊢ ∀ (s : Set γ), MeasurableSet s → MeasurableSet (f '' s)

Tactic:
exact fun s' hs' ↦ hf.measurableSet_image.mpr hs'

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ ((Measure.comap f ((κ : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t)

Tactic:
have : (fun a => Measure.comap f (κ a) t) = fun a => κ a (f '' t) := by
      ext1 a
      rw [Measure.comap_apply _ hf.injective _ _ ht]
      exact fun s' hs' ↦ hf.measurableSet_image.mpr hs'
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ ((Measure.comap f ((κ : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t)
rw : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t)
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.comap f ((κ : (a : α) → Measure β) b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t

Tactic:
rw [this]
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞)
    (fun (a : α) ↦ ((Measure.comap f ((κ : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) fun (a : α) ↦
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t)
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t)

Tactic:
Kernel.measurable_coe _ (hf.measurableSet_image.mpr ht)

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image, ProbabilityTheory.Kernel.measurable_coe