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
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
pos :
  ∀ (hη : IsSFiniteKernel η),
    (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
      κ ⊗ₖ η ⊗ₖ ξ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
have neg : ∀ (hη : ¬IsSFiniteKernel η),
  (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
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
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
have pos : ∀ (hξ : IsSFiniteKernel ξ),
  (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
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
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
pos :
  ∀ (hξ : IsSFiniteKernel ξ),
    (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
      κ ⊗ₖ η ⊗ₖ ξ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
have neg : ∀ (hξ : ¬IsSFiniteKernel ξ),
  (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
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
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : ¬IsSFiniteKernel ξ
⊢ ¬IsSFiniteKernel (ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)
have refine : ∀ (h_sfin : IsSFiniteKernel (ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry)), IsSFiniteKernel ξ
Tactic: refine fun h_sfin ↦ hξ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : ¬IsSFiniteKernel ξ
h_sfin : IsSFiniteKernel (ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)
⊢ IsSFiniteKernel ξ
have this : ξ =
  (ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry).comap
    (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) sorry
Tactic: have : ξ = (ξ.comap MeasurableEquiv.prodAssoc (MeasurableEquiv.measurable _)).comap
          MeasurableEquiv.prodAssoc.symm (MeasurableEquiv.measurable _) := by
        simp [← comap_comp_right]
-- 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 α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : ¬IsSFiniteKernel ξ
h_sfin : IsSFiniteKernel (ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)
this :
  ξ =
    (ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯).comap
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⋯
⊢ IsSFiniteKernel ξ
have rw : IsSFiniteKernel
  ((ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry).comap
    (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) sorry)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : ¬IsSFiniteKernel ξ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
have this : ¬IsSFiniteKernel (ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry)
Tactic: have : ¬ IsSFiniteKernel
        (ξ.comap MeasurableEquiv.prodAssoc (MeasurableEquiv.measurable _)) := by
      refine fun h_sfin ↦ hξ ?_
      have : ξ = (ξ.comap MeasurableEquiv.prodAssoc (MeasurableEquiv.measurable _)).comap
          MeasurableEquiv.prodAssoc.symm (MeasurableEquiv.measurable _) := by
        simp [← comap_comp_right]
      rw [this]
      infer_instance
-- 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 α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : IsSFiniteKernel ξ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ
have pos : ∀ (a : α) (s : Set ((β × γ) × δ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    (((((κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry)).map
                  (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) :
                (a : α) → Measure ((β × γ) × δ))
              a :
            Measure ((β × γ) × δ)) :
          (a : Set ((β × γ) × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ ⊗ₖ η ⊗ₖ ξ : (a : α) → Measure ((β × γ) × δ)) a : Measure ((β × γ) × δ)) : (a : Set ((β × γ) × δ)) → ℝ≥0∞) s :
      ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.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 α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : IsSFiniteKernel ξ
a : α
s : Set ((β × γ) × δ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((((κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
                  (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) :
                (a : α) → Measure ((β × γ) × δ))
              a :
            Measure ((β × γ) × δ)) :
          (a : Set ((β × γ) × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ ⊗ₖ η ⊗ₖ ξ : (a : α) → Measure ((β × γ) × δ)) a : Measure ((β × γ) × δ)) : (a : Set ((β × γ) × δ)) → ℝ≥0∞) s :
      ℝ≥0∞)
have pos : ∫⁻ (b : β),
    (((η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry : (a : α × β) → Measure (γ × δ))
            (a, b) :
          Measure (γ × δ)) :
        (a : Set (γ × δ)) → ℝ≥0∞)
      (Prod.mk b ⁻¹'
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) ⁻¹'
          s) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (b : β),
    ∫⁻ (c : γ),
      (((ξ : (a : α × β × γ) → Measure δ) (a, b, c) : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk (b, c) ⁻¹' s) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: rw [compProd_apply hs, map_apply' _ (by fun_prop) _ hs,
    compProd_apply (hs.preimage (by fun_prop)), lintegral_compProd]
-- 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 α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : IsSFiniteKernel ξ
a : α
s : Set ((β × γ) × δ)
hs : MeasurableSet s
pos :
  ∫⁻ (b : β),
      (((η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯ : (a : α × β) → Measure (γ × δ))
              (a, b) :
            Measure (γ × δ)) :
          (a : Set (γ × δ)) → ℝ≥0∞)
        (Prod.mk b ⁻¹'
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) ⁻¹'
            s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        (((ξ : (a : α × β × γ) → Measure δ) (a, b, c) : Measure δ) : (a : Set δ) → ℝ≥0∞)
          (Prod.mk (b, c) ⁻¹' s) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
⊢ Eq (α := ℝ≥0∞)
    (((((κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
                  (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) :
                (a : α) → Measure ((β × γ) × δ))
              a :
            Measure ((β × γ) × δ)) :
          (a : Set ((β × γ) × δ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ ⊗ₖ η ⊗ₖ ξ : (a : α) → Measure ((β × γ) × δ)) a : Measure ((β × γ) × δ)) : (a : Set ((β × γ) × δ)) → ℝ≥0∞) s :
      ℝ≥0∞)
have pos₁ : Measurable (β := ℝ≥0∞) fun (b : β × γ) ↦
  (((ξ : (a : α × β × γ) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: rw [compProd_apply hs, map_apply' _ (by fun_prop) _ hs,
    compProd_apply (hs.preimage (by fun_prop)), lintegral_compProd]
-- 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 α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : IsSFiniteKernel ξ
a : α
s : Set ((β × γ) × δ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β),
      (((η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯ : (a : α × β) → Measure (γ × δ))
              (a, b) :
            Measure (γ × δ)) :
          (a : Set (γ × δ)) → ℝ≥0∞)
        (Prod.mk b ⁻¹'
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) ⁻¹'
            s) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        (((ξ : (a : α × β × γ) → Measure δ) (a, b, c) : Measure δ) : (a : Set δ) → ℝ≥0∞)
          (Prod.mk (b, c) ⁻¹' s) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have pos : ∀ (b : β),
  (((η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry : (a : α × β) → Measure (γ × δ))
            (a, b) :
          Measure (γ × δ)) :
        (a : Set (γ × δ)) → ℝ≥0∞)
      (Prod.mk b ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) ⁻¹' s) =
    ∫⁻ (c : γ),
      (((ξ : (a : α × β × γ) → Measure δ) (a, b, c) : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk (b, c) ⁻¹' s) ∂(η : (a : α × β) → Measure γ) (a, b)
Tactic: congr with 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 α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : IsSFiniteKernel ξ
a : α
s : Set ((β × γ) × δ)
hs : MeasurableSet s
b : β
⊢ (((η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯ : (a : α × β) → Measure (γ × δ))
            (a, b) :
          Measure (γ × δ)) :
        (a : Set (γ × δ)) → ℝ≥0∞)
      (Prod.mk b ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) ⁻¹' s) =
    ∫⁻ (c : γ),
      (((ξ : (a : α × β × γ) → Measure δ) (a, b, c) : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk (b, c) ⁻¹' s) ∂(η : (a : α × β) → Measure γ) (a, b)
have pos : ∫⁻ (b_1 : γ),
    (((ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) sorry : (a : (α × β) × γ) → Measure δ)
            ((a, b), b_1) :
          Measure δ) :
        (a : Set δ) → ℝ≥0∞)
      (Prod.mk b_1 ⁻¹'
        Prod.mk b ⁻¹'
          (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) ⁻¹'
            s) ∂(η : (a : α × β) → Measure γ) (a, b) =
  ∫⁻ (c : γ),
    (((ξ : (a : α × β × γ) → Measure δ) (a, b, c) : Measure δ) : (a : Set δ) → ℝ≥0∞)
      (Prod.mk (b, c) ⁻¹' s) ∂(η : (a : α × β) → Measure γ) (a, b)
Tactic: rw [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 γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : IsSFiniteKernel ξ
a : α
s : Set ((β × γ) × δ)
hs : MeasurableSet s
b : β
pos :
  ∫⁻ (b_1 : γ),
      (((ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯ : (a : (α × β) × γ) → Measure δ)
              ((a, b), b_1) :
            Measure δ) :
          (a : Set δ) → ℝ≥0∞)
        (Prod.mk b_1 ⁻¹'
          Prod.mk b ⁻¹'
            (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) ⁻¹'
              s) ∂(η : (a : α × β) → Measure γ) (a, b) =
    ∫⁻ (c : γ),
      (((ξ : (a : α × β × γ) → Measure δ) (a, b, c) : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk (b, c) ⁻¹' s) ∂(η : (a : α × β) → Measure γ) (a, b)
⊢ (((η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯ : (a : α × β) → Measure (γ × δ))
            (a, b) :
          Measure (γ × δ)) :
        (a : Set (γ × δ)) → ℝ≥0∞)
      (Prod.mk b ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) ⁻¹' s) =
    ∫⁻ (c : γ),
      (((ξ : (a : α × β × γ) → Measure δ) (a, b, c) : Measure δ) : (a : Set δ) → ℝ≥0∞)
        (Prod.mk (b, c) ⁻¹' s) ∂(η : (a : α × β) → Measure γ) (a, b)
have pos₁ : MeasurableSet (α := γ × δ)
  (Prod.mk b ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) ⁻¹' s)
Tactic: rw [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 κ
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η
have pos : ∀ (hη : IsSFiniteKernel η), (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η
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 γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel μ
inst_1 : IsSFiniteKernel κ
pos : ∀ (hη : IsSFiniteKernel η), (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η
have neg : ∀ (hη : ¬IsSFiniteKernel η), (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η
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 γ
μ κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel μ
inst_1 : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η
have pos : ∀ (a : α) (s : Set (β × γ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    (((((μ + κ) ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((μ ⊗ₖ η + κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext _ _ 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 γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η
have pos : ∀ (hμ : IsSFiniteKernel μ), μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η
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 γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
pos : ∀ (hμ : IsSFiniteKernel μ), μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η
have neg : ∀ (hμ : ¬IsSFiniteKernel μ), μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η
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 γ
μ : Kernel α β
κ η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
hμ : IsSFiniteKernel μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η
have pos : ∀ (a : α) (s : Set (β × γ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((μ ⊗ₖ (κ + η) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((μ ⊗ₖ κ + μ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.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 η
hμ : IsSFiniteKernel μ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((μ ⊗ₖ (κ + η) : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((μ ⊗ₖ κ + μ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∫⁻ (b : β),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) :
        ℝ≥0∞) ∂(μ : (a : α) → Measure β) a =
  ∫⁻ (b : β),
      (((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(μ : (a : α) → Measure β) a +
    ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(μ : (a : α) → Measure β) a
Tactic: simp only [compProd_apply hs, coe_add, Pi.add_apply, Measure.coe_add]
-- 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 η
hμ : IsSFiniteKernel μ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
        ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) :
          ℝ≥0∞) ∂(μ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
        (((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(μ : (a : α) → Measure β) a +
      ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' s) ∂(μ : (a : α) → Measure β) a
have pos : Measurable (β := ℝ≥0∞) fun (b : β) ↦
  (((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
Tactic: rw [lintegral_add_left]
-- 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 : 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∞)
Tactic: simp_rw [sum_apply, compProd_apply hs, sum_apply, lintegral_sum_measure, Measure.sum_apply _ hs,
    compProd_apply hs]