awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact Kernel.measurable_coe _ (hf.measurableSet_image.mpr ht)

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
a : α
⊢ Eq.{u_4 + 1} (α := Measure γ) ((κ.comapRight hf : (a : α) → Measure γ) a : Measure γ)
    (Measure.comap f ((κ : (a : α) → Measure β) a) : Measure γ)

Tactic:
rfl

Premises used: dite, MeasureTheory.Measure.comap, rfl
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
rw :
  Eq (α := ℝ≥0∞) (((Measure.comap f ((κ : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.comapRight hf : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)

Tactic:
rw [comapRight_apply,
    Measure.comap_apply _ hf.injective (fun s => hf.measurableSet_image.mpr) _ ht]

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image, MeasureTheory.Measure.comap_apply, MeasurableEmbedding.injective, ProbabilityTheory.Kernel.comapRight_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h :
  ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ.comapRight ⋯ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ.comapRight ⋯ = κ

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

Tactic:
rw [comapRight_apply' _ _ _ hs]

Premises used: ProbabilityTheory.Kernel.comapRight_apply'
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (id '' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.range f) : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ IsMarkovKernel (κ.comapRight hf)

Tactic:
⟨fun a => ⟨?_⟩⟩

Premises used: MeasureTheory.IsProbabilityMeasure.mk, ProbabilityTheory.IsMarkovKernel.mk
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.range f) : ℝ≥0∞) (1 : ℝ≥0∞)
refine :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((κ.comapRight hf : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
⊢ IsMarkovKernel (κ.comapRight hf)

Tactic:
refine ⟨fun a => ⟨?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.range f) : ℝ≥0∞) (1 : ℝ≥0∞)
a : α
rw : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' Set.univ) : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.comapRight hf : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
rw [comapRight_apply' κ hf a MeasurableSet.univ]

Premises used: ProbabilityTheory.Kernel.comapRight_apply', MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.range f) : ℝ≥0∞) (1 : ℝ≥0∞)
a : α
simp : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.range f) : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' Set.univ) : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp only [Set.image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.range f) : ℝ≥0∞) (1 : ℝ≥0∞)
a : α
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.range f) : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
hκ a
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.range f) : ℝ≥0∞) (1 : ℝ≥0∞)
a : α
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.range f) : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
exact hκ 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 α β
inst : IsFiniteKernel κ
hf : MeasurableEmbedding f
⊢ IsFiniteKernel (κ.comapRight hf)

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 α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst : IsFiniteKernel κ
hf : MeasurableEmbedding f
refine : ∀ (a : α), (((κ.comapRight hf : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound
⊢ IsFiniteKernel (κ.comapRight hf)

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 α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst : IsFiniteKernel κ
hf : MeasurableEmbedding f
a : α
rw : (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' Set.univ) ≤ κ.bound
⊢ (((κ.comapRight hf : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound

Tactic:
rw [comapRight_apply' κ hf a .univ]

Premises used: ProbabilityTheory.Kernel.comapRight_apply', MeasurableSet.univ
-- 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 α β
inst : IsFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' Set.univ) ≤ κ.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 α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst : IsFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' Set.univ) ≤ κ.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 α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst : IsSFiniteKernel κ
hf : MeasurableEmbedding f
⊢ IsSFiniteKernel (κ.comapRight hf)

Tactic:
⟨⟨fun n => comapRight (seq κ n) hf, inferInstance, ?_⟩⟩

Premises used: ProbabilityTheory.IsSFiniteKernel.mk, ProbabilityTheory.Kernel.comapRight, 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 α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst : IsSFiniteKernel κ
hf : MeasurableEmbedding f
refine : κ.comapRight hf = Kernel.sum fun (n : ℕ) ↦ (κ.seq n).comapRight hf
⊢ IsSFiniteKernel (κ.comapRight hf)

Tactic:
refine ⟨⟨fun n => comapRight (seq κ n) hf, inferInstance, ?_⟩⟩
-- 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 α β
inst : IsSFiniteKernel κ
hf : MeasurableEmbedding f
h :
  ∀ (a : α),
    Eq.{u_4 + 1} (α := Measure γ) ((κ.comapRight hf : (a : α) → Measure γ) a : Measure γ)
      ((Kernel.sum fun (n : ℕ) ↦ (κ.seq n).comapRight hf : (a : α) → Measure γ) a : Measure γ)
⊢ κ.comapRight hf = Kernel.sum fun (n : ℕ) ↦ (κ.seq n).comapRight hf

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 α β
inst : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
h :
  ∀ (t : Set γ) (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞)
      (((Measure.sum fun (n : ℕ) ↦ Measure.comap f ((κ.seq n : (a : α) → Measure β) a) : Measure γ) :
            (a : Set γ) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (((Measure.comap f (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a) : Measure γ) :
            (a : Set γ) → ℝ≥0∞)
          t :
        ℝ≥0∞)
⊢ Eq (α := Measure γ) (Measure.sum fun (n : ℕ) ↦ Measure.comap f ((κ.seq n : (a : α) → Measure β) a))
    (Measure.comap f (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a))

Tactic:
ext1 t ht
-- 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 α β
inst : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
h :
  Eq (α := ℝ≥0∞)
    (∑' (i : ℕ), ((Measure.comap f ((κ.seq i : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) t)
    (∑' (i : ℕ), (((κ.seq i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t))
⊢ Eq (α := ℝ≥0∞)
    (((Measure.sum fun (n : ℕ) ↦ Measure.comap f ((κ.seq n : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    (((Measure.comap f (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        t :
      ℝ≥0∞)

Tactic:
rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht,
      Measure.sum_apply _ ht, Measure.sum_apply _ (hf.measurableSet_image.mpr ht)]

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image, MeasureTheory.Measure.sum_apply, 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 α β
inst : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
h :
  ∀ (n : ℕ),
    Eq (α := ℝ≥0∞) (((Measure.comap f ((κ.seq n : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
      ((((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (∑' (i : ℕ), ((Measure.comap f ((κ.seq i : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) t)
    (∑' (i : ℕ), (((κ.seq i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t))

Tactic:
congr with n : 1
-- 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 α β
inst : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
n : ℕ
h h₁ :
  Eq (α := ℝ≥0∞) ((((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
    ((((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f ((κ.seq n : (a : α) → Measure β) a) : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ.seq n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)

Tactic:
rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht]

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image, 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 α β
inst : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
⊢ Eq (α := Measure γ) (Measure.sum fun (n : ℕ) ↦ Measure.comap f ((κ.seq n : (a : α) → Measure β) a))
    (Measure.comap f (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a))

Tactic:
have :
    (Measure.sum fun n => Measure.comap f (seq κ n a)) =
      Measure.comap f (Measure.sum fun n => seq κ n a) := by
    ext1 t ht
    rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht,
      Measure.sum_apply _ ht, Measure.sum_apply _ (hf.measurableSet_image.mpr ht)]
    congr with n : 1
    rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht]
-- 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 α β
inst : IsSFiniteKernel κ
hf : MeasurableEmbedding f
a : α
this :
  Eq (α := Measure γ) (Measure.sum fun (n : ℕ) ↦ Measure.comap f ((κ.seq n : (a : α) → Measure β) a))
    (Measure.comap f (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a))
h :
  Eq (α := Measure γ) (Measure.comap f ((κ : (a : α) → Measure β) a))
    (Measure.comap f (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a))
h₁ h₂ :
  Eq (α := Measure γ) (Measure.comap f ((κ : (a : α) → Measure β) a)) (Measure.comap f ((κ : (a : α) → Measure β) a))
⊢ Eq (α := Measure γ) (Measure.comap f ((κ : (a : α) → Measure β) a))
    (Measure.sum fun (n : ℕ) ↦ Measure.comap f ((κ.seq n : (a : α) → Measure β) a))

Tactic:
rw [this, measure_sum_seq]

Premises used: ProbabilityTheory.Kernel.measure_sum_seq
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) ((piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β)
    (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a : Measure β)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
t : Set β
rw :
  Eq (α := ℝ≥0∞)
    (((if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t :
      ℝ≥0∞)
    (if a ∈ s then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t
      else (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    (if a ∈ s then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t
      else (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t :
      ℝ≥0∞)

Tactic:
rw [piecewise_apply]

Premises used: ProbabilityTheory.Kernel.piecewise_apply
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
t : Set β
pos :
  a ∈ s →
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
neg :
  a ∉ s →
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
      ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t :
      ℝ≥0∞)
    (if a ∈ s then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t
      else (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t :
      ℝ≥0∞)

Tactic:
split_ifs
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
t : Set β
h : a ∈ s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
t : Set β
h : a ∉ s
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
⊢ IsMarkovKernel (Kernel.piecewise (s := s) hs κ η)

Tactic:
⟨fun a => ⟨?_⟩⟩

Premises used: MeasureTheory.IsProbabilityMeasure.mk, ProbabilityTheory.IsMarkovKernel.mk
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
refine :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((Kernel.piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
⊢ IsMarkovKernel (Kernel.piecewise (s := s) hs κ η)

Tactic:
refine ⟨fun a => ⟨?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : IsMarkovKernel κ
inst_2 : IsMarkovKernel η
a : α
rw :
  Eq (α := ℝ≥0∞)
    (if a ∈ s then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ
      else (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) (if a ∈ s then 1 else (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) (if a ∈ s then 1 else 1) 1
rw₃ rw₄ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
rw [piecewise_apply', measure_univ, measure_univ, ite_self]

Premises used: ite_self, ProbabilityTheory.Kernel.piecewise_apply', MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : IsFiniteKernel κ
inst_2 : IsFiniteKernel η
⊢ IsFiniteKernel (Kernel.piecewise (s := s) hs κ η)

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

Premises used: ProbabilityTheory.IsFiniteKernel.mk, max_lt, ProbabilityTheory.Kernel.bound_lt_top, Max.max, 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 β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : IsFiniteKernel κ
inst_2 : IsFiniteKernel η
refine :
  ∀ (a : α),
    (((Kernel.piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤
      max κ.bound η.bound
⊢ IsFiniteKernel (Kernel.piecewise (s := s) hs κ η)

Tactic:
refine ⟨⟨max κ.bound η.bound, max_lt κ.bound_lt_top η.bound_lt_top, fun a => ?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : IsFiniteKernel κ
inst_2 : IsFiniteKernel η
a : α
rw :
  (if a ∈ s then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ
    else (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ) ≤
    max κ.bound η.bound
⊢ (((Kernel.piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤
    max κ.bound η.bound

Tactic:
rw [piecewise_apply']

Premises used: ProbabilityTheory.Kernel.piecewise_apply'