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 β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : IsFiniteKernel κ
inst_2 : IsFiniteKernel η
a : α
⊢ (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:
(ite_le_sup _ _ _).trans (sup_le_sup (measure_le_bound _ _ _) (measure_le_bound _ _ _))

Premises used: sup_le_sup, ite_le_sup, ProbabilityTheory.Kernel.measure_le_bound, LE.le.trans
-- 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 : α
⊢ (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:
exact (ite_le_sup _ _ _).trans (sup_le_sup (measure_le_bound _ _ _) (measure_le_bound _ _ _))

Premises used: sup_le_sup, ite_le_sup, ProbabilityTheory.Kernel.measure_le_bound, LE.le.trans
-- 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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
⊢ IsSFiniteKernel (piecewise (s := s) hs κ η)

Tactic:
⟨⟨fun n => piecewise hs (seq κ n) (seq η n), inferInstance, ?_⟩⟩

Premises used: ProbabilityTheory.IsSFiniteKernel.mk, inferInstance, ProbabilityTheory.Kernel.seq, ProbabilityTheory.Kernel.piecewise, And.intro, Exists.intro
-- 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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
refine : piecewise (s := s) hs κ η = Kernel.sum fun (n : ℕ) ↦ piecewise (s := s) hs (κ.seq n) (η.seq n)
⊢ IsSFiniteKernel (piecewise (s := s) hs κ η)

Tactic:
refine ⟨⟨fun n => piecewise hs (seq κ n) (seq η n), inferInstance, ?_⟩⟩
-- 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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
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 β)
⊢ piecewise (s := s) hs κ η = Kernel.sum fun (n : ℕ) ↦ piecewise (s := s) hs (κ.seq n) (η.seq n)

Tactic:
ext1 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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
a : α
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 β)
⊢ 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:
simp_rw [sum_apply, Kernel.piecewise_apply]

Premises used: ProbabilityTheory.Kernel.piecewise_apply, ProbabilityTheory.Kernel.sum_apply
-- 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 : 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 β)
neg :
  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 β)

Tactic:
split_ifs
-- 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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
a : α
h : a ∈ s
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a : Measure β)

Tactic:
(measure_sum_seq _ a).symm

Premises used: ProbabilityTheory.Kernel.measure_sum_seq, Eq.symm
-- 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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
a : α
h : a ∈ s
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a : Measure β)

Tactic:
exact (measure_sum_seq _ a).symm

Premises used: ProbabilityTheory.Kernel.measure_sum_seq, Eq.symm
-- 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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
a : α
h : a ∉ s
⊢ Eq.{u_2 + 1} (α := Measure β) ((η : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ℕ) ↦ (η.seq n : (a : α) → Measure β) a : Measure β)

Tactic:
(measure_sum_seq _ a).symm

Premises used: ProbabilityTheory.Kernel.measure_sum_seq, Eq.symm
-- 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 : IsSFiniteKernel κ
inst_2 : IsSFiniteKernel η
a : α
h : a ∉ s
⊢ Eq.{u_2 + 1} (α := Measure β) ((η : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ℕ) ↦ (η.seq n : (a : α) → Measure β) a : Measure β)

Tactic:
exact (measure_sum_seq _ a).symm

Premises used: ProbabilityTheory.Kernel.measure_sum_seq, Eq.symm
-- 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 : α
g : β → ℝ≥0∞
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
⊢ ∫⁻ (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

Tactic:
simp_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 : α
g : β → ℝ≥0∞
pos : a ∈ s → ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) a
neg : 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

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 : α
g : β → ℝ≥0∞
h : a ∈ s
⊢ ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), g b ∂(κ : (a : α) → Measure β) a

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 : α
g : β → ℝ≥0∞
h : a ∉ s
⊢ ∫⁻ (b : β), g b ∂(η : (a : α) → Measure β) a = ∫⁻ (b : β), g b ∂(η : (a : α) → Measure β) a

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 : α
g : β → ℝ≥0∞
t : Set β
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
⊢ ∫⁻ (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

Tactic:
simp_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 : α
g : β → ℝ≥0∞
t : Set β
pos : a ∈ s → ∫⁻ (b : β) in t, g b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β) in t, g b ∂(κ : (a : α) → Measure β) a
neg : 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

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 : α
g : β → ℝ≥0∞
t : Set β
h : a ∈ s
⊢ ∫⁻ (b : β) in t, g b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β) in t, g b ∂(κ : (a : α) → Measure β) a

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 : α
g : β → ℝ≥0∞
t : Set β
h : a ∉ s
⊢ ∫⁻ (b : β) in t, g b ∂(η : (a : α) → Measure β) a = ∫⁻ (b : β) in t, g b ∂(η : (a : α) → Measure β) a

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Basic
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
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (toMeasurable μ {a : α | ¬IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simpa [measure_toMeasurable] using h

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.Probability.Kernel.Basic
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
refine :
  ∀ a ∉ toMeasurable μ {a : α | ¬IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)},
    IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        ∀ a ∉ s, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)

