awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
pos :
  ∀ (hκ : IsSFiniteKernel κ),
    (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
      κ ⊗ₖ η ⊗ₖ ξ
neg :
  ∀ (hκ : ¬IsSFiniteKernel κ),
    (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
      κ ⊗ₖ η ⊗ₖ ξ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ

Tactic:
by_cases hκ : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 κ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ

Tactic:
simp [hκ]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : β × γ × δ) → (β × γ) × δ) =
      κ ⊗ₖ η ⊗ₖ ξ
neg :
  ∀ (hη : ¬IsSFiniteKernel η),
    (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
      κ ⊗ₖ η ⊗ₖ ξ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ

Tactic:
by_cases hη : IsSFiniteKernel η

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ

Tactic:
simp [hη]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : β × γ × δ) → (β × γ) × δ) =
      κ ⊗ₖ η ⊗ₖ ξ
neg :
  ∀ (hξ : ¬IsSFiniteKernel ξ),
    (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
        (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
      κ ⊗ₖ η ⊗ₖ ξ
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ

Tactic:
by_cases hξ : IsSFiniteKernel ξ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : (α × β) × γ) → α × β × γ) ⋯)

Tactic:
fun h_sfin ↦ hξ ?_

Premises used: Not
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 ξ
refine :
  ∀ (h_sfin : IsSFiniteKernel (ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)),
    IsSFiniteKernel ξ
⊢ ¬IsSFiniteKernel (ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)

Tactic:
refine fun h_sfin ↦ hξ ?_
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : (α × β) × γ) → α × β × γ) ⋯)
⊢ ξ =
    (ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯).comap
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⋯

Tactic:
simp [← comap_comp_right]

Premises used: ProbabilityTheory.Kernel.comap_comp_right
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : (α × β) × γ) → α × β × γ) ⋯)
⊢ ξ =
    (ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯).comap
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⋯

Tactic:
have : ξ = (ξ.comap MeasurableEquiv.prodAssoc (MeasurableEquiv.measurable _)).comap
          MeasurableEquiv.prodAssoc.symm (MeasurableEquiv.measurable _) := by
        simp [← comap_comp_right]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : α × β × γ) → (α × β) × γ) ⋯
rw :
  IsSFiniteKernel
    ((ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯).comap
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⋯)
⊢ IsSFiniteKernel ξ

Tactic:
rw [this]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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
    ((ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯).comap
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : α × β × γ) → (α × β) × γ) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : (α × β) × γ) → α × β × γ) ⋯)

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
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 ξ
this : ¬IsSFiniteKernel (ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ

Tactic:
simp [hξ, this]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 ξ
pos :
  ∀ (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∞)
⊢ (κ ⊗ₖ (η ⊗ₖ ξ.comap (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⋯)).map
      (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) =
    κ ⊗ₖ η ⊗ₖ ξ

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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
⊢ Measurable (α := β × γ × δ) (β := (β × γ) × δ)
    (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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
pos₁ :
  Measurable (β := ℝ≥0∞) fun (b : β × γ) ↦
    (((ξ : (a : α × β × γ) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' 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∞)

Tactic:
rw [compProd_apply hs, map_apply' _ (by fun_prop) _ hs,
    compProd_apply (hs.preimage (by fun_prop)), lintegral_compProd]

Premises used: MeasurableSet.preimage, ProbabilityTheory.Kernel.map_apply', ProbabilityTheory.Kernel.compProd_apply, ProbabilityTheory.Kernel.lintegral_compProd
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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
⊢ Measurable (β := ℝ≥0∞) fun (b : β × γ) ↦
    (((ξ : (a : α × β × γ) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
measurable_kernel_prodMk_left' hs a

Premises used: ProbabilityTheory.Kernel.measurable_kernel_prodMk_left'
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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
⊢ Measurable (β := ℝ≥0∞) fun (b : β × γ) ↦
    (((ξ : (a : α × β × γ) → Measure δ) (a, b) : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
exact measurable_kernel_prodMk_left' hs a

Premises used: ProbabilityTheory.Kernel.measurable_kernel_prodMk_left'
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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) =
      ∫⁻ (c : γ),
        (((ξ : (a : α × β × γ) → Measure δ) (a, b, c) : Measure δ) : (a : Set δ) → ℝ≥0∞)
          (Prod.mk (b, c) ⁻¹' s) ∂(η : (a : α × β) → Measure γ) (a, b)
⊢ ∫⁻ (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

Tactic:
congr with b
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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)
pos₁ :
  MeasurableSet (α := γ × δ)
    (Prod.mk b ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) ⁻¹' s)
⊢ (((η ⊗ₖ ξ.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)

Tactic:
rw [compProd_apply]

Premises used: ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : β
⊢ ∫⁻ (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)

Tactic:
congr
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : β
⊢ Measurable (β := (β × γ) × δ) fun (x : γ × δ) ↦
    (MeasurableEquiv.symm MeasurableEquiv.prodAssoc : (a : β × γ × δ) → (β × γ) × δ) (b, x)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 : β
⊢ MeasurableSet (α := γ × δ)
    (Prod.mk b ⁻¹' (⇑(MeasurableEquiv.symm MeasurableEquiv.prodAssoc) : (a : β × γ × δ) → (β × γ) × δ) ⁻¹' s)

Tactic:
exact hs.preimage (by fun_prop)

Premises used: MeasurableSet.preimage
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 η), (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η
neg : ∀ (hη : ¬IsSFiniteKernel η), (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η

Tactic:
by_cases hη : IsSFiniteKernel η

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 η
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
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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∞)

Tactic:
simp [compProd_apply hs]

Premises used: ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 η
⊢ (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η

Tactic:
simp [hη]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 μ), μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η
neg : ∀ (hμ : ¬IsSFiniteKernel μ), μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

Tactic:
by_cases hμ : IsSFiniteKernel μ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 μ
⊢ μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η

Tactic:
simp [hμ]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
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 μ
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