awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {_c : γ | b ∈ s} : ℝ≥0∞)
    (s.indicator (fun (x : β) ↦ 1) b : ℝ≥0∞)
have 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∞)
Tactic: by_cases hb : b ∈ s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
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 : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {x : γ | b ∈ s} ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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∞)
⊢ ∫⁻ (b : β),
      (((η : (a : α × β) → Measure γ) (x, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        {x : γ | b ∈ s} ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
have simp_rw : ∫⁻ (b : β), s.indicator (fun (x : β) ↦ 1) b ∂(κ : (a : α) → Measure β) x =
  (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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∞)
⊢ ∫⁻ (b : β), s.indicator (fun (x : β) ↦ 1) b ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) =
  (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
Tactic: rw [lintegral_indicator_const hs, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ ∫⁻ (b : β), s.indicator (fun (x : β) ↦ 1) b ∂(κ : (a : α) → Measure β) x =
    (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s
have rw₁ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [lintegral_indicator_const hs, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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 : α
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have 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
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have 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
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have 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
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have 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
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have 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
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have 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
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ Eq (α := ℝ≥0∞)
    ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) x : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have 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
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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 : α
⊢ 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∞)
have 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}
Tactic: simp only [deterministic_apply, Measure.dirac_apply,
    Set.indicator_apply, Pi.one_apply, compProd_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
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}
⊢ ∫⁻ (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}
have ht : MeasurableSet t
Tactic: have ht : MeasurableSet t := (measurable_id.prodMk (hf.comp measurable_prodMk_left)) hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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 : β), 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}
have 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}
Tactic: rw [← lintegral_add_compl _ ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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 +
      ∫⁻ (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}
have h : ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x = 0
Tactic: convert! add_zero _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ ∫⁻ (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}
have 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
Tactic: convert! add_zero _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x = 0
have rw : ∫⁻ (x : β) in tᶜ, 0 ∂(κ : (a : α) → Measure β) x = 0
Tactic: rw [setLIntegral_congr_fun ht.compl this, lintegral_zero]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
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
⊢ ∫⁻ (x_1 : β) in tᶜ, if f (x, x_1) ∈ Prod.mk x_1 ⁻¹' s then 1 else 0 ∂(κ : (a : α) → Measure β) x = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [setLIntegral_congr_fun ht.compl this, lintegral_zero]