awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
x : α
s : Set δ
ms : MeasurableSet s
⊢ ∫⁻ (a : β), (((η : (a : γ) → Measure δ) (f a) : Measure δ) : (a : Set δ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) x =
    ∫⁻ (b : β),
      (((η.comap f hf : (a : β) → Measure δ) b : Measure δ) : (a : Set δ) → ℝ≥0∞) s ∂(κ : (a : α) → Measure β) x

Tactic:
simp_rw [comap_apply']

Premises used: ProbabilityTheory.Kernel.comap_apply'
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β (γ × δ)
⊢ (η ∘ₖ κ).fst = η.fst ∘ₖ κ

Tactic:
simp [fst_eq, map_comp κ η _]

Premises used: ProbabilityTheory.Kernel.fst_eq, ProbabilityTheory.Kernel.map_comp
-- Module: Mathlib.Probability.Kernel.Composition.CompMap
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β (γ × δ)
simp_rw : Eq (α := Kernel α δ) ((η ∘ₖ κ).map Prod.snd) (η.map Prod.snd ∘ₖ κ)
⊢ (η ∘ₖ κ).snd = η.snd ∘ₖ κ

Tactic:
simp_rw [snd_eq, map_comp κ η _]

Premises used: ProbabilityTheory.Kernel.snd_eq, ProbabilityTheory.Kernel.map_comp
-- Module: Mathlib.Probability.Kernel.Composition.CompNotation
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : IsMarkovKernel κ
⊢ Eq (α := ENNReal) ((((⇑κ : (a : α) → Measure β) ∘ₘ μ : Measure β) : (a : Set β) → ENNReal) Set.univ : ENNReal)
    ((μ : (a : Set α) → ENNReal) Set.univ : ENNReal)

Tactic:
simp [bind_apply .univ κ.aemeasurable]

Premises used: MeasureTheory.Measure.bind_apply, ProbabilityTheory.Kernel.aemeasurable, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.CompNotation
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
⊢ Eq (α := Measure β) ((⇑(Kernel.deterministic f hf) : (a : α) → Measure β) ∘ₘ μ) (map f μ)

Tactic:
Measure.bind_dirac_eq_map μ hf

Premises used: MeasureTheory.Measure.dirac, MeasureTheory.Measure.bind_dirac_eq_map, MeasureTheory.OuterMeasure.toMeasure, MeasureTheory.Measure.ofMeasurable
-- Module: Mathlib.Probability.Kernel.Composition.CompNotation
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
rw : (⇑(Kernel.deterministic id ⋯) : (a : α) → Measure α) ∘ₘ μ = μ
rw₁ : map id μ = μ
rw₂ rw₃ : μ = μ
⊢ (⇑Kernel.id : (a : α) → Measure α) ∘ₘ μ = μ

Tactic:
rw [Kernel.id, deterministic_comp_eq_map, Measure.map_id]

Premises used: MeasureTheory.Measure.map_id, ProbabilityTheory.Kernel.id, MeasureTheory.Measure.deterministic_comp_eq_map
-- Module: Mathlib.Probability.Kernel.Composition.CompNotation
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure (α × β)
⊢ Eq (α := Measure (β × α)) ((⇑(Kernel.swap α β) : (a : α × β) → Measure (β × α)) ∘ₘ μ) (map Prod.swap μ)

Tactic:
deterministic_comp_eq_map measurable_swap

Premises used: MeasureTheory.Measure.deterministic_comp_eq_map, measurable_swap
-- Module: Mathlib.Probability.Kernel.Composition.CompNotation
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
⊢ (⇑(Kernel.const α ν) : (a : α) → Measure β) ∘ₘ μ =
    HSMul.hSMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) Set.univ : ENNReal) ν

Tactic:
μ.bind_const

