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 β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → ℝ≥0∞
⊢ ∫⁻ (b : β), g b ∂(piecewise (s := s) hs κ η : (a : α) → Measure β) a =
    if a ∈ s then ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) a else ∫⁻ (b : β), g b ∂(η : (a : α) → Measure β) a
have simp_rw : (∫⁻ (b : β), g b ∂if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) =
  if a ∈ s then ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) a else ∫⁻ (b : β), g b ∂(η : (a : α) → Measure β) a
Tactic: simp_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 : α
g : β → ℝ≥0∞
⊢ (∫⁻ (b : β), g b ∂if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) =
    if a ∈ s then ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) a else ∫⁻ (b : β), g b ∂(η : (a : α) → Measure β) a
have pos : a ∈ s → ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) a
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 : α
g : β → ℝ≥0∞
pos : a ∈ s → ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) a
⊢ (∫⁻ (b : β), g b ∂if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) =
    if a ∈ s then ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) a else ∫⁻ (b : β), g b ∂(η : (a : α) → Measure β) a
have neg : a ∉ s → ∫⁻ (b : β), g b ∂(η : (a : α) → Measure β) a = ∫⁻ (b : β), g b ∂(η : (a : α) → Measure β) a
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 : α
g : β → ℝ≥0∞
t : Set β
⊢ ∫⁻ (b : β) in t, g b ∂(piecewise (s := s) hs κ η : (a : α) → Measure β) a =
    if a ∈ s then ∫⁻ (b : β) in t, g b ∂(κ : (a : α) → Measure β) a
    else ∫⁻ (b : β) in t, g b ∂(η : (a : α) → Measure β) a
have simp_rw : (∫⁻ (b : β) in t, g b ∂if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) =
  if a ∈ s then ∫⁻ (b : β) in t, g b ∂(κ : (a : α) → Measure β) a else ∫⁻ (b : β) in t, g b ∂(η : (a : α) → Measure β) a
Tactic: simp_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 : α
g : β → ℝ≥0∞
t : Set β
⊢ (∫⁻ (b : β) in t, g b ∂if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) =
    if a ∈ s then ∫⁻ (b : β) in t, g b ∂(κ : (a : α) → Measure β) a
    else ∫⁻ (b : β) in t, g b ∂(η : (a : α) → Measure β) a
have pos : a ∈ s → ∫⁻ (b : β) in t, g b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β) in t, g b ∂(κ : (a : α) → Measure β) a
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 : α
g : β → ℝ≥0∞
t : Set β
pos : a ∈ s → ∫⁻ (b : β) in t, g b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β) in t, g b ∂(κ : (a : α) → Measure β) a
⊢ (∫⁻ (b : β) in t, g b ∂if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) =
    if a ∈ s then ∫⁻ (b : β) in t, g b ∂(κ : (a : α) → Measure β) a
    else ∫⁻ (b : β) in t, g b ∂(η : (a : α) → Measure β) a
have neg : a ∉ s → ∫⁻ (b : β) in t, g b ∂(η : (a : α) → Measure β) a = ∫⁻ (b : β) in t, g b ∂(η : (a : α) → Measure β) a
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 α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
have refine : ∀ a ∉ toMeasurable μ {a : α | ¬IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)},
  IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
Tactic: refine ⟨toMeasurable μ {a | ¬ IsProbabilityMeasure (κ a)}, measurableSet_toMeasurable _ _,
      by simpa [measure_toMeasurable] using h, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
a : α
ha : a ∉ toMeasurable μ {a : α | ¬IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)}
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
have contrapose : ∀ (ha : ¬IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)),
  a ∈ toMeasurable μ {a : α | ¬IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)}
Tactic: contrapose ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
⊢ ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η
have obtain : ∀ (s : Set α) (s_meas : MeasurableSet s) (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
  (hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)),
  ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η
Tactic: obtain ⟨s, s_meas, μs, hs⟩ : ∃ s, MeasurableSet s ∧ μ s = 0
      ∧ ∀ a ∉ s, IsProbabilityMeasure (κ a) := by
    refine ⟨toMeasurable μ {a | ¬ IsProbabilityMeasure (κ a)}, measurableSet_toMeasurable _ _,
      by simpa [measure_toMeasurable] using h, ?_⟩
    intro a ha
    contrapose ha
    exact subset_toMeasurable _ _ ha
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
⊢ sᶜ.Nonempty
have contrapose! : ∀ (h' : sᶜ = ∅), μ = 0
Tactic: contrapose! h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
⊢ ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η
have obtain : ∀ (a : α) (ha : a ∈ sᶜ),
  ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η
Tactic: obtain ⟨a, ha⟩ : sᶜ.Nonempty := by
    contrapose! h'; simpa [μs, h'] using measure_univ_le_add_compl s (μ := μ)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
