awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
simp_rw :
  (((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β)) :
        (a : Set (α × β)) → ℝ≥0∞)
      s =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ
simp_rw₁ :
  ∫⁻ (b : α),
      ((((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β) ((), b) :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(Kernel.const Unit μ : (a : Unit) → Measure α) () =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ
simp_rw₂ :
  ∫⁻ (b : α),
      ((((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β) ((), b) :
            Measure β) :
          (a : Set β) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂μ =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ
⊢ (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) s =
    ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ

Tactic:
simp_rw [compProd, Kernel.compProd_apply hs, Kernel.const_apply, Kernel.prodMkLeft_apply']

Premises used: ProbabilityTheory.Kernel.prodMkLeft_apply', MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.compProd_apply, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsMarkovKernel κ
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp [compProd]

Premises used: MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (μ ⊗ₘ κ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
    ∫⁻ (a : α) in s, (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) t ∂μ

Tactic:
simp [compProd, Kernel.compProd_apply_prod hs ht]

Premises used: MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.compProd_apply_prod
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)
e_a :
  Eq (α := Kernel Unit (α × β)) (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ)
    (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η)
⊢ Eq (α := Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ : (a : Unit) → Measure (α × β)) () : Measure (α × β))
    ((Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η : (a : Unit) → Measure (α × β)) () : Measure (α × β))

Tactic:
congr 1
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)
⊢ Eq (α := Kernel Unit (α × β)) (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ)
    (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η)

Tactic:
Kernel.compProd_congr ?_

Premises used: ProbabilityTheory.Kernel.compProd_congr
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)
e_a :
  ∀ (a : Unit),
    ∀ᵐ (b : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) a : Measure α),
      Eq.{u_2 + 1} (α := Measure β)
        (((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β) (a, b) : Measure β)
        (((Kernel.prodMkLeft Unit η : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β) (a, b) : Measure β)
⊢ Eq (α := Kernel Unit (α × β)) (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ)
    (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η)

Tactic:
refine Kernel.compProd_congr ?_

Premises used: ProbabilityTheory.Kernel.compProd_congr
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure β) (ae μ) (⇑κ : (a : α) → Measure β) (⇑η : (a : α) → Measure β)
⊢ ∀ (a : Unit),
    ∀ᵐ (b : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) a : Measure α),
      Eq.{u_2 + 1} (α := Measure β)
        (((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β) (a, b) : Measure β)
        (((Kernel.prodMkLeft Unit η : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β) (a, b) : Measure β)

Tactic:
simpa
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ 0 ⊗ₘ κ = 0

Tactic:
simp [compProd]

Premises used: MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
⊢ Eq (α := Measure (α × β)) (μ ⊗ₘ 0) 0

Tactic:
simp [compProd]

Premises used: MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = 0 ↔ ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)

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

Premises used: Iff.intro
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
refine_1 :
  ∀ (h : μ ⊗ₘ κ = 0),
    ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)
refine_2 :
  ∀ (h : ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)),
    μ ⊗ₘ κ = 0
⊢ μ ⊗ₘ κ = 0 ↔ ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
refine_1 :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)

Tactic:
simp_rw [← measure_univ_eq_zero]

Premises used: MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(lintegral_eq_zero_iff (Kernel.measurable_coe _ .univ)).mp ?_

Premises used: MeasureTheory.lintegral_eq_zero_iff, Filter.EventuallyEq, Iff.mp, ProbabilityTheory.Kernel.measurable_coe, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
refine_1 : ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂μ = 0
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine (lintegral_eq_zero_iff (Kernel.measurable_coe _ .univ)).mp ?_