Tactic:
refine ⟨toMeasurable μ {a | ¬ IsProbabilityMeasure (κ a)}, measurableSet_toMeasurable _ _,
      by simpa [measure_toMeasurable] using h, ?_⟩
-- Module: Mathlib.Probability.Kernel.Basic
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)}
contrapose :
  ∀ (ha : ¬IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)),
    a ∈ toMeasurable μ {a : α | ¬IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)}
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)

Tactic:
contrapose ha
-- Module: Mathlib.Probability.Kernel.Basic
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 : ¬IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
⊢ a ∈ toMeasurable μ {a : α | ¬IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)}

Tactic:
subset_toMeasurable _ _ ha

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.Probability.Kernel.Basic
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 : ¬IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
⊢ a ∈ toMeasurable μ {a : α | ¬IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)}

Tactic:
exact subset_toMeasurable _ _ ha

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.Probability.Kernel.Basic
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 α) (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 η

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
-- Module: Mathlib.Probability.Kernel.Basic
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)
contrapose! : ∀ (h' : sᶜ = ∅), μ = 0
⊢ sᶜ.Nonempty

Tactic:
contrapose! h'
-- Module: Mathlib.Probability.Kernel.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
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)
h' : sᶜ = ∅
⊢ μ = 0

Tactic:
simpa [μs, h'] using measure_univ_le_add_compl s (μ := μ)

Premises used: MeasureTheory.measure_univ_le_add_compl
-- Module: Mathlib.Probability.Kernel.Basic
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)
obtain :
  ∀ (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 η

Tactic:
obtain ⟨a, ha⟩ : sᶜ.Nonempty := by
    contrapose! h'; simpa [μs, h'] using measure_univ_le_add_compl s (μ := μ)

Premises used: Compl.compl, Set.Nonempty
-- Module: Mathlib.Probability.Kernel.Basic
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 η

Tactic:
⟨Kernel.piecewise s_meas (Kernel.const _ (κ a)) κ, ?_, ?_⟩

Premises used: ProbabilityTheory.Kernel.piecewise, And.intro, Exists.intro, ProbabilityTheory.Kernel.const, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Basic
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 β)
refine_2 : IsMarkovKernel (piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ)
⊢ ∃ (η : Kernel α β),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β) ∧
      IsMarkovKernel η

Tactic:
refine ⟨Kernel.piecewise s_meas (Kernel.const _ (κ a)) κ, ?_, ?_⟩
-- Module: Mathlib.Probability.Kernel.Basic
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ᶜ
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 β)
⊢ Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β)
    (⇑(piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ) : (a : α) → Measure β)

Tactic:
filter_upwards [measure_eq_zero_iff_ae_notMem.1 μs] with b hb

Premises used: Iff.mp, MeasureTheory.measure_eq_zero_iff_ae_notMem
-- Module: Mathlib.Probability.Kernel.Basic
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 : α
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:
simp [hb, piecewise]

Premises used: ProbabilityTheory.Kernel.piecewise
-- Module: Mathlib.Probability.Kernel.Basic
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)) κ)

Tactic:
⟨fun b ↦ ?_⟩

Premises used: ProbabilityTheory.IsMarkovKernel.mk
-- Module: Mathlib.Probability.Kernel.Basic
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_2 :
  ∀ (b : α),
    IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ)
      ((piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ : (a : α) → Measure β) b)
⊢ IsMarkovKernel (piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ)

Tactic:
refine ⟨fun b ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.Basic
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)
neg :
  ∀ (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)

Tactic:
by_cases hb : b ∈ s
-- Module: Mathlib.Probability.Kernel.Basic
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 : α
hb : b ∈ s
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ)
    ((piecewise (s := s) s_meas (const α ((κ : (a : α) → Measure β) a)) κ : (a : α) → Measure β) b)

Tactic:
simpa [hb, piecewise] using hs _ ha

Premises used: ProbabilityTheory.Kernel.piecewise