a : α
ha : a ∈ sᶜ
⊢ ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η
have refine_1 : Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β)
  (⇑(piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ) : (a : α) → Measure β)
Tactic: refine ⟨Kernel.piecewise s_meas (Kernel.const _ (κ a)) κ, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
a : α
ha : a ∈ sᶜ
refine_1 :
  Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β)
    (⇑(piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ) : (a : α) → Measure β)
⊢ ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η
have refine_2 : IsMarkovKernel (piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ)
Tactic: refine ⟨Kernel.piecewise s_meas (Kernel.const _ (κ a)) κ, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
a : α
ha : a ∈ sᶜ
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β)
    (⇑(piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ) : (a : α) → Measure β)
have h₁ : ∀ (b : α) (hb : b ∉ s),
  Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) b : Measure β)
    ((piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ : (a : α) → Measure β) b : Measure β)
Tactic: filter_upwards [measure_eq_zero_iff_ae_notMem.1 μs] with b hb
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
a : α
ha : a ∈ sᶜ
⊢ IsMarkovKernel (piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ)
have refine_2 : ∀ (b : α),
  IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ)
    ((piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ : (a : α) → Measure β) b)
Tactic: refine ⟨fun b ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
a : α
ha : a ∈ sᶜ
b : α
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ)
    ((piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ : (a : α) → Measure β) b)
have pos : ∀ (hb : b ∈ s),
  IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ)
    ((piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ : (a : α) → Measure β) b)
Tactic: by_cases hb : b ∈ s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
a : α
ha : a ∈ sᶜ
b : α
pos :
  ∀ (hb : b ∈ s),
    IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ)
      ((piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ : (a : α) → Measure β) b)
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ)
    ((piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ : (a : α) → Measure β) b)
have neg : ∀ (hb : b ∉ s),
  IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ)
    ((piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ : (a : α) → Measure β) b)
Tactic: by_cases hb : b ∈ s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
⊢ ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η
have obtain : ∃ (s : Set α),
  MeasurableSet s ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
      ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
Tactic: classical
  obtain ⟨s, s_meas, μs, hs⟩ : ∃ s, MeasurableSet s ∧ μ s = 0
      ∧ ∀ a ∉ s, IsProbabilityMeasure (κ a) := by
    refine ⟨toMeasurable μ {a | ¬ IsProbabilityMeasure (κ a)}, measurableSet_toMeasurable _ _,
      by simpa [measure_toMeasurable] using h, ?_⟩
    intro a ha
    contrapose ha
    exact subset_toMeasurable _ _ ha
  obtain ⟨a, ha⟩ : sᶜ.Nonempty := by
    contrapose! h'; simpa [μs, h'] using measure_univ_le_add_compl s (μ := μ)
  refine ⟨Kernel.piecewise s_meas (Kernel.const _ (κ a)) κ, ?_, ?_⟩
  · filter_upwards [measure_eq_zero_iff_ae_notMem.1 μs] with b hb
    simp [hb, piecewise]
  · refine ⟨fun b ↦ ?_⟩
    by_cases hb : b ∈ s
    · simpa [hb, piecewise] using hs _ ha
    · simpa [hb, piecewise] using hs _ hb
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
obtain :
  ∃ (s : Set α),
    MeasurableSet s ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
⊢ ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η
have obtain₁ : ∀ (s : Set α) (s_meas : MeasurableSet s) (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
  (hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)),
  ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η
