awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
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∞)
⊢ κ = Kernel.sum fun (n : ℕ) ↦ if n = 0 then κ else 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 β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
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∞)
⊢ 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:
rw [Kernel.sum_apply' _ _ 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 β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
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∞)
⊢ 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:
ext1 i
-- Module: Mathlib.Probability.Kernel.Defs
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∞)
neg :
  ¬i = 0 →
    Eq (α := ℝ≥0∞) (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥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∞)

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 κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
h_1 : i = 0
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
h_1 : ¬i = 0
⊢ Eq (α := ℝ≥0∞) (((((0 : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Defs
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

Tactic:
have : (fun i => ((ite (i = 0) κ 0) a) s) = fun i => ite (i = 0) (κ a s) 0 := by
        ext1 i; split_ifs <;> rfl
-- Module: Mathlib.Probability.Kernel.Defs
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∞)
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∞)
    (∑' (n : ℕ), (((if n = 0 then κ else 0 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [this, tsum_ite_eq]

Premises used: tsum_ite_eq, SummationFilter.unconditional
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel κ
⊢ Kernel.sum κ.seq = κ

Tactic:
h.tsum_finite.choose_spec.2.symm

Premises used: Exists.choose_spec, ProbabilityTheory.IsSFiniteKernel.tsum_finite, ProbabilityTheory.Kernel.seq, And.right, Eq.symm
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel κ
a : α
rw :
  Eq.{u_2 + 1} (α := Measure β) ((Kernel.sum κ.seq : (a : α) → Measure β) a : Measure β)
    ((κ : (a : α) → Measure β) a : Measure β)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) ((κ : (a : α) → Measure β) a : Measure β)
⊢ Eq.{u_2 + 1} (α := Measure β) (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)

Tactic:
rw [← Kernel.sum_apply, kernel_sum_seq κ]

Premises used: ProbabilityTheory.Kernel.kernel_sum_seq, ProbabilityTheory.Kernel.sum_apply
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η κ : Kernel α β
h : IsSFiniteKernel κ
n : ℕ
⊢ IsFiniteKernel (κ.seq n)

Tactic:
h.tsum_finite.choose_spec.1 n

Premises used: Exists.choose_spec, ProbabilityTheory.IsSFiniteKernel.tsum_finite, ProbabilityTheory.Kernel.seq, And.left
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsSFiniteKernel κ
a : α
⊢ SFinite.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)

Tactic:
⟨⟨fun n ↦ seq κ n a, inferInstance, (measure_sum_seq κ a).symm⟩⟩

Premises used: inferInstance, ProbabilityTheory.Kernel.seq, And.intro, MeasureTheory.SFinite.mk, Exists.intro, ProbabilityTheory.Kernel.measure_sum_seq, Eq.symm, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η_1 κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
⊢ IsSFiniteKernel (κ + η)

Tactic:
⟨⟨fun n => seq κ n + seq η n, fun n => inferInstance, ?_⟩⟩

Premises used: ProbabilityTheory.IsSFiniteKernel.mk, inferInstance, ProbabilityTheory.Kernel.seq, HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η_1 κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
refine : κ + η = Kernel.sum fun (n : ℕ) ↦ κ.seq n + η.seq n
⊢ IsSFiniteKernel (κ + η)

Tactic:
refine ⟨⟨fun n => seq κ n + seq η n, fun n => inferInstance, ?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 η_1 κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
rw : κ + η = Kernel.sum κ.seq + Kernel.sum η.seq
rw₁ : κ + η = κ + Kernel.sum η.seq
rw₂ rw₃ : κ + η = κ + η
⊢ κ + η = Kernel.sum fun (n : ℕ) ↦ κ.seq n + η.seq n

Tactic:
rw [sum_add, kernel_sum_seq κ, kernel_sum_seq η]

Premises used: ProbabilityTheory.Kernel.sum_add, ProbabilityTheory.Kernel.kernel_sum_seq
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
i : ι
I : Finset ι
hi_notMem_I : i ∉ I
h_ind :
  ∀ (h : ∀ i ∈ I, IsSFiniteKernel (κs i)),
    IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i)
h : ∀ i_1 ∈ Insert.insert i I, IsSFiniteKernel (κs i_1)
insert : IsSFiniteKernel (κs i + ∑ x ∈ I, κs x)
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ Insert.insert i I, κs i)

