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 γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s ×ˢ t) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (a_1 : β),
      s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t)
        a_1 ∂(κ : (a : α) → Measure β) a
⊢ (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (s ×ˢ t) =
    ∫⁻ (b : β) in s,
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t ∂(κ : (a : α) → Measure β) a

Tactic:
rw [compProd_apply (hs.prod ht), ← lintegral_indicator hs]

Premises used: MeasurableSet.prod, MeasureTheory.lintegral_indicator, 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 η
a : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
e_f :
  ∀ (a_1 : β),
    Eq (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' s ×ˢ t) : ℝ≥0∞)
      (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) a_1 :
        ℝ≥0∞)
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s ×ˢ t) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (a_1 : β),
      s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t)
        a_1 ∂(κ : (a : α) → Measure β) a

Tactic:
congr with a
-- 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 η
a_1 : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
pos :
  ∀ (ha : a ∈ s),
    Eq (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a_1, a) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s ×ˢ t) : ℝ≥0∞)
      (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a_1, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) a :
        ℝ≥0∞)
neg :
  ∀ (ha : a ∉ s),
    Eq (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a_1, a) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s ×ˢ t) : ℝ≥0∞)
      (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a_1, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) a :
        ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a_1, a) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s ×ˢ t) : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a_1, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) a : ℝ≥0∞)

Tactic:
by_cases ha : a ∈ s
-- 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 η
a_1 : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
ha : a ∈ s
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a_1, a) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s ×ˢ t) : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a_1, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) a : ℝ≥0∞)

Tactic:
simp [ha]
-- 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 η
a_1 : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
ha : a ∉ s
⊢ Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure γ) (a_1, a) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' s ×ˢ t) : ℝ≥0∞)
    (s.indicator (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a_1, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) t) a : ℝ≥0∞)

Tactic:
simp [ha]
-- 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 :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
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 :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
hκ : ¬IsSFiniteKernel κ
⊢ κ ⊗ₖ η = κ ⊗ₖ η'

Tactic:
simp_rw [compProd_of_not_isSFiniteKernel_left _ _ hκ]

