awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel κ
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)
have rw : Eq.{u_2 + 1} (α := Measure β) ((Kernel.sum κ.seq : (a : α) → Measure β) a : Measure β)
  ((κ : (a : α) → Measure β) a : Measure β)
Tactic: rw [← Kernel.sum_apply, kernel_sum_seq κ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
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 β)
⊢ Eq.{u_2 + 1} (α := Measure β) (Measure.sum fun (n : ℕ) ↦ (κ.seq n : (a : α) → Measure β) a)
    ((κ : (a : α) → Measure β) a)
have rw₁ : Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) ((κ : (a : α) → Measure β) a : Measure β)
Tactic: rw [← Kernel.sum_apply, kernel_sum_seq κ]
-- 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 : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
⊢ IsSFiniteKernel (κ + η)
have refine : κ + η = Kernel.sum fun (n : ℕ) ↦ κ.seq n + η.seq n
Tactic: refine ⟨⟨fun n => seq κ n + seq η n, fun n => inferInstance, ?_⟩⟩
-- 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 : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
⊢ κ + η = Kernel.sum fun (n : ℕ) ↦ κ.seq n + η.seq n
have rw : κ + η = Kernel.sum κ.seq + Kernel.sum η.seq
Tactic: rw [sum_add, kernel_sum_seq κ, kernel_sum_seq η]
-- 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 : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
rw : κ + η = Kernel.sum κ.seq + Kernel.sum η.seq
⊢ κ + η = Kernel.sum fun (n : ℕ) ↦ κ.seq n + η.seq n
have rw₁ : κ + η = κ + Kernel.sum η.seq
Tactic: rw [sum_add, kernel_sum_seq κ, kernel_sum_seq η]
-- 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 : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
rw : κ + η = Kernel.sum κ.seq + Kernel.sum η.seq
rw₁ : κ + η = κ + Kernel.sum η.seq
⊢ κ + η = Kernel.sum fun (n : ℕ) ↦ κ.seq n + η.seq n
have rw₂ : κ + η = κ + η
Tactic: rw [sum_add, kernel_sum_seq κ, kernel_sum_seq η]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
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.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ insert i I, κs i)
have insert : IsSFiniteKernel (κs i + ∑ x ∈ I, κs x)
Tactic: rw [Finset.sum_insert hi_notMem_I]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (hypothesis)
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 + ∑ x ∈ I, κs x)
have this : IsSFiniteKernel (κs i)
Tactic: haveI : IsSFiniteKernel (κs i) := h i (Finset.mem_insert_self _ _)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (hypothesis)
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 (κs i + ∑ x ∈ I, κs x)
have this₁ : 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)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
I : Finset ι
h : ∀ i ∈ I, IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i)
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsSFiniteKernel (κs i)),
  IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ 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 _ _
Cleared hypotheses: I, 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 β
κ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)
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i)
have 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 i I, IsSFiniteKernel (κs i_1)),
  IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ insert 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 _ _
Cleared hypotheses: I, 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 β
κs : ι → Kernel α β
I : Finset ι
h : ∀ i ∈ I, IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i)
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsSFiniteKernel (κs i)),
  IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ 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 _ _
Cleared hypotheses: I, 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 β
κ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)
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ I, κs i)
have 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 i I, IsSFiniteKernel (κs i_1)),
  IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i ∈ insert 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 _ _