Tactic:
rw [Finset.sum_insert hi_notMem_I]

Premises used: Finset.sum_insert
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
i : ι
I : Finset ι
hi_notMem_I : i ∉ I
h_ind :
  ∀ (h : ∀ i ∈ I, IsSFiniteKernel (κs i)),
    IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i)
h : ∀ i_1 ∈ insert i I, IsSFiniteKernel (κs i_1)
⊢ IsSFiniteKernel (κs i)

Tactic:
haveI : IsSFiniteKernel (κs i) := h i (Finset.mem_insert_self _ _)
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
i : ι
I : Finset ι
hi_notMem_I : i ∉ I
h_ind :
  ∀ (h : ∀ i ∈ I, IsSFiniteKernel (κs i)),
    IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i)
h : ∀ i_1 ∈ insert i I, IsSFiniteKernel (κs i_1)
this : IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ x ∈ I, κs x)

Tactic:
have : IsSFiniteKernel (∑ x ∈ I, κs x) :=
      h_ind fun i hiI => h i (Finset.mem_insert_of_mem hiI)
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
i : ι
I : Finset ι
hi_notMem_I : i ∉ I
h_ind :
  ∀ (h : ∀ i ∈ I, IsSFiniteKernel (κs i)),
    IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i)
h : ∀ i_1 ∈ insert i I, IsSFiniteKernel (κs i_1)
this_1 : IsSFiniteKernel (κs i)
this : IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ x ∈ I, κs x)
⊢ IsSFiniteKernel (κs i + ∑ x ∈ I, κs x)

Tactic:
IsSFiniteKernel.add _ _

Premises used: ProbabilityTheory.Kernel.IsSFiniteKernel.add
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
i : ι
I : Finset ι
hi_notMem_I : i ∉ I
h_ind :
  ∀ (h : ∀ i ∈ I, IsSFiniteKernel (κs i)),
    IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i)
h : ∀ i_1 ∈ insert i I, IsSFiniteKernel (κs i_1)
this_1 : IsSFiniteKernel (κs i)
this : IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ x ∈ I, κs x)
⊢ IsSFiniteKernel (κs i + ∑ x ∈ I, κs x)

Tactic:
exact IsSFiniteKernel.add _ _

Premises used: ProbabilityTheory.Kernel.IsSFiniteKernel.add
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
I : Finset ι
h : ∀ i ∈ I, IsSFiniteKernel (κs i)
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsSFiniteKernel (κs i)),
    IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ ∅, κs i)
insert :
  ∀ (i : ι) (I : Finset ι) (hi_notMem_I : i ∉ I)
    (h_ind :
      ∀ (h : ∀ i ∈ I, IsSFiniteKernel (κs i)),
        IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i))
    (h : ∀ i_1 ∈ Insert.insert i I, IsSFiniteKernel (κs i_1)),
    IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ Insert.insert i I, κs i)
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i)

Tactic:
induction I using Finset.induction with
  | empty => rw [Finset.sum_empty]; infer_instance
  | insert i I hi_notMem_I h_ind =>
    rw [Finset.sum_insert hi_notMem_I]
    haveI : IsSFiniteKernel (κs i) := h i (Finset.mem_insert_self _ _)
    have : IsSFiniteKernel (∑ x ∈ I, κs x) :=
      h_ind fun i hiI => h i (Finset.mem_insert_of_mem hiI)
    exact IsSFiniteKernel.add _ _

Premises used: ProbabilityTheory.Kernel.IsSFiniteKernel.add, Insert.insert, Finset.sum_empty
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
I : Finset ι
h : ∀ i ∈ I, IsSFiniteKernel (κs i)
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsSFiniteKernel (κs i)),
    IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ ∅, κs i)
insert :
  ∀ (i : ι) (I : Finset ι) (hi_notMem_I : i ∉ I)
    (h_ind :
      ∀ (h : ∀ i ∈ I, IsSFiniteKernel (κs i)),
        IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i))
    (h : ∀ i_1 ∈ Insert.insert i I, IsSFiniteKernel (κs i_1)),
    IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ Insert.insert i I, κs i)
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i)

