awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ Kernel.const α ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (a : α),
    ((((Kernel.const α ν : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
      (Prod.mk a ⁻¹' s) ∂μ =
  (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s
Tactic: simp_rw [compProd_apply hs, prod_apply hs, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h :
  ∫⁻ (a : α),
      ((((Kernel.const α ν : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        (Prod.mk a ⁻¹' s) ∂μ =
    (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ Kernel.const α ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∫⁻ (a : α),
    ((((Kernel.const α ν : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
      (Prod.mk a ⁻¹' s) ∂μ =
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ
Tactic: simp_rw [compProd_apply hs, prod_apply hs, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α β
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
have pos : ∀ (hκ : IsSFiniteKernel κ), (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α β
pos : ∀ (hκ : IsSFiniteKernel κ), (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
have neg : ∀ (hκ : ¬IsSFiniteKernel κ), (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
have pos : (Kernel.const Unit (μ + ν) ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () =
  HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
    ((Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
Tactic: simp_rw [Measure.compProd, Kernel.const_add, Kernel.compProd_add_left, Kernel.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
pos :
  (Kernel.const Unit (μ + ν) ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () =
    HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
      ((Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
have pos₁ : (HAdd.hAdd (α := Kernel Unit α) (Kernel.const Unit μ) (Kernel.const Unit ν) ⊗ₖ Kernel.prodMkLeft Unit κ :
      (a : Unit) → Measure (α × β))
    () =
  HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
    ((Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
Tactic: simp_rw [Measure.compProd, Kernel.const_add, Kernel.compProd_add_left, Kernel.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
pos :
  (Kernel.const Unit (μ + ν) ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () =
    HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
      ((Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
pos₁ :
  (HAdd.hAdd (α := Kernel Unit α) (Kernel.const Unit μ) (Kernel.const Unit ν) ⊗ₖ Kernel.prodMkLeft Unit κ :
        (a : Unit) → Measure (α × β))
      () =
    HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
      ((Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
have pos₂ : (HAdd.hAdd (α := Kernel Unit (α × β)) (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ)
        (Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ) :
      (a : Unit) → Measure (α × β))
    () =
  HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
    ((Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
Tactic: simp_rw [Measure.compProd, Kernel.const_add, Kernel.compProd_add_left, Kernel.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
have pos : ∀ (hμ : SFinite μ), μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
Tactic: by_cases hμ : SFinite μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
pos : ∀ (hμ : SFinite μ), μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
have neg : ∀ (hμ : ¬SFinite μ), μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
Tactic: by_cases hμ : SFinite μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
hμ : SFinite μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
have pos : (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (κ + η) : (a : Unit) → Measure (α × β)) () =
  HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η : (a : Unit) → Measure (α × β)) () : Measure (α × β))
Tactic: simp_rw [Measure.compProd, Kernel.prodMkLeft_add, Kernel.compProd_add_right, Kernel.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
hμ : SFinite μ
pos :
  (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (κ + η) : (a : Unit) → Measure (α × β)) () =
    HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η : (a : Unit) → Measure (α × β)) () : Measure (α × β))
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
have pos₁ : (Kernel.const Unit μ ⊗ₖ
        HAdd.hAdd (α := Kernel.{u_1, u_2} (Unit × α) β) (Kernel.prodMkLeft Unit κ) (Kernel.prodMkLeft Unit η) :
      (a : Unit) → Measure (α × β))
    () =
  HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η : (a : Unit) → Measure (α × β)) () : Measure (α × β))
Tactic: simp_rw [Measure.compProd, Kernel.prodMkLeft_add, Kernel.compProd_add_right, Kernel.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
hμ : SFinite μ
pos :
  (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (κ + η) : (a : Unit) → Measure (α × β)) () =
    HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η : (a : Unit) → Measure (α × β)) () : Measure (α × β))
pos₁ :
  (Kernel.const Unit μ ⊗ₖ
          HAdd.hAdd (α := Kernel.{u_1, u_2} (Unit × α) β) (Kernel.prodMkLeft Unit κ) (Kernel.prodMkLeft Unit η) :
        (a : Unit) → Measure (α × β))
      () =
    HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
      ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η : (a : Unit) → Measure (α × β)) () : Measure (α × β))
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η
have pos₂ : (HAdd.hAdd (α := Kernel Unit (α × β)) (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ)
        (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η) :
      (a : Unit) → Measure (α × β))
    () =
  HAdd.hAdd (α := Measure (α × β)) (β := Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η : (a : Unit) → Measure (α × β)) () : Measure (α × β))
Tactic: simp_rw [Measure.compProd, Kernel.prodMkLeft_add, Kernel.compProd_add_right, Kernel.add_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
ι : Type u_3
inst : Countable ι
μ : ι → Measure α
inst_1 : ∀ (i : ι), SFinite (μ i)
⊢ sum μ ⊗ₘ κ = sum fun (i : ι) ↦ μ i ⊗ₘ κ
have rw : Eq (α := Measure (α × β))
  ((Kernel.sum fun (i : ι) ↦ Kernel.const Unit (μ i) ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () :
    Measure (α × β))
  (sum fun (i : ι) ↦ μ i ⊗ₘ κ : Measure (α × β))
Tactic: rw [compProd, ← Kernel.sum_const, Kernel.compProd_sum_left]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ι : Type u_3
inst : Countable ι
κ : ι → Kernel α β
h : ∀ (i : ι), IsSFiniteKernel (κ i)
⊢ μ ⊗ₘ Kernel.sum κ = sum fun (i : ι) ↦ μ ⊗ₘ κ i
have rw : Eq (α := Measure (α × β))
  ((Kernel.sum fun (i : ι) ↦ Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (κ i) : (a : Unit) → Measure (α × β)) () :
    Measure (α × β))
  (sum fun (i : ι) ↦ μ ⊗ₘ κ i : Measure (α × β))
Tactic: rw [compProd, ← Kernel.sum_prodMkLeft, Kernel.compProd_sum_right]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsMarkovKernel κ
⊢ (μ ⊗ₘ κ).fst = μ
have h : ∀ (s : Set α),
  MeasurableSet s → Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsMarkovKernel κ
s : Set α
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  (((fst.{u_1, u_2} (β := β) ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) :
          Measure α) :
        (a : Set α) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [compProd, Measure.fst, ← Kernel.fst_apply, Kernel.fst_compProd, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsMarkovKernel κ
s : Set α
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((fst.{u_1, u_2} (β := β) ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞)
  (((map (α := α × β) Prod.fst ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) :
          Measure α) :
        (a : Set α) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [compProd, Measure.fst, ← Kernel.fst_apply, Kernel.fst_compProd, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsMarkovKernel κ
s : Set α
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((fst.{u_1, u_2} (β := β) ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    (((map (α := α × β) Prod.fst ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞)
  ((((Kernel.fst (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) : (a : Unit) → Measure α) () : Measure α) :
        (a : Set α) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [compProd, Measure.fst, ← Kernel.fst_apply, Kernel.fst_compProd, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsMarkovKernel κ
s : Set α
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((fst.{u_1, u_2} (β := β) ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    (((map (α := α × β) Prod.fst ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞)
    ((((Kernel.fst (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) : (a : Unit) → Measure α) () : Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) ((((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [compProd, Measure.fst, ← Kernel.fst_apply, Kernel.fst_compProd, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst : SFinite μ
κ : Kernel α β
inst_1 : IsMarkovKernel κ
s : Set α
h_1 : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((fst.{u_1, u_2} (β := β) ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    (((map (α := α × β) Prod.fst ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) ()) :
            Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞)
    ((((Kernel.fst (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) : (a : Unit) → Measure α) () : Measure α) :
          (a : Set α) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₃ :
  Eq (α := ℝ≥0∞) ((((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ ⊗ₘ κ).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [compProd, Measure.fst, ← Kernel.fst_apply, Kernel.fst_compProd, Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
a : ℝ≥0∞
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
⊢ (a • μ) ⊗ₘ κ = a • μ ⊗ₘ κ
have h : ∀ (s : Set (α × β)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((a • μ) ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((a • μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : α × β), f x ∂μ ⊗ₘ κ = ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a ∂μ
have rw : ∫⁻ (b : α),
    ∫⁻ (c : β),
      f
        (b,
          c) ∂((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β)
        ((), b) ∂(Kernel.const Unit μ : (a : Unit) → Measure α) () =
  ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂(κ : (a : α) → Measure β) a ∂μ
Tactic: rw [compProd, Kernel.lintegral_compProd _ _ _ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
⊢ ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂(κ : (a : α) → Measure β) a ∂μ
have rw : ∫⁻ (x : α) in s,
    ∫⁻ (y : β) in t,
      f
        (x,
          y) ∂((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β)
        ((), x) ∂(Kernel.const Unit μ : (a : Unit) → Measure α) () =
  ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂(κ : (a : α) → Measure β) a ∂μ
Tactic: rw [compProd, Kernel.setLIntegral_compProd _ _ _ hf hs ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : MeasurableSingletonClass α
a : α
inst_1 : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((dirac a ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
have rw : ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂dirac a =
  (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)
Tactic: rw [compProd_apply hs, lintegral_dirac]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst : MeasurableSingletonClass α
a : α
inst_1 : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
rw :
  ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂dirac a =
    (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) ((dirac a ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
Tactic: rw [compProd_apply hs, lintegral_dirac]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
κ : Kernel Unit β
inst : IsSFiniteKernel κ
⊢ dirac () ⊗ₘ κ = map (Prod.mk ()) ((κ : (a : Unit) → Measure β) ())
have h : ∀ (s : Set (Unit × β)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((dirac () ⊗ₘ κ : (a : Set (Unit × β)) → ℝ≥0∞) s : ℝ≥0∞)
    (((map (Prod.mk ()) ((κ : (a : Unit) → Measure β) ()) : Measure (Unit × β)) : (a : Set (Unit × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
κ : Kernel Unit β
inst : IsSFiniteKernel κ
s : Set (Unit × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((dirac () ⊗ₘ κ : (a : Set (Unit × β)) → ℝ≥0∞) s : ℝ≥0∞)
    (((map (Prod.mk ()) ((κ : (a : Unit) → Measure β) ()) : Measure (Unit × β)) : (a : Set (Unit × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((((κ : (a : Unit) → Measure β) () : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk () ⁻¹' s) : ℝ≥0∞)
  (((map (Prod.mk ()) ((κ : (a : Unit) → Measure β) ()) : Measure (Unit × β)) : (a : Set (Unit × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [dirac_compProd_apply hs, Measure.map_apply measurable_prodMk_left hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
κ : Kernel Unit β
inst : IsSFiniteKernel κ
s : Set (Unit × β)
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((((κ : (a : Unit) → Measure β) () : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk () ⁻¹' s) : ℝ≥0∞)
    (((map (Prod.mk ()) ((κ : (a : Unit) → Measure β) ()) : Measure (Unit × β)) : (a : Set (Unit × β)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((dirac () ⊗ₘ κ : (a : Set (Unit × β)) → ℝ≥0∞) s : ℝ≥0∞)
    (((map (Prod.mk ()) ((κ : (a : Unit) → Measure β) ()) : Measure (Unit × β)) : (a : Set (Unit × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((((κ : (a : Unit) → Measure β) () : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk () ⁻¹' s) : ℝ≥0∞)
  ((((κ : (a : Unit) → Measure β) () : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk () ⁻¹' s) : ℝ≥0∞)
Tactic: rw [dirac_compProd_apply hs, Measure.map_apply measurable_prodMk_left hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.MeasureCompProd (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
inst : SFinite μ
⊢ Eq (α := Measure (Unit × β)) (dirac () ⊗ₘ Kernel.const Unit μ) (map (Prod.mk ()) μ)
have rw : Eq (α := Measure (Unit × β)) (map (Prod.mk ()) ((Kernel.const Unit μ : (a : Unit) → Measure β) ())) (map (Prod.mk ()) μ)
Tactic: rw [dirac_unit_compProd, Kernel.const_apply]