Premises used: MeasureTheory.lintegral_eq_zero_iff, Iff.mp, ProbabilityTheory.Kernel.measurable_coe, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
refine_1 :
  Eq (α := ℝ≥0∞) ((0 : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ ∂μ = 0

Tactic:
rw [← setLIntegral_univ, ← compProd_apply_prod .univ .univ, h]

Premises used: MeasureTheory.Measure.compProd_apply_prod, MeasurableSet.univ, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h : μ ⊗ₘ κ = 0
⊢ Eq (α := ℝ≥0∞) ((0 : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h : ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)
refine_2 : μ ⊗ₘ κ = μ ⊗ₘ 0
⊢ μ ⊗ₘ κ = 0

Tactic:
rw [← compProd_zero_right μ]

Premises used: MeasureTheory.Measure.compProd_zero_right
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h : ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)
⊢ μ ⊗ₘ κ = μ ⊗ₘ 0

Tactic:
compProd_congr h

Premises used: MeasureTheory.Measure.compProd_congr
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
h : ∀ᵐ (a : α) ∂μ, Eq.{u_2 + 1} (α := Measure β) ((κ : (a : α) → Measure β) a : Measure β) (0 : Measure β)
⊢ μ ⊗ₘ κ = μ ⊗ₘ 0

Tactic:
exact compProd_congr h
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
a : α
h :
  ∀ (s : Set (β × γ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
      (((κ : (a : α) → Measure β) a ⊗ₘ η.sectR a : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (κ ⊗ₖ η : (a : α) → Measure (β × γ)) a = (κ : (a : α) → Measure β) a ⊗ₘ η.sectR a

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

Tactic:
simp_rw [Kernel.compProd_apply hs, compProd_apply hs, Kernel.sectR_apply]

Premises used: ProbabilityTheory.Kernel.sectR_apply, MeasureTheory.Measure.compProd_apply, ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h :
  ∀ (s : Set (α × α)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ ⊗ₘ Kernel.id : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)
      (((map (fun (x : α) ↦ (x, x)) μ : Measure (α × α)) : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ ⊗ₘ Kernel.id = map (fun (x : α) ↦ (x, x)) μ

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h :
  ∫⁻ (a : α), (((Kernel.id : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ Kernel.id : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)
    (((map (fun (x : α) ↦ (x, x)) μ : Measure (α × α)) : (a : Set (α × α)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [compProd_apply hs, map_apply (measurable_id.prod measurable_id) hs]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.compProd_apply, Measurable.prod
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
⊢ ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)

Tactic:
have h_meas a : MeasurableSet (Prod.mk a ⁻¹' s) := measurable_prodMk_left hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
h : ∫⁻ (a : α), (Prod.mk a ⁻¹' s).indicator 1 a ∂μ = (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)
⊢ ∫⁻ (a : α), (((Kernel.id : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)

Tactic:
simp_rw [Kernel.id_apply, dirac_apply' _ (h_meas _)]

Premises used: MeasureTheory.Measure.dirac_apply', ProbabilityTheory.Kernel.id_apply
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), (Prod.mk a ⁻¹' s).indicator 1 a ∂μ = ∫⁻ (a : α), indicator ((fun (x : α) ↦ (x, x)) ⁻¹' s) 1 a ∂μ

Tactic:
rfl

Premises used: Set.Mem, Set.indicator, setOf, Set.preimage, rfl
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
rw : MeasurableSet (α := α) ((fun (x : α) ↦ (x, x)) ⁻¹' s)
⊢ ∫⁻ (a : α), indicator ((fun (x : α) ↦ (x, x)) ⁻¹' s) 1 a ∂μ = (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)

Tactic:
rw [lintegral_indicator_one]

Premises used: MeasureTheory.lintegral_indicator_one
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ MeasurableSet (α := α) ((fun (x : α) ↦ (x, x)) ⁻¹' s)

Tactic:
(measurable_id.prod measurable_id) hs

Premises used: Measurable.prod
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ MeasurableSet (α := α) ((fun (x : α) ↦ (x, x)) ⁻¹' s)

Tactic:
exact (measurable_id.prod measurable_id) hs

Premises used: Measurable.prod
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
calc :
  ∫⁻ (a : α), indicator ((fun (x : α) ↦ (x, x)) ⁻¹' s) 1 a ∂μ = (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)
⊢ ∫⁻ (a : α), (Prod.mk a ⁻¹' s).indicator 1 a ∂μ = (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, x)) ⁻¹' s)

Tactic:
calc ∫⁻ a, (Prod.mk a ⁻¹' s).indicator 1 a ∂μ
  _ = ∫⁻ a, ((fun x ↦ (x, x)) ⁻¹' s).indicator 1 a ∂μ := rfl
  _ = μ ((fun x ↦ (x, x)) ⁻¹' s) := by
    rw [lintegral_indicator_one]
    exact (measurable_id.prod measurable_id) hs

Premises used: Prod.mk, Set.preimage, DFunLike.coe, rfl
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : α × β → Prop
hp : MeasurableSet (α := α × β) {x : α × β | p x}
h : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β), p (a, b)
⊢ ∀ᵐ (x : α × β) ∂μ ⊗ₘ κ, p x

Tactic:
Kernel.ae_compProd_of_ae_ae hp h

Premises used: ProbabilityTheory.Kernel.ae_compProd_of_ae_ae, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
p : α × β → Prop
h : ∀ᵐ (x : α × β) ∂μ ⊗ₘ κ, p x
⊢ ∀ᵐ (b : α) ∂((Kernel.const Unit μ : (a : Unit) → Measure α) () : Measure α),
    ∀ᵐ (c :
      β) ∂(((Kernel.prodMkLeft Unit κ : Kernel.{u_1, u_2} (Unit × α) β) : (a : Unit × α) → Measure β) ((), b) :
        Measure β),
      p (b, c)

Tactic:
Kernel.ae_ae_of_ae_compProd h

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
p : α × β → Prop
h : ∀ᵐ (x : α × β) ∂μ ⊗ₘ κ, p x
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β), p (a, b)

Tactic:
convert! Kernel.ae_ae_of_ae_compProd h

Premises used: ProbabilityTheory.Kernel.ae_ae_of_ae_compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst : SFinite μ
inst_1 : IsSFiniteKernel κ
p : α × β → Prop
hp : MeasurableSet (α := α × β) {x : α × β | p x}
⊢ (∀ᵐ (x : α × β) ∂μ ⊗ₘ κ, p x) ↔ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β), p (a, b)

Tactic:
Kernel.ae_compProd_iff hp

Premises used: ProbabilityTheory.Kernel.ae_compProd_iff, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : α → Prop
hp : MeasurableSet.{u_1} (α := α) {x : α | p x}
h : ∀ᵐ (a : α) ∂μ, p a
a : α
ha : p a
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β), p a

Tactic:
simp [ha]
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : α → Prop
hp : MeasurableSet.{u_1} (α := α) {x : α | p x}
h : ∀ᵐ (a : α) ∂μ, p a
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ p a) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β), p (a, b).1) x} x}
      a
h₂ h₃ : ∀ (a : α) (ha : p a), ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β), p a
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β), p (a, b).1

Tactic:
filter_upwards [h] with a ha using by simp [ha]
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
γ : Type u_3
mγ : MeasurableSpace γ
inst : MeasurableEq γ
κ : Kernel α β
f g : α → γ
hf : Measurable f
hg : Measurable g
h : f =ᶠ[ae μ] g
⊢ (ae (μ ⊗ₘ κ)).EventuallyEq (β := γ) (fun (p : α × β) ↦ f p.1) fun (p : α × β) ↦ g p.1

Tactic:
ae_compProd_of_ae_fst κ (measurableSet_eq_fun hf hg) h

Premises used: MeasureTheory.Measure.ae_compProd_of_ae_fst, measurableSet_eq_fun, Filter.EventuallyEq
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
h :
  ∀ (s : Set (α × β)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ ⊗ₘ Kernel.const α ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ ⊗ₘ Kernel.const α ν = μ.prod ν

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst : SFinite μ
inst_1 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h :
  ∫⁻ (a : α),
      ((((Kernel.const α ν : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        (Prod.mk a ⁻¹' s) ∂μ =
    (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s
h₁ :
  ∫⁻ (a : α),
      ((((Kernel.const α ν : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        (Prod.mk a ⁻¹' s) ∂μ =
    ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ ⊗ₘ Kernel.const α ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [compProd_apply hs, prod_apply hs, Kernel.const_apply]

Premises used: MeasureTheory.Measure.prod_apply, MeasureTheory.Measure.compProd_apply, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst : SFinite μ
inst_1 : SFinite ν
κ : Kernel α β
pos : ∀ (hκ : IsSFiniteKernel κ), (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
neg : ∀ (hκ : ¬IsSFiniteKernel κ), (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

Tactic:
by_cases hκ : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel