awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((((κ.comapRight hf : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' 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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ κ.comapRight ⋯ = κ
have h : ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((κ.comapRight sorry : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext _ _ hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
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∞)
have h : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (id '' s) : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [comapRight_apply' _ _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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)
have refine : ∀ (a : α),
  Eq (α := ℝ≥0∞) ((((κ.comapRight hf : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
Tactic: refine ⟨fun a => ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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∞) ((((κ.comapRight hf : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' Set.univ) : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [comapRight_apply' κ hf a MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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∞) (f '' Set.univ) : ℝ≥0∞) (1 : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.range f) : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: simp only [Set.image_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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)
have refine : ∀ (a : α), (((κ.comapRight hf : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound
Tactic: refine ⟨⟨κ.bound, κ.bound_lt_top, fun a => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 : α
⊢ (((κ.comapRight hf : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ ≤ κ.bound
have rw : (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' Set.univ) ≤ κ.bound
Tactic: rw [comapRight_apply' κ hf a .univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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)
have refine : κ.comapRight hf = Kernel.sum fun (n : ℕ) ↦ (κ.seq n).comapRight hf
Tactic: refine ⟨⟨fun n => comapRight (seq κ n) hf, inferInstance, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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
⊢ κ.comapRight hf = Kernel.sum fun (n : ℕ) ↦ (κ.seq n).comapRight hf
have 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 γ)
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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))
have 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∞)
Tactic: ext1 t ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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
⊢ 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∞)
have 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))
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)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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
⊢ 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))
have 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∞)
Tactic: congr with n : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 : ℕ
⊢ 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∞)
have 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∞)
Tactic: rw [Measure.comap_apply _ hf.injective (fun s' => hf.measurableSet_image.mpr) _ ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (hypothesis)
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.comap f ((κ : (a : α) → Measure β) a))
    (Measure.sum fun (n : ℕ) ↦ Measure.comap f ((κ.seq n : (a : α) → Measure β) a))
have 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))
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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))
⊢ Eq (α := Measure γ) (Measure.comap f ((κ : (a : α) → Measure β) a))
    (Measure.sum fun (n : ℕ) ↦ Measure.comap f ((κ.seq n : (a : α) → Measure β) a))
have h : Eq (α := Measure γ) (Measure.comap f ((κ : (a : α) → Measure β) a))
  (Measure.comap f (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a))
Tactic: rw [this, measure_sum_seq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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))
⊢ Eq (α := Measure γ) (Measure.comap f ((κ : (a : α) → Measure β) a))
    (Measure.sum fun (n : ℕ) ↦ Measure.comap f ((κ.seq n : (a : α) → Measure β) a))
have h₁ : Eq (α := Measure γ) (Measure.comap f ((κ : (a : α) → Measure β) a)) (Measure.comap f ((κ : (a : α) → Measure β) a))
Tactic: rw [this, measure_sum_seq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 β
⊢ 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∞)
have 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∞)
Tactic: rw [piecewise_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 β
⊢ 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∞)
have pos : a ∈ s →
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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∞)
⊢ 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∞)
have neg : a ∉ s →
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
    ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 κ η)
have refine : ∀ (a : α),
  Eq (α := ℝ≥0∞)
    ((((Kernel.piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
Tactic: refine ⟨fun a => ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 : α
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
have 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∞)
Tactic: rw [piecewise_apply', measure_univ, measure_univ, ite_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (if a ∈ s then 1 else (((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
  (1 : ℝ≥0∞)
Tactic: rw [piecewise_apply', measure_univ, measure_univ, ite_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) (if a ∈ s then 1 else 1) 1
Tactic: rw [piecewise_apply', measure_univ, measure_univ, ite_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [piecewise_apply', measure_univ, measure_univ, ite_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 κ η)
have refine : ∀ (a : α),
  (((Kernel.piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤
    max κ.bound η.bound
Tactic: refine ⟨⟨max κ.bound η.bound, max_lt κ.bound_lt_top η.bound_lt_top, fun a => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 : α
⊢ (((Kernel.piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤
    max κ.bound η.bound
have 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
Tactic: rw [piecewise_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
⊢ IsSFiniteKernel (piecewise (s := s) hs κ η)
have refine : piecewise (s := s) hs κ η = Kernel.sum fun (n : ℕ) ↦ piecewise (s := s) hs (κ.seq n) (η.seq n)
Tactic: refine ⟨⟨fun n => piecewise hs (seq κ n) (seq η n), inferInstance, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
⊢ piecewise (s := s) hs κ η = Kernel.sum fun (n : ℕ) ↦ piecewise (s := s) hs (κ.seq n) (η.seq n)
have h : ∀ (a : α),
  Eq.{u_2 + 1} (α := Measure β) ((piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β)
    ((Kernel.sum fun (n : ℕ) ↦ piecewise (s := s) hs (κ.seq n) (η.seq n) : (a : α) → Measure β) a : Measure β)
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) ((piecewise (s := s) hs κ η : (a : α) → Measure β) a : Measure β)
    ((Kernel.sum fun (n : ℕ) ↦ piecewise (s := s) hs (κ.seq n) (η.seq n) : (a : α) → Measure β) a : Measure β)
have h : Eq.{u_2 + 1} (α := Measure β) (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a : Measure β)
  (Measure.sum fun (n : ℕ) ↦ if a ∈ s then (κ.seq n : (a : α) → Measure β) a else (η.seq n : (a : α) → Measure β) a :
    Measure β)
Tactic: simp_rw [sum_apply, Kernel.piecewise_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ℕ) ↦ if a ∈ s then (κ.seq n : (a : α) → Measure β) a else (η.seq n : (a : α) → Measure β) a :
      Measure β)
have pos : a ∈ s →
  Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a : Measure β)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
a : α
pos :
  a ∈ s →
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
      (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a : Measure β)
⊢ Eq.{u_2 + 1} (α := Measure β) (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ℕ) ↦ if a ∈ s then (κ.seq n : (a : α) → Measure β) a else (η.seq n : (a : α) → Measure β) a :
      Measure β)
have neg : a ∉ s →
  Eq.{u_2 + 1} (α := Measure β) ((η : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ℕ) ↦ (η.seq n : (a : α) → Measure β) a : Measure β)
Tactic: split_ifs