awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) ((η : (a : α) → Measure β) a : Measure β)
⊢ κ = η

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
simp_rw :
  (∀ (a : α),
      Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β)
        ((η : (a : α) → Measure β) a : Measure β)) ↔
    ∀ (a : α) (s : Set β),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ = η ↔
    ∀ (a : α) (s : Set β),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [Kernel.ext_iff, Measure.ext_iff]

Premises used: MeasureTheory.Measure.ext_iff, ProbabilityTheory.Kernel.ext_iff
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h :
  ∀ (a : α) (f : β → ℝ≥0∞),
    Measurable f → ∫⁻ (b : β), f b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), f b ∂(η : (a : α) → Measure β) a
h₁ :
  ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ = η

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h :
  ∀ (a : α) (f : β → ℝ≥0∞),
    Measurable f → ∫⁻ (b : β), f b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), f b ∂(η : (a : α) → Measure β) a
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β), s.indicator (fun (x : β) ↦ 1) b ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β), s.indicator (fun (x : β) ↦ 1) b ∂(η : (a : α) → Measure β) a

Tactic:
specialize h a (s.indicator fun _ => 1) (Measurable.indicator measurable_const hs)

Premises used: Set.indicator, Measurable.indicator, measurable_const, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
h :
  ∫⁻ (b : β), s.indicator (fun (x : β) ↦ 1) b ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β), s.indicator (fun (x : β) ↦ 1) b ∂(η : (a : α) → Measure β) a
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [lintegral_indicator_const hs, one_mul] at h

Premises used: MeasureTheory.lintegral_indicator_const, one_mul
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
h₁ h₂ :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [h]
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : κ = η
a : α
f : β → ℝ≥0∞
h_1 : Measurable f
rw rw₁ : ∫⁻ (b : β), f b ∂(η : (a : α) → Measure β) a = ∫⁻ (b : β), f b ∂(η : (a : α) → Measure β) a
⊢ ∫⁻ (b : β), f b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), f b ∂(η : (a : α) → Measure β) a

Tactic:
rw [h]
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η_1 : Kernel α β
inst : IsEmpty β
κ η : Kernel α β
h :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ = η

Tactic:
ext a s
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η_1 : Kernel α β
inst : IsEmpty β
κ η : Kernel α β
a : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [Set.eq_empty_of_isEmpty s]

Premises used: Set.eq_empty_of_isEmpty
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η : Kernel α β
inst : IsEmpty α
κ : Kernel α β
⊢ ∀ (a : α), IsProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η : Kernel α β
inst : IsEmpty β
κ : Kernel α β
h : κ = 0
⊢ κ = 0 ∨ IsMarkovKernel κ

Tactic:
left
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η : Kernel α β
inst : IsEmpty β
κ : Kernel α β
h :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ = 0

Tactic:
ext a s
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η : Kernel α β
inst : IsEmpty β
κ : Kernel α β
a : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [Set.eq_empty_of_isEmpty s]

Premises used: Set.eq_empty_of_isEmpty
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Nonempty α
by_contra : ∀ (h : IsMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0), False
⊢ ¬IsMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0