Premises used: ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left
-- 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 :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
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
-- 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 :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  ∫⁻ (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
⊢ Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ ⊗ₖ η' : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [compProd_apply hs, 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 :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (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:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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 :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))
    fun (b : β) ↦ (((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)
⊢ ∫⁻ (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:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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 :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
b : β
hb :
  Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
    ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
rw rw₁ :
  Eq (α := ℝ≥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∞)
⊢ Eq (α := ℝ≥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∞)

Tactic:
rw [hb]
-- 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 :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
h₁ :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
                    ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq (α := ℝ≥0∞)
                    ((fun (b : β) ↦
                        ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) :
                          ℝ≥0∞))
                      x)
                    ((fun (b : β) ↦
                        ((((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) :
                          ℝ≥0∞))
                      x))
                x}
            x}
      a_1
h₂ h₃ :
  ∀ (b : β)
    (hb :
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ)
        ((η' : (a : α × β) → Measure γ) (a, b) : Measure γ)),
    Eq (α := ℝ≥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∞)
⊢ (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦ (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))
    fun (b : β) ↦ (((η' : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s)

Tactic:
filter_upwards [h a] with b hb using by rw [hb]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
pos : ∀ (h : IsSFiniteKernel κ), 0 ⊗ₖ κ = 0
neg : ∀ (h : ¬IsSFiniteKernel κ), 0 ⊗ₖ κ = 0
⊢ 0 ⊗ₖ κ = 0

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 (α × β) γ
h : IsSFiniteKernel κ
pos :
  ∀ (a : α) (s : Set (β × γ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((0 ⊗ₖ κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ 0 ⊗ₖ κ = 0

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 γ
κ : Kernel (α × β) γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  ∫⁻ (b : β),
      (((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂((0 : Kernel α β) : (a : α) → Measure β) a =
    (((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((((0 ⊗ₖ κ : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Kernel.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 (α × β) γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β),
      (((κ : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂((0 : Kernel α β) : (a : α) → Measure β) a =
    (((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
h : ¬IsSFiniteKernel κ
neg neg₁ : Eq (α := Kernel α (β × γ)) 0 0
⊢ 0 ⊗ₖ κ = 0

Tactic:
rw [Kernel.compProd_of_not_isSFiniteKernel_right _ _ h]

Premises used: ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
pos : ∀ (h : IsSFiniteKernel κ), Eq (α := Kernel α (β × γ)) (κ ⊗ₖ 0) 0
neg : ∀ (h : ¬IsSFiniteKernel κ), Eq (α := Kernel α (β × γ)) (κ ⊗ₖ 0) 0
⊢ Eq (α := Kernel α (β × γ)) (κ ⊗ₖ 0) 0

Tactic:
by_cases h : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
h : IsSFiniteKernel κ
pos :
  ∀ (a : α) (s : Set (β × γ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ ⊗ₖ 0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
      ((((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel α (β × γ)) (κ ⊗ₖ 0) 0

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
pos :
  ∫⁻ (b : β),
      (((0 : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    (((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((((κ ⊗ₖ 0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Kernel.compProd_apply hs]

Premises used: ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
h : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β),
      (((0 : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) a =
    (((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
h : ¬IsSFiniteKernel κ
neg neg₁ : Eq (α := Kernel α (β × γ)) 0 0
⊢ Eq (α := Kernel α (β × γ)) (κ ⊗ₖ 0) 0

Tactic:
rw [Kernel.compProd_of_not_isSFiniteKernel_left _ _ h]

Premises used: ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_left
-- 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 η
⊢ κ ⊗ₖ η = 0 ↔
    ∀ (a : α),
      ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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 η
refine_1 :
  ∀ (h : κ ⊗ₖ η = 0) (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)
refine_2 :
  ∀
    (h :
      ∀ (a : α),
        ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
          Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)),
    κ ⊗ₖ η = 0
⊢ κ ⊗ₖ η = 0 ↔
    ∀ (a : α),
      ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
        Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)

Tactic:
refine ⟨fun h ↦ ?_, fun 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 : κ ⊗ₖ η = 0
refine_1 :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        (0 : ℝ≥0∞)
⊢ ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)

Tactic:
simp_rw [← Measure.measure_univ_eq_zero]

Premises used: MeasureTheory.Measure.measure_univ_eq_zero
-- 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 : κ ⊗ₖ η = 0
⊢ ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        (0 : ℝ≥0∞)

Tactic:
fun a ↦ (lintegral_eq_zero_iff ?_).mp ?_

Premises used: MeasureTheory.lintegral_eq_zero_iff, Filter.EventuallyEq, Iff.mp
-- 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 : κ ⊗ₖ η = 0
refine_1 :
  ∀ (a : α),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ
refine_1₁ :
  ∀ (a : α),
    ∫⁻ (a_1 : β),
        (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          Set.univ ∂(κ : (a : α) → Measure β) a =
      0
⊢ ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        (0 : ℝ≥0∞)

Tactic:
refine fun a ↦ (lintegral_eq_zero_iff ?_).mp ?_

Premises used: MeasureTheory.lintegral_eq_zero_iff, Iff.mp
-- 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 : κ ⊗ₖ η = 0
a : α
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ

Tactic:
(η.measurable_coe .univ).comp measurable_prodMk_left

Premises used: Measurable.comp, ProbabilityTheory.Kernel.measurable_coe, measurable_prodMk_left, MeasurableSet.univ
-- 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 : κ ⊗ₖ η = 0
a : α
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) Set.univ

Tactic:
exact (η.measurable_coe .univ).comp measurable_prodMk_left

Premises used: Measurable.comp, ProbabilityTheory.Kernel.measurable_coe, measurable_prodMk_left, MeasurableSet.univ