Cleared hypotheses: I, 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 β
inst : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := Equiv.symm (Denumerable.eqv (ι × ℕ))
⊢ IsSFiniteKernel (Kernel.sum κs)
have refine : Kernel.sum κs = Kernel.sum fun (n : ℕ) ↦ (κs ((e : (a : ℕ) → ι × ℕ) n).1).seq ((e : (a : ℕ) → ι × ℕ) n).2
Tactic: refine ⟨⟨fun n => seq (κs (e n).1) (e n).2, inferInstance, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (hypothesis)
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 : ℕ) ↦ (κs ((e : (a : ℕ) → ι × ℕ) n).1).seq ((e : (a : ℕ) → ι × ℕ) n).2
have hκ_eq : 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]
-- 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 : 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
⊢ Kernel.sum κs = Kernel.sum fun (n : ℕ) ↦ (κs ((e : (a : ℕ) → ι × ℕ) n).1).seq ((e : (a : ℕ) → ι × ℕ) n).2
have 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∞)
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 : 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
⊢ 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∞)
have 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∞)
Tactic: rw [hκ_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 β
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
⊢ 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∞)
have 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)
Tactic: simp_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 β
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
⊢ 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))
have 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)
Tactic: rw [e.tsum_eq (fun im : ι × ℕ => seq (κs im.fst) im.snd a s),
    ENNReal.summable.tsum_prod' fun _ => ENNReal.summable]
-- 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 : 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)
⊢ 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))
have 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)
Tactic: rw [e.tsum_eq (fun im : ι × ℕ => seq (κs im.fst) im.snd a s),
    ENNReal.summable.tsum_prod' fun _ => ENNReal.summable]
-- 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 : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
⊢ IsSFiniteKernel (Kernel.sum κs)
have inl : ∀ (val : Fintype ι), IsSFiniteKernel (Kernel.sum κs)
Tactic: cases fintypeOrInfinite ι
-- 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 : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
inl : ∀ (val : Fintype ι), IsSFiniteKernel (Kernel.sum κs)
⊢ IsSFiniteKernel (Kernel.sum κs)
have inr : Infinite ι → IsSFiniteKernel (Kernel.sum κs)
Tactic: cases fintypeOrInfinite ι
-- 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 : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val : Fintype ι
⊢ IsSFiniteKernel (Kernel.sum κs)
have inl : IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) (∑ i : ι, κs i)
Tactic: rw [sum_fintype]
-- 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 : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val : Infinite ι
⊢ IsSFiniteKernel (Kernel.sum κs)
have inr : ∀ (val : Denumerable ι), IsSFiniteKernel (Kernel.sum κs)
Tactic: cases nonempty_denumerable ι
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ deterministic f hf ∥ₖ deterministic f hf ∘ₖ copy α = copy β ∘ₖ deterministic f hf
have simp_rw : deterministic f hf ×ₖ deterministic f hf = copy β ∘ₖ deterministic f hf
Tactic: simp_rw [parallelComp_comp_copy, deterministic_prod_deterministic, copy,
      deterministic_comp_deterministic, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
simp_rw : deterministic f hf ×ₖ deterministic f hf = copy β ∘ₖ deterministic f hf
⊢ deterministic f hf ∥ₖ deterministic f hf ∘ₖ copy α = copy β ∘ₖ deterministic f hf
have simp_rw₁ : deterministic (fun (a : α) ↦ (f a, f a)) sorry = copy β ∘ₖ deterministic f hf
Tactic: simp_rw [parallelComp_comp_copy, deterministic_prod_deterministic, copy,
      deterministic_comp_deterministic, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
simp_rw : deterministic f hf ×ₖ deterministic f hf = copy β ∘ₖ deterministic f hf
simp_rw₁ : deterministic (fun (a : α) ↦ (f a, f a)) ⋯ = copy β ∘ₖ deterministic f hf
⊢ deterministic f hf ∥ₖ deterministic f hf ∘ₖ copy α = copy β ∘ₖ deterministic f hf
have simp_rw₂ : deterministic (fun (a : α) ↦ (f a, f a)) sorry = deterministic (fun (x : β) ↦ (x, x)) sorry ∘ₖ deterministic f hf
Tactic: simp_rw [parallelComp_comp_copy, deterministic_prod_deterministic, copy,
      deterministic_comp_deterministic, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
simp_rw : deterministic f hf ×ₖ deterministic f hf = copy β ∘ₖ deterministic f hf
simp_rw₁ : deterministic (fun (a : α) ↦ (f a, f a)) ⋯ = copy β ∘ₖ deterministic f hf
simp_rw₂ : deterministic (fun (a : α) ↦ (f a, f a)) ⋯ = deterministic (fun (x : β) ↦ (x, x)) ⋯ ∘ₖ deterministic f hf
⊢ deterministic f hf ∥ₖ deterministic f hf ∘ₖ copy α = copy β ∘ₖ deterministic f hf
have simp_rw₃ : deterministic (fun (a : α) ↦ (f a, f a)) sorry = deterministic ((fun (x : β) ↦ (x, x)) ∘ f) sorry
Tactic: simp_rw [parallelComp_comp_copy, deterministic_prod_deterministic, copy,
      deterministic_comp_deterministic, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
⊢ IsDeterministic κ ↔ ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
have mp : IsDeterministic κ → ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
mp : IsDeterministic κ → ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
⊢ IsDeterministic κ ↔ ∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
have mpr : (∀ (a : α), IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)) → IsDeterministic κ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
⊢ IsZeroOneMeasure.{u_2} (α := β) (mα := mβ) ((κ : (a : α) → Measure β) a)
have mp : ∀ (s : Set β) (hs : MeasurableSet s),
  Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)
Tactic: refine ⟨fun s hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)
have this : Eq (α := ENNReal)
  ((((κ ∥ₖ κ ∘ₖ copy α : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ENNReal) (s ×ˢ s) :
    ENNReal)
  ((((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ENNReal) (s ×ˢ s) : ENNReal)
Tactic: have := DFunLike.congr_fun κ.parallelComp_self_comp_copy a |> DFunLike.congr_fun
      <| (s ×ˢ s)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Deterministic (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this :
  Eq (α := ENNReal)
    ((((κ ∥ₖ κ ∘ₖ copy α : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ENNReal) (s ×ˢ s) :
      ENNReal)
    ((((copy β ∘ₖ κ : (a : α) → Measure (β × β)) a : Measure (β × β)) : (a : Set (β × β)) → ENNReal) (s ×ˢ s) : ENNReal)
⊢ Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)
have mp : ∀
  (this :
    HMul.hMul (α := ENNReal) (β := ENNReal)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal)
        ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) =
      (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s),
  Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ENNReal) s : ENNReal) (1 : ENNReal)
Tactic: rw [parallelComp_comp_copy, prod_apply_prod, copy_comp_apply_prod, inter_self] at this
Cleared hypotheses: this