Tactic:
by_contra h
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Nonempty α
h : IsMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
x : α := Nonempty.some ⋯
⊢ Eq (α := ℝ≥0∞) (((0 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
have h1 : (0 : Measure β) .univ = 1 := (h.isProbabilityMeasure x).measure_univ
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Nonempty α
h : IsMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
x : α := Nonempty.some ⋯
h1 : Eq (α := ℝ≥0∞) (((0 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ False

Tactic:
simp at h1
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
(Measure.measurable_coe hs).comp κ.measurable

Premises used: MeasureTheory.Measure.measurable_coe, Measurable.comp, ProbabilityTheory.Kernel.measurable
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
y' y : α
hy' : y' ∈ measurableAtom y
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) y' : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) y : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) y' : Measure β) ((κ : (a : α) → Measure β) y : Measure β)

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
y' y : α
hy' : y' ∈ measurableAtom y
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) y' : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) y : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
mem_of_mem_measurableAtom hy' (κ.measurable_coe hs (measurableSet_singleton (κ y s))) rfl

Premises used: MeasurableSingletonClass.measurableSet_singleton, Set.Mem, setOf, Set.preimage, Set.singleton, ProbabilityTheory.Kernel.measurable_coe, mem_of_mem_measurableAtom, DFunLike.coe, rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
y' y : α
hy' : y' ∈ measurableAtom y
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) y' : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) y : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact mem_of_mem_measurableAtom hy' (κ.measurable_coe hs (measurableSet_singleton (κ y s))) rfl

Premises used: MeasurableSingletonClass.measurableSet_singleton, ProbabilityTheory.Kernel.measurable_coe, mem_of_mem_measurableAtom, DFunLike.coe, rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsEmpty α
h₁ :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ = 0

Tactic:
ext a
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsEmpty α
a : α
s : Set β
h_1 : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
h.elim a

Premises used: IsEmpty.elim
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsEmpty α
a : α
s : Set β
h_1 : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact h.elim a
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsEmpty β
h :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ = 0

Tactic:
ext a
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsEmpty β
a : α
s : Set β
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [Measure.eq_zero_of_isEmpty (κ a)]

Premises used: MeasureTheory.Measure.eq_zero_of_isEmpty, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η : Kernel α β
inst : Countable ι
κ : ι → Kernel α β
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (a : α) ↦ Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a

Tactic:
Measure.measurable_of_measurable_coe _ fun s hs => ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η : Kernel α β
inst : Countable ι
κ : ι → Kernel α β
refine :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Measurable (β := ℝ≥0∞) fun (b : α) ↦
      ((Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (a : α) ↦ Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a

Tactic:
refine Measure.measurable_of_measurable_coe _ fun s hs => ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η : Kernel α β
inst : Countable ι
κ : ι → Kernel α β
s : Set β
hs : MeasurableSet s
simp_rw :
  Measurable (β := ℝ≥0∞) fun (b : α) ↦ ∑' (i : ι), (((κ i : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
simp_rw [Measure.sum_apply _ hs]

Premises used: MeasureTheory.Measure.sum_apply
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η : Kernel α β
inst : Countable ι
κ : ι → Kernel α β
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ ∑' (i : ι), (((κ i : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
Measurable.tsum fun n => Kernel.measurable_coe (κ n) hs

Premises used: Measurable.tsum, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η : Kernel α β
inst : Countable ι
κ : ι → Kernel α β
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ ∑' (i : ι), (((κ i : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
exact Measurable.tsum fun n => Kernel.measurable_coe (κ n) hs

Premises used: Measurable.tsum, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) ((Kernel.sum κ : (a : α) → Measure β) a : Measure β)
    (Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a : Measure β)

Tactic:
rfl

Premises used: MeasureTheory.OuterMeasure.toMeasure, MeasureTheory.Measure.ofMeasurable, MeasureTheory.Measure.sum, rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → Kernel α β
a : α
s : Set β
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ι), (((κ n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∑' (i : ι), (((κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
    (∑' (n : ι), (((κ n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞) ((((Kernel.sum κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ι), (((κ n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [sum_apply κ a, Measure.sum_apply _ hs]

Premises used: MeasureTheory.Measure.sum_apply, ProbabilityTheory.Kernel.sum_apply
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
h :
  ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((Kernel.sum fun (x : ι) ↦ 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel α β) (Kernel.sum fun (x : ι) ↦ 0) 0

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
a : α
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (∑' (n : ι), ((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((Kernel.sum fun (x : ι) ↦ 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [sum_apply' _ a hs]

Premises used: ProbabilityTheory.Kernel.sum_apply'
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (∑' (n : ι), ((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [zero_apply, Measure.coe_zero, Pi.zero_apply, tsum_zero]

Premises used: Pi.zero_apply, tsum_zero, ProbabilityTheory.Kernel.zero_apply, MeasureTheory.Measure.coe_zero
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → ι → Kernel α β
h :
  ∀ (a : α) (s : Set β),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        ((((Kernel.sum fun (n : ι) ↦ Kernel.sum (κ n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
          ℝ≥0∞)
        ((((Kernel.sum fun (m : ι) ↦ Kernel.sum fun (n : ι) ↦ κ n m : (a : α) → Measure β) a : Measure β) :
              (a : Set β) → ℝ≥0∞)
            s :
          ℝ≥0∞)
⊢ Eq (α := Kernel α β) (Kernel.sum fun (n : ι) ↦ Kernel.sum (κ n))
    (Kernel.sum fun (m : ι) ↦ Kernel.sum fun (n : ι) ↦ κ n m)

Tactic:
ext a s
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((Measure.sum fun (n : ι) ↦ Measure.sum fun (n_1 : ι) ↦ (κ n n_1 : (a : α) → Measure β) a : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((Measure.sum fun (n : ι) ↦ Measure.sum fun (n_1 : ι) ↦ (κ n_1 n : (a : α) → Measure β) a : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (n : ι) ↦ Kernel.sum (κ n) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (m : ι) ↦ Kernel.sum fun (n : ι) ↦ κ n m : (a : α) → Measure β) a : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp_rw [sum_apply]

Premises used: ProbabilityTheory.Kernel.sum_apply
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
h_1 : MeasurableSet s
h h₁ :
  Eq (α := ℝ≥0∞)
    (((Measure.sum fun (m : ι) ↦ Measure.sum fun (n : ι) ↦ (κ n m : (a : α) → Measure β) a : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((Measure.sum fun (n : ι) ↦ Measure.sum fun (n_1 : ι) ↦ (κ n_1 n : (a : α) → Measure β) a : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.sum fun (n : ι) ↦ Measure.sum fun (n_1 : ι) ↦ (κ n n_1 : (a : α) → Measure β) a : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((Measure.sum fun (n : ι) ↦ Measure.sum fun (n_1 : ι) ↦ (κ n_1 n : (a : α) → Measure β) a : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [Measure.sum_comm]

Premises used: MeasureTheory.Measure.sum_comm
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Fintype ι
κ : ι → Kernel α β
h :
  ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((Kernel.sum κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((((∑ i : ι, κ i : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Kernel.sum κ = ∑ i : ι, κ i

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Fintype ι
κ : ι → Kernel α β
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((Kernel.sum κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((((∑ i : ι, κ i : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [sum_apply' κ a hs, finsetSum_apply' _ κ a s, tsum_fintype]

Premises used: ProbabilityTheory.Kernel.finsetSum_apply', tsum_fintype, ProbabilityTheory.Kernel.sum_apply'
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ η : ι → Kernel α β
h :
  ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((Kernel.sum fun (n : ι) ↦ κ n + η n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((Kernel.sum κ + Kernel.sum η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (Kernel.sum fun (n : ι) ↦ κ n + η n) = Kernel.sum κ + Kernel.sum η

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ η : ι → Kernel α β
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (n : ι) ↦ κ n + η n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum κ + Kernel.sum η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [coe_add, Pi.add_apply, sum_apply, Measure.sum_apply _ hs, Pi.add_apply,
    Measure.coe_add, ENNReal.summable.tsum_add ENNReal.summable]

Premises used: ProbabilityTheory.Kernel.coe_add, MeasureTheory.Measure.sum_apply, ENNReal.summable, MeasureTheory.Measure.coe_add, Pi.add_apply, ProbabilityTheory.Kernel.sum_apply, Summable.tsum_add
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
n : ℕ
pos : n = 0 → IsFiniteKernel κ
neg : ¬n = 0 → IsFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
⊢ IsFiniteKernel (if n = 0 then κ else 0)

Tactic:
split_ifs
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
n : ℕ
h_1 : n = 0
⊢ IsFiniteKernel κ

Tactic:
h
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
n : ℕ
h_1 : n = 0
⊢ IsFiniteKernel κ

Tactic:
exact h
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
n : ℕ
h_1 : ¬n = 0
⊢ IsFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0

Tactic:
infer_instance