Tactic: classical
  obtain ⟨s, s_meas, μs, hs⟩ : ∃ s, MeasurableSet s ∧ μ s = 0
      ∧ ∀ a ∉ s, IsProbabilityMeasure (κ a) := by
    refine ⟨toMeasurable μ {a | ¬ IsProbabilityMeasure (κ a)}, measurableSet_toMeasurable _ _,
      by simpa [measure_toMeasurable] using h, ?_⟩
    intro a ha
    contrapose ha
    exact subset_toMeasurable _ _ ha
  obtain ⟨a, ha⟩ : sᶜ.Nonempty := by
    contrapose! h'; simpa [μs, h'] using measure_univ_le_add_compl s (μ := μ)
  refine ⟨Kernel.piecewise s_meas (Kernel.const _ (κ a)) κ, ?_, ?_⟩
  · filter_upwards [measure_eq_zero_iff_ae_notMem.1 μs] with b hb
    simp [hb, piecewise]
  · refine ⟨fun b ↦ ?_⟩
    by_cases hb : b ∈ s
    · simpa [hb, piecewise] using hs _ ha
    · simpa [hb, piecewise] using hs _ hb
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
obtain :
  ∃ (s : Set α),
    MeasurableSet s ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
obtain₁ :
  ∀ (s : Set α) (s_meas : MeasurableSet s) (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
    (hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)),
    ∃ (η : Kernel α β),
      Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
        IsMarkovKernel η
⊢ ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η
have obtain₂ : ∀ (s : Set α) (s_meas : MeasurableSet s) (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
  (hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)) (a : α) (ha : a ∈ sᶜ),
  ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η
Tactic: classical
  obtain ⟨s, s_meas, μs, hs⟩ : ∃ s, MeasurableSet s ∧ μ s = 0
      ∧ ∀ a ∉ s, IsProbabilityMeasure (κ a) := by
    refine ⟨toMeasurable μ {a | ¬ IsProbabilityMeasure (κ a)}, measurableSet_toMeasurable _ _,
      by simpa [measure_toMeasurable] using h, ?_⟩
    intro a ha
    contrapose ha
    exact subset_toMeasurable _ _ ha
  obtain ⟨a, ha⟩ : sᶜ.Nonempty := by
    contrapose! h'; simpa [μs, h'] using measure_univ_le_add_compl s (μ := μ)
  refine ⟨Kernel.piecewise s_meas (Kernel.const _ (κ a)) κ, ?_, ?_⟩
  · filter_upwards [measure_eq_zero_iff_ae_notMem.1 μs] with b hb
    simp [hb, piecewise]
  · refine ⟨fun b ↦ ?_⟩
    by_cases hb : b ∈ s
    · simpa [hb, piecewise] using hs _ ha
    · simpa [hb, piecewise] using hs _ hb
-- Lean 4 proof step from Mathlib.Probability.Kernel.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
h' : μ ≠ 0
obtain :
  ∃ (s : Set α),
    MeasurableSet s ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
obtain₁ :
  ∀ (s : Set α) (s_meas : MeasurableSet s) (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
    (hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)),
    ∃ (η : Kernel α β),
      Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
        IsMarkovKernel η
obtain₂ :
  ∀ (s : Set α) (s_meas : MeasurableSet s) (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
    (hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)) (a : α) (ha : a ∈ sᶜ),
    ∃ (η : Kernel α β),
      Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
        IsMarkovKernel η
⊢ ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η
have refine_1 : ∀ (s : Set α) (s_meas : MeasurableSet s) (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
  (hs : ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)) (a : α) (ha : a ∈ sᶜ),
  Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β)
    (⇑(piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ) : (a : α) → Measure β)
Tactic: classical
  obtain ⟨s, s_meas, μs, hs⟩ : ∃ s, MeasurableSet s ∧ μ s = 0
      ∧ ∀ a ∉ s, IsProbabilityMeasure (κ a) := by
    refine ⟨toMeasurable μ {a | ¬ IsProbabilityMeasure (κ a)}, measurableSet_toMeasurable _ _,
      by simpa [measure_toMeasurable] using h, ?_⟩
    intro a ha
    contrapose ha
    exact subset_toMeasurable _ _ ha
  obtain ⟨a, ha⟩ : sᶜ.Nonempty := by
    contrapose! h'; simpa [μs, h'] using measure_univ_le_add_compl s (μ := μ)
  refine ⟨Kernel.piecewise s_meas (Kernel.const _ (κ a)) κ, ?_, ?_⟩
  · filter_upwards [measure_eq_zero_iff_ae_notMem.1 μs] with b hb
    simp [hb, piecewise]
  · refine ⟨fun b ↦ ?_⟩
    by_cases hb : b ∈ s
    · simpa [hb, piecewise] using hs _ ha
    · simpa [hb, piecewise] using hs _ hb