Tactic:
classical
  induction I using Finset.induction with
  | empty => rw [Finset.sum_empty]; infer_instance
  | insert i I hi_notMem_I h_ind =>
    rw [Finset.sum_insert hi_notMem_I]
    haveI : IsSFiniteKernel (κs i) := h i (Finset.mem_insert_self _ _)
    have : IsSFiniteKernel (∑ x ∈ I, κs x) :=
      h_ind fun i hiI => h i (Finset.mem_insert_of_mem hiI)
    exact IsSFiniteKernel.add _ _

Premises used: ProbabilityTheory.Kernel.IsSFiniteKernel.add, Insert.insert, Finset.sum_empty
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := Equiv.symm (Denumerable.eqv (ι × ℕ))
⊢ IsSFiniteKernel (Kernel.sum κs)

Tactic:
⟨⟨fun n => seq (κs (e n).1) (e n).2, inferInstance, ?_⟩⟩

Premises used: ProbabilityTheory.IsSFiniteKernel.mk, inferInstance, Prod.fst, ProbabilityTheory.Kernel.seq, And.intro, Exists.intro, Prod.snd, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := Equiv.symm (Denumerable.eqv (ι × ℕ))
refine : Kernel.sum κs = Kernel.sum fun (n : ℕ) ↦ (κs ((e : (a : ℕ) → ι × ℕ) n).1).seq ((e : (a : ℕ) → ι × ℕ) n).2
⊢ IsSFiniteKernel (Kernel.sum κs)

Tactic:
refine ⟨⟨fun n => seq (κs (e n).1) (e n).2, inferInstance, ?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := Equiv.symm (Denumerable.eqv (ι × ℕ))
⊢ Kernel.sum κs = Kernel.sum fun (n : ι) ↦ Kernel.sum (κs n).seq

Tactic:
simp_rw [kernel_sum_seq]

Premises used: ProbabilityTheory.Kernel.kernel_sum_seq
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := Equiv.symm (Denumerable.eqv (ι × ℕ))
⊢ Kernel.sum κs = Kernel.sum fun (n : ι) ↦ Kernel.sum (κs n).seq

