awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsZeroOrMarkovKernel κ
a : α
inl :
  ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) (((0 : Kernel α β) : (a : α) → Measure β) a)
⊢ IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
have inr : ∀ (h' : IsMarkovKernel κ), IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
Tactic: rcases eq_zero_or_isMarkovKernel κ with rfl | h'
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsZeroOrMarkovKernel κ
⊢ IsFiniteKernel κ
have inl : ∀ [h : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
  IsFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
Tactic: rcases eq_zero_or_isMarkovKernel κ with rfl | _h'
Cleared hypotheses: κ, h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsZeroOrMarkovKernel κ
inl :
  ∀ [h : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    IsFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
⊢ IsFiniteKernel κ
have inr : ∀ (_h' : IsMarkovKernel κ), IsFiniteKernel κ
Tactic: rcases eq_zero_or_isMarkovKernel κ with rfl | _h'
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
⊢ κ.bound ≤ 1
have inl : IsEmpty α → κ.bound ≤ 1
Tactic: rcases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
inl : IsEmpty α → κ.bound ≤ 1
⊢ κ.bound ≤ 1
have inr : Nonempty α → κ.bound ≤ 1
Tactic: rcases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
h : Nonempty α
⊢ κ.bound ≤ 1
have inr : ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
  bound.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0 ≤ 1
Tactic: rcases eq_zero_or_isMarkovKernel κ with rfl | _
Cleared hypotheses: κ, inst
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsZeroOrMarkovKernel κ
h : Nonempty α
inr :
  ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
    bound.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0 ≤ 1
⊢ κ.bound ≤ 1
have inr₁ : IsMarkovKernel κ → κ.bound ≤ 1
Tactic: rcases eq_zero_or_isMarkovKernel κ with rfl | _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
⊢ κ = η ↔
    ∀ (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∞)
have 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∞)
Tactic: simp_rw [Kernel.ext_iff, Measure.ext_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
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
⊢ κ = η
have 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (hypothesis)
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
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∫⁻ (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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((((η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : κ = η
a : α
f : β → ℝ≥0∞
h_1 : Measurable f
⊢ ∫⁻ (b : β), f b ∂(κ : (a : α) → Measure β) a = ∫⁻ (b : β), f b ∂(η : (a : α) → Measure β) a
have rw : ∫⁻ (b : β), f b ∂(η : (a : α) → Measure β) a = ∫⁻ (b : β), f b ∂(η : (a : α) → Measure β) a
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η_1 : Kernel α β
inst : IsEmpty β
κ η : Kernel α β
⊢ κ = η
have 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η : Kernel α β
inst : IsEmpty β
κ : Kernel α β
⊢ κ = 0 ∨ IsMarkovKernel κ
have h : κ = 0
Tactic: left
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η : Kernel α β
inst : IsEmpty β
κ : Kernel α β
⊢ κ = 0
have 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∞)
Tactic: ext a s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (hypothesis)
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 ⋯
⊢ False
have h1 : Eq (α := ℝ≥0∞) (((0 : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: have h1 : (0 : Measure β) .univ = 1 := (h.isProbabilityMeasure x).measure_univ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
y' y : α
hy' : y' ∈ measurableAtom y
⊢ Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) y' : Measure β) ((κ : (a : α) → Measure β) y : Measure β)
have 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∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsEmpty α
⊢ κ = 0
have 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∞)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsEmpty β
⊢ κ = 0
have 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∞)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
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
have refine : ∀ (s : Set β) (hs : MeasurableSet s),
  Measurable (β := ℝ≥0∞) fun (b : α) ↦
    ((Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s
Tactic: refine Measure.measurable_of_measurable_coe _ fun s hs => ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
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 : α) ↦
    ((Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s
have simp_rw : Measurable (β := ℝ≥0∞) fun (b : α) ↦ ∑' (i : ι), (((κ i : (a : α) → Measure β) b : Measure β) : (a : Set β) → ℝ≥0∞) s
Tactic: simp_rw [Measure.sum_apply _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
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 κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ι), (((κ n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: rw [sum_apply κ a, Measure.sum_apply _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((((Kernel.sum κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ι), (((κ n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (∑' (i : ι), (((κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
  (∑' (n : ι), (((κ n : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
Tactic: rw [sum_apply κ a, Measure.sum_apply _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
⊢ Eq (α := Kernel α β) (Kernel.sum fun (x : ι) ↦ 0) 0
have 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∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
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∞)
have 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∞)
Tactic: rw [sum_apply' _ a hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → ι → Kernel α β
⊢ Eq (α := Kernel α β) (Kernel.sum fun (n : ι) ↦ Kernel.sum (κ n))
    (Kernel.sum fun (m : ι) ↦ Kernel.sum fun (n : ι) ↦ κ n m)
have 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∞)
Tactic: ext a s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
h : 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∞)
have 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∞)
Tactic: simp_rw [sum_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
h : MeasurableSet s
⊢ 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∞)
have 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∞)
Tactic: rw [Measure.sum_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Fintype ι
κ : ι → Kernel α β
⊢ Kernel.sum κ = ∑ i : ι, κ i
have 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∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
κ η : ι → Kernel α β
⊢ (Kernel.sum fun (n : ι) ↦ κ n + η n) = Kernel.sum κ + Kernel.sum η
have 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∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
n : ℕ
⊢ IsFiniteKernel (if n = 0 then κ else 0)
have pos : n = 0 → IsFiniteKernel κ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
n : ℕ
pos : n = 0 → IsFiniteKernel κ
⊢ IsFiniteKernel (if n = 0 then κ else 0)
have neg : ¬n = 0 → IsFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
⊢ κ = Kernel.sum fun (n : ℕ) ↦ if n = 0 then κ else 0
have h₁ : ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (n : ℕ) ↦ if n = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (n : ℕ) ↦ if n = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  (∑' (n : ℕ), (((if n = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Kernel.sum_apply' _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := (i : ℕ) → ℝ≥0∞)
    (fun (i : ℕ) ↦ (((if i = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
    fun (i : ℕ) ↦ if i = 0 then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s else 0
have h₁ : ∀ (i : ℕ),
  Eq (α := ℝ≥0∞) ((((if i = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (if i = 0 then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s else 0 : ℝ≥0∞)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
⊢ Eq (α := ℝ≥0∞) ((((if i = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (if i = 0 then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s else 0 : ℝ≥0∞)
have pos : i = 0 →
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
pos :
  i = 0 →
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((if i = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (if i = 0 then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s else 0 : ℝ≥0∞)
have neg : ¬i = 0 →
  Eq (α := ℝ≥0∞) (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (((if n = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have this : Eq (α := (i : ℕ) → ℝ≥0∞)
  (fun (i : ℕ) ↦ (((if i = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s) fun (i : ℕ) ↦
  if i = 0 then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s else 0
Tactic: have : (fun i => ((ite (i = 0) κ 0) a) s) = fun i => ite (i = 0) (κ a s) 0 := by
        ext1 i; split_ifs <;> rfl
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
this :
  Eq (α := (i : ℕ) → ℝ≥0∞)
    (fun (i : ℕ) ↦ (((if i = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
    fun (i : ℕ) ↦ if i = 0 then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s else 0
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (((if n = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  (∑' (i : ℕ), if i = 0 then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s else 0 : ℝ≥0∞)
Tactic: rw [this, tsum_ite_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
this :
  Eq (α := (i : ℕ) → ℝ≥0∞)
    (fun (i : ℕ) ↦ (((if i = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
    fun (i : ℕ) ↦ if i = 0 then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s else 0
h₁ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (i : ℕ), if i = 0 then (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s else 0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (((if n = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [this, tsum_ite_eq]