Premises used: MeasureTheory.Measure.bind_const
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
simp_rw :
  ∫⁻ (a_1 : β),
      ENNReal.ofReal
        (ENNReal.toReal
          ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (Prod.mk a_1 ⁻¹' s))) ∂(κ : (a : α) → Measure β) a <
    ∞
⊢ @HasFiniteIntegral _ ℝ _ mβ
    (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)

Tactic:
simp_rw [hasFiniteIntegral_iff_enorm, measureReal_def, enorm_eq_ofReal toReal_nonneg]

Premises used: ENNReal.toReal_nonneg, MeasureTheory.measureReal_def, Real.enorm_eq_ofReal, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
⊢ ∫⁻ (b : β),
      ENNReal.ofReal
        (ENNReal.toReal
          ((((η : (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 ⁻¹' t) ∂(κ : (a : α) → Measure β) a

Tactic:
lintegral_mono_ae ?_

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
refine :
  ∀ᵐ (a_1 : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ENNReal.ofReal
        (ENNReal.toReal
          ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' s))) ≤
      (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' t)
⊢ ∫⁻ (b : β),
      ENNReal.ofReal
        (ENNReal.toReal
          ((((η : (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 ⁻¹' t) ∂(κ : (a : α) → Measure β) a

Tactic:
refine lintegral_mono_ae ?_

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
h :
  ∀ (b : β)
    (hb :
      LT.lt (α := ℝ≥0∞)
        ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
        (∞ : ℝ≥0∞)),
    ENNReal.ofReal
        (ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))) ≤
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' t)
⊢ ∀ᵐ (a_1 : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    ENNReal.ofReal
        (ENNReal.toReal
          ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' s))) ≤
      (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' t)

Tactic:
filter_upwards [ae_kernel_lt_top a h2s] with b hb

Premises used: ProbabilityTheory.Kernel.ae_kernel_lt_top
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
b : β
hb :
  LT.lt (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
h :
  LE.le (α := ℝ≥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 ⁻¹' t) : ℝ≥0∞)
⊢ ENNReal.ofReal
      (ENNReal.toReal ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s))) ≤
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' t)

Tactic:
rw [ofReal_toReal hb.ne]

Premises used: ENNReal.ofReal_toReal, LT.lt.ne
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
b : β
hb :
  LT.lt (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥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 ⁻¹' t) : ℝ≥0∞)

Tactic:
measure_mono (preimage_mono (subset_toMeasurable _ _))

Premises used: MeasureTheory.subset_toMeasurable, Set.preimage_mono, MeasureTheory.measure_mono
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
b : β
hb :
  LT.lt (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥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 ⁻¹' t) : ℝ≥0∞)

Tactic:
exact measure_mono (preimage_mono (subset_toMeasurable _ _))

Premises used: MeasureTheory.subset_toMeasurable, Set.preimage_mono, MeasureTheory.measure_mono
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(κ : (a : α) → Measure β) a ≤
    (((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) t

Tactic:
le_compProd_apply _ _ _ _

Premises used: Set.Mem, setOf, ProbabilityTheory.Kernel.le_compProd_apply, Set.preimage
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
⊢ Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_toMeasurable s

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
⊢ LT.lt (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
h2s.lt_top

Premises used: Ne.lt_top
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
b :
  ∫⁻ (b : β),
      ENNReal.ofReal
        (ENNReal.toReal
          ((((η : (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 ⁻¹' t) ∂(κ : (a : α) → Measure β) a
⊢ ∫⁻ (a_1 : β),
      ENNReal.ofReal
        (ENNReal.toReal
          ((((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (Prod.mk a_1 ⁻¹' s))) ∂(κ : (a : α) → Measure β) a <
    ∞

Tactic:
calc
    ∫⁻ b, ENNReal.ofReal (η (a, b) (Prod.mk b ⁻¹' s)).toReal ∂κ a
    _ ≤ ∫⁻ b, η (a, b) (Prod.mk b ⁻¹' t) ∂κ a := by
      refine lintegral_mono_ae ?_
      filter_upwards [ae_kernel_lt_top a h2s] with b hb
      rw [ofReal_toReal hb.ne]
      exact measure_mono (preimage_mono (subset_toMeasurable _ _))
    _ ≤ (κ ⊗ₖ η) a t := le_compProd_apply _ _ _ _
    _ = (κ ⊗ₖ η) a s := measure_toMeasurable s
    _ < ⊤ := h2s.lt_top

Premises used: ProbabilityTheory.Kernel.le_compProd_apply, MeasureTheory.measure_toMeasurable, Ne.lt_top, DFunLike.coe, ProbabilityTheory.Kernel.compProd
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
left :
  AEStronglyMeasurable (β := ℝ) (m₀ := mβ)
    (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)
right :
  @HasFiniteIntegral _ ℝ _ mβ
    (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)

Tactic:
constructor
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mβ)
    (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)

Tactic:
(measurable_kernel_prodMk_left' hs a).ennreal_toReal.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, MeasureTheory.Measure.real, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left', Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mβ)
    (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)

Tactic:
exact (measurable_kernel_prodMk_left' hs a).ennreal_toReal.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left', Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ @HasFiniteIntegral _ ℝ _ mβ
    (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)

Tactic:
hasFiniteIntegral_prodMk_left a h2s

Premises used: ProbabilityTheory.hasFiniteIntegral_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ @HasFiniteIntegral _ ℝ _ mβ
    (fun (b : β) ↦ Measure.real (m := mγ) ((η : (a : α × β) → Measure γ) (a, b)) (Prod.mk b ⁻¹' s))
    ((κ : (a : α) → Measure β) a)

Tactic:
exact hasFiniteIntegral_prodMk_left a h2s

Premises used: ProbabilityTheory.hasFiniteIntegral_prodMk_left
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hf : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
a_1 : β
hx :
  ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ), f (a_1, c) = AEStronglyMeasurable.mk f hf (a_1, c)
⊢ Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y))
    (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ AEStronglyMeasurable.mk f hf (a_1, y))

Tactic:
integral_congr_ae hx

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : NormedAddCommGroup E
a : α
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_2 : IsSFiniteKernel η
inst_3 : NormedSpace ℝ E
f : β × γ → E
hf : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (b : β) ↦
                  ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, b) : Measure γ),
                    f (b, c) = AEStronglyMeasurable.mk f hf (b, c))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq.{u_4 + 1} (α := E)
                    ((fun (x : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y) : E))
                      x)
                    ((fun (x : β) ↦
                        (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦
                            AEStronglyMeasurable.mk f hf (x, y) :
                          E))
                      x))
                x}
            x}
      a_1
h₁ h₂ :
  ∀ (a_1 : β)
    (hx :
      ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ),
        f (a_1, c) = AEStronglyMeasurable.mk f hf (a_1, c)),
    Eq.{u_4 + 1} (α := E) (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦ f (a_1, y))
      (@integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, a_1)) fun (y : γ) ↦
        AEStronglyMeasurable.mk f hf (a_1, y))
⊢ EventuallyEq.{u_2, u_4} (β := E) (ae (F := Measure β) ((κ : (a : α) → Measure β) a : Measure β))
    (fun (x : β) ↦ @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ f (x, y)) fun (x : β) ↦
    @integral _ _ _ _ mγ ((η : (a : α × β) → Measure γ) (a, x)) fun (y : γ) ↦ AEStronglyMeasurable.mk f hf (x, y)

Tactic:
filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ hx using integral_congr_ae hx

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_compProd, MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
δ : Type u_5
inst_2 : TopologicalSpace δ
f : β × γ → δ
hf : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
x : β
hx : ∀ᵐ (c : γ) ∂((η : (a : α × β) → Measure γ) (a, x) : Measure γ), f (x, c) = AEStronglyMeasurable.mk f hf (x, c)
⊢ AEStronglyMeasurable.{u_3, u_5} (β := δ) (m₀ := mγ) (fun (y : γ) ↦ f (x, y)) ((η : (a : α × β) → Measure γ) (a, x))

Tactic:
⟨fun y => hf.mk f (x, y), hf.stronglyMeasurable_mk.comp_measurable measurable_prodMk_left, hx⟩

Premises used: Prod.mk, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.StronglyMeasurable.comp_measurable, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable, measurable_prodMk_left