Tactic:
have hκ_eq : Kernel.sum κs = Kernel.sum fun n => Kernel.sum (seq (κs n)) := by
    simp_rw [kernel_sum_seq]
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := Equiv.symm (Denumerable.eqv (ι × ℕ))
hκ_eq : Kernel.sum κs = Kernel.sum fun (n : ι) ↦ Kernel.sum (κs n).seq
h :
  ∀ (a : α) (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((Kernel.sum κs : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((Kernel.sum fun (n : ℕ) ↦ (κs ((e : (a : ℕ) → ι × ℕ) n).1).seq ((e : (a : ℕ) → ι × ℕ) n).2 :
                  (a : α) → Measure β)
                a :
              Measure β) :
            (a : Set β) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Kernel.sum κs = Kernel.sum fun (n : ℕ) ↦ (κs ((e : (a : ℕ) → ι × ℕ) n).1).seq ((e : (a : ℕ) → ι × ℕ) n).2

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 : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := Equiv.symm (Denumerable.eqv (ι × ℕ))
hκ_eq : Kernel.sum κs = Kernel.sum fun (n : ι) ↦ Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (n : ι) ↦ Kernel.sum (κs n).seq : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((Kernel.sum fun (n : ℕ) ↦ (κs ((e : (a : ℕ) → ι × ℕ) n).1).seq ((e : (a : ℕ) → ι × ℕ) n).2 : (a : α) → Measure β)
              a :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((Kernel.sum κs : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (n : ℕ) ↦ (κs ((e : (a : ℕ) → ι × ℕ) n).1).seq ((e : (a : ℕ) → ι × ℕ) n).2 : (a : α) → Measure β)
              a :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [hκ_eq]
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := Equiv.symm (Denumerable.eqv (ι × ℕ))
hκ_eq : Kernel.sum κs = Kernel.sum fun (n : ι) ↦ Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (∑' (n : ι) (n_1 : ℕ), ((((κs n).seq n_1 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
    (∑' (n : ℕ),
      ((((κs ((e : (a : ℕ) → ι × ℕ) n).1).seq ((e : (a : ℕ) → ι × ℕ) n).2 : (a : α) → Measure β) a : Measure β) :
          (a : Set β) → ℝ≥0∞)
        s)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum fun (n : ι) ↦ Kernel.sum (κs n).seq : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)
    ((((Kernel.sum fun (n : ℕ) ↦ (κs ((e : (a : ℕ) → ι × ℕ) n).1).seq ((e : (a : ℕ) → ι × ℕ) n).2 : (a : α) → Measure β)
              a :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp_rw [Kernel.sum_apply' _ _ 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 : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := Equiv.symm (Denumerable.eqv (ι × ℕ))
hκ_eq : Kernel.sum κs = Kernel.sum fun (n : ι) ↦ Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (∑' (i : ι) (m : ℕ), ((((κs i).seq m : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
    (∑' (b : ι × ℕ), ((((κs b.1).seq b.2 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
h₁ h₂ :
  Eq (α := ℝ≥0∞) (∑' (i : ι) (m : ℕ), ((((κs i).seq m : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
    (∑' (b : ι) (c : ℕ), ((((κs (b, c).1).seq (b, c).2 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι) (m : ℕ), ((((κs i).seq m : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
    (∑' (n : ℕ),
      (fun (im : ι × ℕ) ↦ (((((κs im.1).seq im.2 : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞))
        ((e : (a : ℕ) → ι × ℕ) n))

Tactic:
rw [e.tsum_eq (fun im : ι × ℕ => seq (κs im.fst) im.snd a s),
    ENNReal.summable.tsum_prod' fun _ => ENNReal.summable]

Premises used: Summable.tsum_prod', Equiv.tsum_eq, ENNReal.summable, Prod.fst, ProbabilityTheory.Kernel.seq, Prod.snd, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
inl : ∀ (val : Fintype ι), IsSFiniteKernel (Kernel.sum κs)
inr : Infinite ι → IsSFiniteKernel (Kernel.sum κs)
⊢ IsSFiniteKernel (Kernel.sum κs)

Tactic:
cases fintypeOrInfinite ι

Premises used: fintypeOrInfinite
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val : Fintype ι
inl : IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i : ι, κs i)
⊢ IsSFiniteKernel (Kernel.sum κs)

Tactic:
rw [sum_fintype]

Premises used: ProbabilityTheory.Kernel.sum_fintype
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val : Fintype ι
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i : ι, κs i)

Tactic:
IsSFiniteKernel.finsetSum Finset.univ fun i _ => hκs i

Premises used: Finset.univ, ProbabilityTheory.Kernel.IsSFiniteKernel.finsetSum
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val : Fintype ι
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i : ι, κs i)

Tactic:
exact IsSFiniteKernel.finsetSum Finset.univ fun i _ => hκs i

Premises used: Finset.univ, ProbabilityTheory.Kernel.IsSFiniteKernel.finsetSum
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val : Infinite ι
inr : ∀ (val : Denumerable ι), IsSFiniteKernel (Kernel.sum κs)
⊢ IsSFiniteKernel (Kernel.sum κs)

Tactic:
cases nonempty_denumerable ι

Premises used: nonempty_denumerable
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val : Infinite ι
val_1 : Denumerable ι
⊢ IsSFiniteKernel (Kernel.sum κs)

Tactic:
isSFiniteKernel_sum_of_denumerable hκs

Premises used: ProbabilityTheory.Kernel.isSFiniteKernel_sum_of_denumerable
-- Module: Mathlib.Probability.Kernel.Defs
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val : Infinite ι
val_1 : Denumerable ι
⊢ IsSFiniteKernel (Kernel.sum κs)

Tactic:
exact isSFiniteKernel_sum_of_denumerable hκs

Premises used: ProbabilityTheory.Kernel.isSFiniteKernel_sum_of_denumerable
-- Module: Mathlib.Probability.Kernel.Deterministic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsDeterministic κ
⊢ κ ∥ₖ κ ∘ₖ copy α = copy β ∘ₖ κ

Tactic:
IsDeterministic.parallelComp_self_comp_copy'

Premises used: ProbabilityTheory.IsDeterministic.parallelComp_self_comp_copy'