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 η
h : κ ⊗ₖ η = 0
a : α
refine_1 :
  Eq (α := ℝ≥0∞)
    ((((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) (β := Set γ) Set.univ Set.univ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ ∫⁻ (a_1 : β),
      (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        Set.univ ∂(κ : (a : α) → Measure β) a =
    0

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

Premises used: ProbabilityTheory.Kernel.compProd_apply_prod, MeasurableSet.univ, MeasureTheory.setLIntegral_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 : α
⊢ Eq (α := ℝ≥0∞)
    ((((0 : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) (β := Set γ) Set.univ Set.univ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

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 α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsSFiniteKernel η
h :
  ∀ (a : α),
    ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
      Eq.{u_3 + 1} (α := Measure γ) ((η : (a : α × β) → Measure γ) (a, b) : Measure γ) (0 : Measure γ)
refine_2 : κ ⊗ₖ η = κ ⊗ₖ 0
⊢ κ ⊗ₖ η = 0

Tactic:
rw [← Kernel.compProd_zero_right κ]

Premises used: ProbabilityTheory.Kernel.compProd_zero_right
-- 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 γ) (0 : Measure γ)
⊢ κ ⊗ₖ η = κ ⊗ₖ 0

Tactic:
Kernel.compProd_congr h

Premises used: ProbabilityTheory.Kernel.compProd_congr
-- 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 γ) (0 : Measure γ)
⊢ κ ⊗ₖ η = κ ⊗ₖ 0

Tactic:
exact Kernel.compProd_congr h

Premises used: ProbabilityTheory.Kernel.compProd_congr
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
x : α
simp_rw :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {x : γ | b ∈ s} ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [compProd_apply (measurable_fst hs), ← Set.preimage_comp, Prod.fst_comp_mk, Set.preimage,
    Function.const_apply]

Premises used: Function.const_apply, Set.preimage_comp, Set.preimage, ProbabilityTheory.Kernel.compProd_apply, Prod.fst_comp_mk, measurable_fst
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
x : α
b : β
pos :
  ∀ (hb : b ∈ s),
    Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
      (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)
neg :
  ∀ (hb : b ∉ s),
    Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
      (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
    (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)

Tactic:
by_cases hb : b ∈ s
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
x : α
b : β
hb : b ∈ s
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
    (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)

Tactic:
simp [hb]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
x : α
b : β
hb : b ∉ s
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
    (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)

Tactic:
simp [hb]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
x : α
⊢ ∀ (b : β),
    Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
      (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)

Tactic:
have : ∀ b : β, η (x, b) {_c | b ∈ s} = s.indicator (fun _ ↦ 1) b := by
    intro b
    by_cases hb : b ∈ s <;> simp [hb]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
x : α
this :
  ∀ (b : β),
    Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
      (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)
simp_rw :
  ∫⁻ (b : β), s.indicator (fun (x : β) ↦ 1) b ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {x : γ | b ∈ s} ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
simp_rw [this]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
x : α
this :
  ∀ (b : β),
    Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
      (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (b : β), s.indicator (fun (x : β) ↦ 1) b ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
rw [lintegral_indicator_const hs, one_mul]

Premises used: MeasureTheory.lintegral_indicator_const, one_mul
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
κ : Kernel α β
η : Kernel (α × β) γ
inst : IsSFiniteKernel κ
inst_1 : IsMarkovKernel η
x : α
simp_rw :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' Prod.fst ⁻¹' s) ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
simp_rw₁ :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Prod.fst ∘ Prod.mk b ⁻¹' s) ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
simp_rw₂ :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        (Function.const γ b ⁻¹' s) ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
simp_rw₃ :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {x : γ | Function.const γ b x ∈ s} ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
simp_rw₄ :
  ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {x : γ | b ∈ s} ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
simp_rw₅ :
  ∀
    (this :
      ∀ (b : β),
        Eq (α := ℝ≥0∞)
          ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
          (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)),
    ∫⁻ (b : β),
        (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
          {x : γ | b ∈ s} ∂(κ : (a : α) → Measure β) x =
      (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
simp_rw₆ :
  ∀
    (this :
      ∀ (b : β),
        Eq (α := ℝ≥0∞)
          ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
          (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)),
    ∫⁻ (b : β), s.indicator (fun (x : β) ↦ 1) b ∂(κ : (a : α) → Measure β) x =
      (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
classical
  simp_rw [compProd_apply (measurable_fst hs), ← Set.preimage_comp, Prod.fst_comp_mk, Set.preimage,
    Function.const_apply]
  have : ∀ b : β, η (x, b) {_c | b ∈ s} = s.indicator (fun _ ↦ 1) b := by
    intro b
    by_cases hb : b ∈ s <;> simp [hb]
  simp_rw [this]
  rw [lintegral_indicator_const hs, one_mul]

Premises used: Function.const_apply, Set.preimage_comp, Set.preimage, MeasureTheory.lintegral_indicator_const, ProbabilityTheory.Kernel.compProd_apply, Prod.fst_comp_mk, measurable_fst, one_mul
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
simp :
  ∫⁻ (b : β), if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s}
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ deterministic f hf : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s} : ℝ≥0∞)

Tactic:
simp only [deterministic_apply, Measure.dirac_apply,
    Set.indicator_apply, Pi.one_apply, compProd_apply hs]

Premises used: Set.indicator_apply, Pi.one_apply, ProbabilityTheory.Kernel.deterministic_apply, MeasureTheory.Measure.dirac_apply, 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 γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
t : Set β := {b : β | (b, f (x, b)) ∈ s}
⊢ MeasurableSet t

Tactic:
have ht : MeasurableSet t := (measurable_id.prodMk (hf.comp measurable_prodMk_left)) hs
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
t : Set β := {b : β | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
rw :
  ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x +
      ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s}
⊢ ∫⁻ (b : β), if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s}

Tactic:
rw [← lintegral_add_compl _ ht]

Premises used: MeasureTheory.lintegral_add_compl
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
t : Set β := {b : β | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
⊢ ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x + 0 =
    ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x

Tactic:
add_zero _

Premises used: add_zero
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
t : Set β := {b : β | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
h : ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x = 0
h₁ :
  (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s} =
    ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x
⊢ ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x +
      ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s}

Tactic:
convert! add_zero _

Premises used: add_zero
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
t : Set β := {b : β | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
this : ∀ b ∈ tᶜ, Eq (α := ℝ≥0∞) (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) 0
rw : ∫⁻ (x : β) in tᶜ, 0 ∂(κ : (a : α) → Measure β) x = 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x = 0

Tactic:
rw [setLIntegral_congr_fun ht.compl this, lintegral_zero]

Premises used: MeasureTheory.setLIntegral_congr_fun, MeasureTheory.lintegral_zero, MeasurableSet.compl
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
t : Set β := {b : β | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
h : ∀ b ∈ tᶜ, Eq (α := ℝ≥0∞) (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) 0
⊢ ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x = 0

Tactic:
suffices ∀ b ∈ tᶜ, (if f (x, b) ∈ Prod.mk b ⁻¹' s then (1 : ℝ≥0∞) else 0) = 0 by
      rw [setLIntegral_congr_fun ht.compl this, lintegral_zero]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
t : Set β := {b : β | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
b : β
hb : b ∈ tᶜ
⊢ (b, f (x, b)) ∉ s

Tactic:
simp only [t, Set.mem_compl_iff, Set.mem_setOf_eq] at hb

Premises used: Set.mem_setOf_eq, Set.mem_compl_iff
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
t : Set β := {b : β | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
b : β
hb : (b, f (x, b)) ∉ s
⊢ Eq (α := ℝ≥0∞) (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) 0

Tactic:
simp [hb]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
t : Set β := {b : β | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
this : ∀ b ∈ t, Eq (α := ℝ≥0∞) (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) 1
rw :
  (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s} =
    ∫⁻ (x : β) in t, 1 ∂(κ : (a : α) → Measure β) x
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s} : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s} =
    ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x

Tactic:
rw [setLIntegral_congr_fun ht this, setLIntegral_one]

Premises used: MeasureTheory.setLIntegral_congr_fun, MeasureTheory.setLIntegral_one
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
t : Set β := {b : β | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
h : ∀ b ∈ t, Eq (α := ℝ≥0∞) (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) 1
⊢ (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s} =
    ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x

Tactic:
suffices ∀ b ∈ t, (if f (x, b) ∈ Prod.mk b ⁻¹' s then (1 : ℝ≥0∞) else 0) = 1 by
      rw [setLIntegral_congr_fun ht this, setLIntegral_one]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
t : Set β := {b : β | (b, f (x, b)) ∈ s}
ht : MeasurableSet t
b : β
hb : (b, f (x, b)) ∈ s
⊢ Eq (α := ℝ≥0∞) (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) 1

Tactic:
simp [hb]
-- Module: Mathlib.Probability.Kernel.Composition.CompProd
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass γ
f : α × β → γ
hf : Measurable f
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst_1 : IsSFiniteKernel κ
x : α
simp :
  ∫⁻ (b : β), if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s}
simp₁ :
  ∫⁻ (b : β), if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s}
simp₂ :
  let t : Set β := {b : β | (b, f (x, b)) ∈ s};
  ∀ (ht : MeasurableSet t),
    ∫⁻ (b : β), if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x =
      (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s}
simp₃ :
  let t : Set β := {b : β | (b, f (x, b)) ∈ s};
  ∀ (ht : MeasurableSet t),
    ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x +
        ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x =
      (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s}
h :
  let t : Set β := {b : β | (b, f (x, b)) ∈ s};
  ∀ (ht : MeasurableSet t),
    ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x = 0
h₁ h₂ :
  let t : Set β := {b : β | (b, f (x, b)) ∈ s};
  ∀ (ht : MeasurableSet t),
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s} =
      ∫⁻ (x_1 : β) in t, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ deterministic f hf : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s} : ℝ≥0∞)

Tactic:
classical
  simp only [deterministic_apply, Measure.dirac_apply,
    Set.indicator_apply, Pi.one_apply, compProd_apply hs]
  let t := {b | (b, f (x, b)) ∈ s}
  have ht : MeasurableSet t := (measurable_id.prodMk (hf.comp measurable_prodMk_left)) hs
  rw [← lintegral_add_compl _ ht]
  convert! add_zero _
  · suffices ∀ b ∈ tᶜ, (if f (x, b) ∈ Prod.mk b ⁻¹' s then (1 : ℝ≥0∞) else 0) = 0 by
      rw [setLIntegral_congr_fun ht.compl this, lintegral_zero]
    intro b hb
    simp only [t, Set.mem_compl_iff, Set.mem_setOf_eq] at hb
    simp [hb]
  · suffices ∀ b ∈ t, (if f (x, b) ∈ Prod.mk b ⁻¹' s then (1 : ℝ≥0∞) else 0) = 1 by
      rw [setLIntegral_congr_fun ht this, setLIntegral_one]
    intro b hb
    simp only [t, Set.mem_setOf_eq] at hb
    simp [hb]

Premises used: Set.indicator_apply, Pi.one_apply, ProbabilityTheory.Kernel.deterministic_apply, Set.mem_setOf_eq, MeasureTheory.Measure.dirac_apply, ProbabilityTheory.Kernel.compProd_apply, add_zero, Set.mem_compl_iff