awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
rw : ∫⁻ (a : α), f a ∂Measure.dirac a = f a
⊢ ∫⁻ (a : α), f a ∂(Kernel.id : (a : α) → Measure α) a = f a
have rw₁ : f a = f a
Tactic: rw [id_apply, lintegral_dirac' _ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ ∫⁻ (a : α), f a ∂(Kernel.id : (a : α) → Measure α) a = f a
have rw : ∫⁻ (a : α), f a ∂Measure.dirac a = f a
Tactic: rw [id_apply, lintegral_dirac]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
inst : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
rw : ∫⁻ (a : α), f a ∂Measure.dirac a = f a
⊢ ∫⁻ (a : α), f a ∂(Kernel.id : (a : α) → Measure α) a = f a
have rw₁ : f a = f a
Tactic: rw [id_apply, lintegral_dirac]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ab : α × β
⊢ Eq (α := Measure (β × α)) ((swap α β : (a : α × β) → Measure (β × α)) ab : Measure (β × α))
    (Measure.dirac ab.swap : Measure (β × α))
have rw : Eq (α := Measure (β × α)) ((deterministic Prod.swap sorry : (a : α × β) → Measure (β × α)) ab : Measure (β × α))
  (Measure.dirac ab.swap : Measure (β × α))
Tactic: rw [swap, deterministic_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ab : α × β
rw :
  Eq (α := Measure (β × α)) ((deterministic Prod.swap ⋯ : (a : α × β) → Measure (β × α)) ab : Measure (β × α))
    (Measure.dirac ab.swap : Measure (β × α))
⊢ Eq (α := Measure (β × α)) ((swap α β : (a : α × β) → Measure (β × α)) ab : Measure (β × α))
    (Measure.dirac ab.swap : Measure (β × α))
have rw₁ : Eq (α := Measure (β × α)) (Measure.dirac ab.swap) (Measure.dirac ab.swap)
Tactic: rw [swap, deterministic_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ab : α × β
s : Set (β × α)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((swap α β : (a : α × β) → Measure (β × α)) ab : Measure (β × α)) : (a : Set (β × α)) → ℝ≥0∞) s : ℝ≥0∞)
    (s.indicator 1 ab.swap : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((Measure.dirac ab.swap : (a : Set (β × α)) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 ab.swap : ℝ≥0∞)
Tactic: rw [swap_apply, Measure.dirac_apply' _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ab : α × β
s : Set (β × α)
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((Measure.dirac ab.swap : (a : Set (β × α)) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 ab.swap : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((swap α β : (a : α × β) → Measure (β × α)) ab : Measure (β × α)) : (a : Set (β × α)) → ℝ≥0∞) s : ℝ≥0∞)
    (s.indicator 1 ab.swap : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (s.indicator 1 ab.swap) (s.indicator 1 ab.swap)
Tactic: rw [swap_apply, Measure.dirac_apply' _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ Eq (α := Kernel α β) (const α 0) 0
have h : ∀ (x : α) (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((((const α 0 : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((((0 : Kernel α β) : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext x s _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
β : Type u_4
inst : MeasurableSpace β
μ ν : Measure α
⊢ const β (μ + ν) = HAdd.hAdd (α := Kernel β α) (const β μ) (const β ν)
have h : ∀ (a : β) (s : Set α),
  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: ext
-- 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 α β
μβ : Measure β
inst : SFinite μβ
⊢ Eq (α := Kernel α β) (const α μβ) (Kernel.sum fun (n : ℕ) ↦ const α (sfiniteSeq μβ n))
have rw : Eq (α := Kernel α β) (const α μβ) (const α (Measure.sum (sfiniteSeq μβ)))
Tactic: rw [sum_const, sum_sfiniteSeq]
-- 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 α β
μβ : Measure β
inst : SFinite μβ
rw : Eq (α := Kernel α β) (const α μβ) (const α (Measure.sum (sfiniteSeq μβ)))
⊢ Eq (α := Kernel α β) (const α μβ) (Kernel.sum fun (n : ℕ) ↦ const α (sfiniteSeq μβ n))
have rw₁ : Eq (α := Kernel α β) (const α μβ) (const α μβ)
Tactic: rw [sum_const, sum_sfiniteSeq]
-- 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 α β
μβ : Measure β
hμβ : IsZeroOrProbabilityMeasure μβ
⊢ IsZeroOrMarkovKernel (mα := mα) (const α μβ)
have inl : ∀ [hμβ : IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) 0],
  IsZeroOrMarkovKernel.{u_1, u_2} (β := β) (mα := mα) (mβ := mβ) (const α 0)
Tactic: rcases eq_zero_or_isProbabilityMeasure μβ with rfl | h
Cleared hypotheses: μβ, hμβ
-- 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 α β
μβ : Measure β
hμβ : IsZeroOrProbabilityMeasure μβ
inl :
  ∀ [hμβ : IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) 0],
    IsZeroOrMarkovKernel.{u_1, u_2} (β := β) (mα := mα) (mβ := mβ) (const α 0)
⊢ IsZeroOrMarkovKernel (mα := mα) (const α μβ)
have inr : ∀ (h : IsProbabilityMeasure μβ), IsZeroOrMarkovKernel (mα := mα) (const α μβ)
Tactic: rcases eq_zero_or_isProbabilityMeasure μβ with rfl | h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
μ : Measure β
a : α
⊢ ∫⁻ (x : β), f x ∂((const α μ : Kernel α β) : (a : α) → Measure β) a = ∫⁻ (x : β), f x ∂μ
have rw : ∫⁻ (x : β), f x ∂μ = ∫⁻ (x : β), f x ∂μ
Tactic: rw [const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
μ : Measure β
a : α
s : Set β
⊢ ∫⁻ (x : β) in s, f x ∂((const α μ : Kernel α β) : (a : α) → Measure β) a = ∫⁻ (x : β) in s, f x ∂μ
have rw : ∫⁻ (x : β) in s, f x ∂μ = ∫⁻ (x : β) in s, f x ∂μ
Tactic: rw [const_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 β
κ_1 : Kernel α β
s t : Set β
κ : Kernel α β
hs : MeasurableSet s
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (a : α) ↦ Measure.restrict ((κ : (a : α) → Measure β) a) s
have refine : ∀ (t : Set β) (ht : MeasurableSet t),
  Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.restrict ((κ : (a : α) → Measure β) b) s : Measure β) : (a : Set β) → ℝ≥0∞) t
Tactic: refine Measure.measurable_of_measurable_coe _ fun 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 α β
s t_1 : Set β
κ : Kernel α β
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.restrict ((κ : (a : α) → Measure β) b) s : Measure β) : (a : Set β) → ℝ≥0∞) t
have simp_rw : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (((κ : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) (t ∩ s)
Tactic: simp_rw [Measure.restrict_apply ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set β
κ : Kernel α β
hs : MeasurableSet s
a : α
ht : MeasurableSet t
⊢ 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∞)
have 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∞)
Tactic: rw [restrict_apply κ hs a, Measure.restrict_apply ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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∞)
⊢ 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∞)
have rw₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [restrict_apply κ hs a, Measure.restrict_apply ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
μ : Measure β
hs : MeasurableSet s
⊢ Eq (α := Kernel α β) (Kernel.restrict (s := s) (const α μ) hs) (const α (μ.restrict s))
have 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∞)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ κ.restrict (s := Set.univ) ⋯ = κ
have h : ∀ (a : α),
  Eq.{u_2 + 1} (α := Measure β) ((κ.restrict (s := Set.univ) sorry : (a : α) → Measure β) a : Measure β)
    ((κ : (a : α) → Measure β) a : Measure β)
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ.restrict (s := Set.univ) ⋯ : (a : α) → Measure β) a : Measure β)
    ((κ : (a : α) → Measure β) a : Measure β)
have h : Eq.{u_2 + 1} (α := Measure β) (Measure.restrict ((κ : (a : α) → Measure β) a) Set.univ) ((κ : (a : α) → Measure β) a)
Tactic: rw [Kernel.restrict_apply, Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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)
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ.restrict (s := Set.univ) ⋯ : (a : α) → Measure β) a : Measure β)
    ((κ : (a : α) → Measure β) a : Measure β)
have h₁ : Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) ((κ : (a : α) → Measure β) a : Measure β)
Tactic: rw [Kernel.restrict_apply, Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
κ : Kernel α β
hs : MeasurableSet s
a : α
f : β → ℝ≥0∞
⊢ ∫⁻ (b : β), f b ∂(κ.restrict (s := s) hs : (a : α) → Measure β) a = ∫⁻ (b : β) in s, f b ∂(κ : (a : α) → Measure β) a
have rw : ∫⁻ (b : β) in s, f b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β) in s, f b ∂(κ : (a : α) → Measure β) a
Tactic: rw [restrict_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
κ : Kernel α β
hs : MeasurableSet s
a : α
f : β → ℝ≥0∞
t : Set β
⊢ ∫⁻ (b : β) in t, f b ∂(κ.restrict (s := s) hs : (a : α) → Measure β) a =
    ∫⁻ (b : β) in t ∩ s, f b ∂(κ : (a : α) → Measure β) a
have rw : ∫⁻ (b : β) in t, f b ∂Measure.restrict ((κ : (a : α) → Measure β) a) s =
  ∫⁻ (b : β) in t ∩ s, f b ∂(κ : (a : α) → Measure β) a
Tactic: rw [restrict_apply, Measure.restrict_restrict' hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
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
⊢ ∫⁻ (b : β) in t, f b ∂(κ.restrict (s := s) hs : (a : α) → Measure β) a =
    ∫⁻ (b : β) in t ∩ s, f b ∂(κ : (a : α) → Measure β) a
have rw₁ : ∫⁻ (b : β) in t ∩ s, f b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β) in t ∩ s, f b ∂(κ : (a : α) → Measure β) a
Tactic: rw [restrict_apply, Measure.restrict_restrict' hs]
-- 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 α β
s t : Set β
κ : Kernel α β
inst : IsFiniteKernel κ
hs : MeasurableSet s
⊢ IsFiniteKernel (κ.restrict (s := s) hs)
have refine : ∀ (a : α), (((κ.restrict (s := s) hs : (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 α β
s t : Set β
κ : Kernel α β
inst : IsFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ (((κ.restrict (s := s) hs : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound
have rw : (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Set.univ ∩ s) ≤ κ.bound
Tactic: rw [restrict_apply' κ hs a MeasurableSet.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 α β
s t : Set β
κ : Kernel α β
inst : IsSFiniteKernel κ
hs : MeasurableSet s
⊢ IsSFiniteKernel (κ.restrict (s := s) hs)
have refine : κ.restrict (s := s) hs = Kernel.sum fun (n : ℕ) ↦ (κ.seq n).restrict (s := s) hs
Tactic: refine ⟨⟨fun n => Kernel.restrict (seq κ n) hs, 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 α β
s t : Set β
κ : Kernel α β
inst : IsSFiniteKernel κ
hs : MeasurableSet s
⊢ κ.restrict (s := s) hs = Kernel.sum fun (n : ℕ) ↦ (κ.seq n).restrict (s := s) hs
have 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 β)
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 α β
s t : Set β
κ : Kernel α β
inst : IsSFiniteKernel κ
hs : MeasurableSet s
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 β)
have 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 β)
Tactic: simp_rw [sum_apply, restrict_apply, ← Measure.restrict_sum _ hs, ← sum_apply, kernel_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 α β
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 β)
⊢ 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 β)
have h₁ : Eq (α := Measure β) (Measure.restrict ((κ : (a : α) → Measure β) a) s)
  (Measure.sum fun (n : ℕ) ↦ Measure.restrict ((κ.seq n : (a : α) → Measure β) a) s)
Tactic: simp_rw [sum_apply, restrict_apply, ← Measure.restrict_sum _ hs, ← sum_apply, kernel_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 α β
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)
⊢ 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 β)
have h₂ : Eq (α := Measure β) (Measure.restrict ((κ : (a : α) → Measure β) a) s)
  (Measure.restrict (Measure.sum fun (i : ℕ) ↦ (κ.seq i : (a : α) → Measure β) a) s)
Tactic: simp_rw [sum_apply, restrict_apply, ← Measure.restrict_sum _ hs, ← sum_apply, kernel_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 α β
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)
⊢ 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 β)
have h₃ : Eq (α := Measure β) (Measure.restrict ((κ : (a : α) → Measure β) a) s)
  (Measure.restrict ((Kernel.sum κ.seq : (a : α) → Measure β) a) s)
Tactic: simp_rw [sum_apply, restrict_apply, ← Measure.restrict_sum _ hs, ← sum_apply, kernel_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 α β
hf : MeasurableEmbedding f
⊢ Measurable.{u_1, u_4} (β := Measure γ) fun (a : α) ↦ Measure.comap f ((κ : (a : α) → Measure β) a)
have refine : ∀ (t : Set γ) (ht : MeasurableSet t),
  Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.comap f ((κ : (a : α) → Measure β) b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t
Tactic: refine Measure.measurable_measure.mpr fun 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 α β
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)
have 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∞)
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 α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
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∞)
have rw : ∀ (s : Set γ), MeasurableSet s → MeasurableSet (f '' s)
Tactic: rw [Measure.comap_apply _ hf.injective _ _ 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 α β
hf : MeasurableEmbedding f
t : Set γ
ht : MeasurableSet t
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.comap f ((κ : (a : α) → Measure β) b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t
have 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)
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'
-- 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 α β
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 (b : α) ↦
    ((Measure.comap f ((κ : (a : α) → Measure β) b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t
have rw : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (f '' t)
Tactic: rw [this]
-- 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
⊢ 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∞) (((Measure.comap f ((κ : (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]