awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ i ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have pos₁ : ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(Kernel.sum κ : (a : α) → Measure β) a =
  (Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s
Tactic: simp_rw [sum_apply, compProd_apply hs, sum_apply, lintegral_sum_measure, Measure.sum_apply _ hs,
    compProd_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
pos₁ :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(Kernel.sum κ : (a : α) → Measure β) a =
    (Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ i ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have pos₂ : (∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a) =
  (Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s
Tactic: simp_rw [sum_apply, compProd_apply hs, sum_apply, lintegral_sum_measure, Measure.sum_apply _ hs,
    compProd_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
pos₁ :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(Kernel.sum κ : (a : α) → Measure β) a =
    (Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s
pos₂ :
  (∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a) =
    (Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ i ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have pos₃ : Eq (α := ℝ≥0∞)
  (∑' (i : ι),
      ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(κ i : (a : α) → Measure β) a :
    ℝ≥0∞)
  ((Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [sum_apply, compProd_apply hs, sum_apply, lintegral_sum_measure, Measure.sum_apply _ hs,
    compProd_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
pos₁ :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(Kernel.sum κ : (a : α) → Measure β) a =
    (Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s
pos₂ :
  (∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂Measure.sum fun (n : ι) ↦ (κ n : (a : α) → Measure β) a) =
    (Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s
pos₃ :
  Eq (α := ℝ≥0∞)
    (∑' (i : ι),
        ∫⁻ (b : β),
          (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (Prod.mk b ⁻¹' s) ∂(κ i : (a : α) → Measure β) a :
      ℝ≥0∞)
    ((Measure.sum fun (n : ι) ↦ (κ n ⊗ₖ η : (a : α) → Measure (β × γ)) a : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.sum κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ i ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have pos₄ : Eq (α := ℝ≥0∞)
  (∑' (i : ι),
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ i : (a : α) → Measure β) a)
  (∑' (i : ι), (((κ i ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s)
Tactic: simp_rw [sum_apply, compProd_apply hs, sum_apply, lintegral_sum_measure, Measure.sum_apply _ hs,
    compProd_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
⊢ κ ⊗ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i
have pos : ∀ (hκ : IsSFiniteKernel κ), κ ⊗ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
pos : ∀ (hκ : IsSFiniteKernel κ), κ ⊗ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i
⊢ κ ⊗ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i
have neg : ∀ (hκ : ¬IsSFiniteKernel κ), κ ⊗ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
⊢ κ ⊗ₖ Kernel.sum η = Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i
have pos : ∀ (a : α) (s : Set (β × γ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ Kernel.sum η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ Kernel.sum η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((Kernel.sum fun (i : ι) ↦ κ ⊗ₖ η i : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have pos : ∫⁻ (b : β),
    ((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
  ∑' (i : ι),
    ∫⁻ (b : β),
      (((η i : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [sum_apply, compProd_apply hs, Measure.sum_apply _ hs, sum_apply, compProd_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β),
      ((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∑' (i : ι),
      ∫⁻ (b : β),
        (((η i : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
have pos : ∫⁻ (b : β),
    ((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (a_1 : β),
    ∑' (i : ι),
      (((η i : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a
Tactic: rw [← lintegral_tsum]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  ∫⁻ (b : β),
      ((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (a_1 : β),
      ∑' (i : ι),
        (((η i : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (b : β),
      ((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∑' (i : ι),
      ∫⁻ (b : β),
        (((η i : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a
have pos₁ : ∀ (i : ι),
  AEMeasurable (β := ℝ≥0∞) (_m := mβ)
    (fun (b : β) ↦ (((η i : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)
Tactic: rw [← lintegral_tsum]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β),
      ((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (a_1 : β),
      ∑' (i : ι),
        (((η i : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk a_1 ⁻¹' s) ∂(κ : (a : α) → Measure β) a
have pos : ∀ (i : β),
  Eq (α := ℝ≥0∞)
    (((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, i) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk i ⁻¹' s) :
      ℝ≥0∞)
    (∑' (i_1 : ι), (((η i_1 : (a : α × β) → Measure γ) (a, i) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk i ⁻¹' s) :
      ℝ≥0∞)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst_1 : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
i : β
⊢ Eq (α := ℝ≥0∞)
    (((Measure.sum fun (n : ι) ↦ (η n : (a : α × β) → Measure γ) (a, i) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk i ⁻¹' s) :
      ℝ≥0∞)
    (∑' (i_1 : ι), (((η i_1 : (a : α × β) → Measure γ) (a, i) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk i ⁻¹' s) :
      ℝ≥0∞)
have pos : MeasurableSet (Prod.mk i ⁻¹' s)
Tactic: rw [Measure.sum_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
⊢ (κ ⊗ₖ η).comapRight ⋯ = κ ⊗ₖ η.comapRight hf
have h : ∀ (a : α) (t : Set (β × δ)) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞)
    (((((κ ⊗ₖ η).comapRight sorry : (a : α) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ ⊗ₖ η.comapRight hf : (a : α) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: ext a t ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞)
    (((((κ ⊗ₖ η).comapRight ⋯ : (a : α) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ ⊗ₖ η.comapRight hf : (a : α) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) t : ℝ≥0∞)
have h : ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' Prod.map id f '' t) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (b : β),
    (((η.comapRight hf : (a : α × β) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' t) ∂(κ : (a : α) → Measure β) a
Tactic: rw [comapRight_apply' _ _ _ ht, compProd_apply, compProd_apply ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
h :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Prod.map id f '' t) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η.comapRight hf : (a : α × β) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(κ : (a : α) → Measure β) a
⊢ Eq (α := ℝ≥0∞)
    (((((κ ⊗ₖ η).comapRight ⋯ : (a : α) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ ⊗ₖ η.comapRight hf : (a : α) → Measure (β × δ)) a : Measure (β × δ)) : (a : Set (β × δ)) → ℝ≥0∞) t : ℝ≥0∞)
have h₁ : MeasurableSet (Prod.map id f '' t)
Tactic: rw [comapRight_apply' _ _ _ ht, compProd_apply, compProd_apply ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Prod.map id f '' t) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((η.comapRight hf : (a : α × β) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(κ : (a : α) → Measure β) a
have h : ∀ (b : β),
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' Prod.map id f '' t) :
      ℝ≥0∞)
    ((((η.comapRight hf : (a : α × β) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' t) : ℝ≥0∞)
Tactic: refine lintegral_congr fun b ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
b : β
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' Prod.map id f '' t) :
      ℝ≥0∞)
    ((((η.comapRight hf : (a : α × β) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' t) : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' Prod.map id f '' t) : ℝ≥0∞)
  ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (f '' Prod.mk b ⁻¹' t) : ℝ≥0∞)
Tactic: rw [comapRight_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
b : β
h :
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' Prod.map id f '' t) :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (f '' Prod.mk b ⁻¹' t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' Prod.map id f '' t) :
      ℝ≥0∞)
    ((((η.comapRight hf : (a : α × β) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' t) : ℝ≥0∞)
have h₁ : MeasurableSet (Prod.mk b ⁻¹' t)
Tactic: rw [comapRight_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
f : δ → γ
hf : MeasurableEmbedding f
a : α
t : Set (β × δ)
ht : MeasurableSet t
b : β
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' Prod.map id f '' t) :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (f '' Prod.mk b ⁻¹' t) : ℝ≥0∞)
have h : ∀ (x : γ), x ∈ Prod.mk b ⁻¹' Prod.map id f '' t ↔ x ∈ f '' Prod.mk b ⁻¹' t
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
⊢ ((((κ ⊗ₖ η).fst : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
        b ∂(κ : (a : α) → Measure β) x
have rw : ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' {p : β × γ | p.1 ∈ s}) ∂(κ : (a : α) → Measure β) x =
  ∫⁻ (b : β),
    s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
      b ∂(κ : (a : α) → Measure β) x
Tactic: rw [Kernel.fst_apply' _ _ hs, Kernel.compProd_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
rw :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' {p : β × γ | p.1 ∈ s}) ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
        b ∂(κ : (a : α) → Measure β) x
⊢ ((((κ ⊗ₖ η).fst : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s =
    ∫⁻ (b : β),
      s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ)
        b ∂(κ : (a : α) → Measure β) x
have hs₁ : MeasurableSet (α := β × γ) {p : β × γ | p.1 ∈ s}
Tactic: rw [Kernel.fst_apply' _ _ hs, Kernel.compProd_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
x : α
s : Set β
hs : MeasurableSet s
b : β
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | b ∈ s} : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ) b :
      ℝ≥0∞)
have pos : ∀ (hb : b ∈ s),
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | b ∈ s} : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ) b :
      ℝ≥0∞)
Tactic: by_cases hb : b ∈ s