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 γ
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
have h : ∀ b ∈ tᶜ, Eq (α := ℝ≥0∞) (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) 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]
-- 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}
ht : MeasurableSet t
b : β
hb : b ∈ tᶜ
⊢ Eq (α := ℝ≥0∞) (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) 0
have hb₁ : (b, f (x, b)) ∉ s
Tactic: simp only [t, Set.mem_compl_iff, Set.mem_setOf_eq] at hb
Cleared hypotheses: 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 γ
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
⊢ (((κ : (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
have rw : (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s} =
  ∫⁻ (x : β) in t, 1 ∂(κ : (a : α) → Measure β) x
Tactic: rw [setLIntegral_congr_fun ht this, setLIntegral_one]
-- 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) 1
rw :
  (((κ : (a : α) → Measure β) x : Measure β) : (a : Set β) → ℝ≥0∞) {b : β | (b, f (x, b)) ∈ s} =
    ∫⁻ (x : β) in t, 1 ∂(κ : (a : α) → Measure β) x
⊢ (((κ : (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
have 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∞)
Tactic: rw [setLIntegral_congr_fun ht this, setLIntegral_one]
-- 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
⊢ (((κ : (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
have h : ∀ b ∈ t, Eq (α := ℝ≥0∞) (if f (x, b) ∈ Prod.mk b ⁻¹' s then 1 else 0) 1
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]
-- 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: 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]
-- 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 : α
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}
⊢ 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₂ : 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}
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]
-- 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 : α
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}
⊢ 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₃ : 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}
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]
-- 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 : α
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}
⊢ 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 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
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]
-- 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 : α
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
⊢ 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 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
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]
-- 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 (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have this : ∀ (b : β),
  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: have : ∀ b : β, η (a, b) (Prod.mk b ⁻¹' s) ≤ η (a, b) (Prod.mk b ⁻¹' t) := fun b =>
    measure_mono (Set.preimage_mono (subset_toMeasurable _ _))
-- 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 (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
this :
  ∀ (b : β),
    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∞)
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have ht : MeasurableSet t
Tactic: have ht : MeasurableSet t := measurableSet_toMeasurable _ _
-- 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 (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
this :
  ∀ (b : β),
    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∞)
ht : MeasurableSet t
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have h2t : Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: have h2t : (κ ⊗ₖ η) a t ≠ ∞ := by rwa [measure_toMeasurable]
-- 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 (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
this :
  ∀ (b : β),
    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∞)
ht : MeasurableSet t
h2t :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
have h2t₁ : ∫⁻ (b : β),
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      (Prod.mk b ⁻¹' t) ∂(κ : (a : α) → Measure β) a ≠
  ∞
Tactic: rw [Kernel.compProd_apply ht] at h2t
Cleared hypotheses: h2t
-- 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 (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
this :
  ∀ (b : β),
    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∞)
ht : MeasurableSet t
h2t :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have ht_lt_top : ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
  LT.lt (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' t) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: have ht_lt_top : ∀ᵐ b ∂κ a, η (a, b) (Prod.mk b ⁻¹' t) < ∞ := by
    rw [Kernel.compProd_apply ht] at h2t
    exact ae_lt_top (Kernel.measurable_kernel_prodMk_left' ht a) h2t
-- 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 (β × γ)
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
h2s :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
    (∞ : ℝ≥0∞)
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a) s
this :
  ∀ (b : β),
    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∞)
ht : MeasurableSet t
h2t :
  Ne (α := ℝ≥0∞) ((((κ ⊗ₖ η : (a : α) → Measure (β × γ)) a : Measure (β × γ)) : (a : Set (β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
    (∞ : ℝ≥0∞)
ht_lt_top :
  ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ : (a : α) → Measure β) a : Measure β),
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have h : ∀ (b : β)
  (hb :
    LT.lt (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LT.lt (α := ℝ≥0∞) ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) (Prod.mk b ⁻¹' s) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: filter_upwards [ht_lt_top] with b hb